Documentation

Complexity.Computability.GenericRAM.Native.ExhaustiveCountFallback

Streaming polynomial-space exhaustive counting and finite-threshold fallback absorption #

This module formalizes the streaming polynomial-space $2^n$ exhaustive counting fallbacks and their constant-factor time absorption from Ā§5.5 (Proof of Theorem 2.2, p. 39) and Ā§6.4 (Proof of Proposition 6.4, pp. 43ā€“44) of OpenAI, The Exponential Time Hypothesis is False:

  1. Streaming sparse š”½ā‚‚ polynomial system counter (countSystemExhaustive): iterates over all 0 ā‰¤ idx < 2 ^ n via Cslib.GenericRAM.BooleanFold.run without materializing enumList n, retaining only ((n, sys), Z) with Z ā‰¤ idx ā‰¤ 2 ^ n, and increments Z whenever Cslib.Complexity.evalSystem vanishes on (lowBits n idx).getD v false (defaulting variable indices v ā‰„ n to false). On canonical equations with variables < n, this equals Cslib.BitString.commonZeroCount.
  2. Streaming declared-variable CNF model counter (countCNFExhaustive): iterates over all 0 ā‰¤ idx < 2 ^ n via Cslib.GenericRAM.BooleanFold.run, evaluating Ļ† : CNF ā„• on (lowBits n idx).getD v false (defaulting variables v ā‰„ n to false), and equals CNF.modelCountOn Ļ† (Finset.range n) (hence 2 ^ (n - Ļ†.numVars) * Ļ†.modelCount whenever every occurring variable of Ļ† is < n).
  3. Finite-threshold guard-fallback combinator and constant absorption: combines a polynomial guard ok : Ī± ā†’ Bool, a fast certificate c_fast, and an exhaustive fallback certificate c_exhaust via NativeCertificate.branch (evaluating only the selected branch), preserves polynomial workspace, and absorbs the O(poly(|x|) * 2 ^ Ī¼(x)) fallback runtime into a pure additive polynomial C * (|ei x| + 1) ^ d (and into C' * (|ei x| + 1) ^ e * 2 ^ E(x) for any nonnegative exponent E(x)) whenever ok x = false ā†’ Ī¼ x < Nā‚€.

Main definitions #

Main results #

References #

Streaming Boolean-Cube Predicate Counter Infrastructure #

source
def Cslib.GenericRAM.ExhaustiveCountFallback.countStep {P : Type} (pred : P ā†’ List Bool ā†’ Bool) (s : (ā„• Ɨ List Bool) Ɨ (ā„• Ɨ P) Ɨ ā„•) :
(ā„• Ɨ P) Ɨ ā„•

One streaming BooleanFold callback step for counting n-bit words satisfying pred: retains the captured input s.2.1 = (n, payload) and increments the binary counter s.2.2 when pred payload word holds on the current decoded n-bit word s.1.2.

Instances For
    source
    theorem Cslib.GenericRAM.ExhaustiveCountFallback.computableInPolyTime_countStep {P : Type} {encP : P ā†Ŗ List Bool} {pred : P ā†’ List Bool ā†’ Bool} (hpred : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : P Ɨ List Bool) => pred q.1 q.2) (Turing.MultiTapeTM.encPair encP Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) :
    Turing.MultiTapeTM.ComputableInPolyTime (countStep pred) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encP) Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encP) Turing.MultiTapeTM.encNat)

    If evaluating pred on (payload, word) is polynomial-time, then one streaming countStep callback is polynomial-time.

    source
    noncomputable def Cslib.GenericRAM.ExhaustiveCountFallback.countPredicateCertificate {P : Type} {encP : P ā†Ŗ List Bool} {pred : P ā†’ List Bool ā†’ Bool} (hpred : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : P Ɨ List Bool) => pred q.1 q.2) (Turing.MultiTapeTM.encPair encP Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) :
    NativeCertificate (fun (x : ā„• Ɨ P) => (BooleanFold.run (countStep pred) x.1 (x, 0)).2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encP) Turing.MultiTapeTM.encNat

    Generic NativeCertificate for counting n-bit assignments satisfying pred via BooleanFold.certificate without materializing enumList n.

    Instances For

      1. Streaming Sparse š”½ā‚‚ Polynomial System Counter (Ā§5.5, pp. 38ā€“39) #

      source
      def Cslib.GenericRAM.ExhaustiveCountFallback.countSystemPrefix (x : ā„• Ɨ List (List (List ā„•))) (j : ā„•) :
      ā„• Ɨ ā„• Ɨ (ā„• Ɨ List (List (List ā„•))) Ɨ ā„•

      Prefix state after visiting the first j assignments 0 ā‰¤ idx < j of the streaming sparse š”½ā‚‚ system counter on (n, sys). Variable indices v ā‰„ n default to false via List.getD.

      Instances For
        source
        def Cslib.GenericRAM.ExhaustiveCountFallback.countSystemExhaustive (x : ā„• Ɨ List (List (List ā„•))) :
        ā„•

        Streaming polynomial-space $2^n$ sparse š”½ā‚‚ polynomial system counter (Ā§5.5, p. 39): iterates over 0 ā‰¤ idx < 2 ^ n via BooleanFold.run without materializing enumList n, keeping live state ((n, sys), Z) and incrementing Z whenever every equation in sys evaluates to false (0 āˆˆ š”½ā‚‚) under (lowBits n idx).getD v false (variables v ā‰„ n default to false).

        Instances For
          source
          def Cslib.GenericRAM.ExhaustiveCountFallback.equationToFinset (n : ā„•) (eq : List (List ā„•)) :
          Finset (Finset (Fin n))

          Project a sparse equation eq : List (List ā„•) onto Finset (Finset (Fin n)) by intersecting each monomial with {0, ā€¦, n - 1}.

          Instances For
            source
            @[simp]
            theorem Cslib.GenericRAM.ExhaustiveCountFallback.countSystemPrefix_payload (x : ā„• Ɨ List (List (List ā„•))) (j : ā„•) :
            (countSystemPrefix x j).2.2.1 = x

            At every prefix j, the retained payload in countSystemPrefix x j equals x = (n, sys).

            source
            theorem Cslib.GenericRAM.ExhaustiveCountFallback.countSystemPrefix_count_eq (x : ā„• Ɨ List (List (List ā„•))) (j : ā„•) :
            (countSystemPrefix x j).2.2.2 = List.countP (fun (word : List Bool) => Complexity.evalSystem x.2 fun (v : ā„•) => word.getD v false) (List.map (BitString.lowBits x.1) (List.range j))

            At every prefix j, the running count Z equals the number of indices idx < j whose decoded n-bit word satisfies evalSystem.

            source
            theorem Cslib.GenericRAM.ExhaustiveCountFallback.countSystemPrefix_le_index (x : ā„• Ɨ List (List (List ā„•))) (j : ā„•) :
            (countSystemPrefix x j).2.2.2 ā‰¤ j

            Unconditional prefix count bound Z ā‰¤ j for countSystemPrefix.

            source
            theorem Cslib.GenericRAM.ExhaustiveCountFallback.countSystemPrefix_invariant (x : ā„• Ɨ List (List (List ā„•))) {j : ā„•} (hj : j ā‰¤ 2 ^ x.1) :
            (countSystemPrefix x j).2.2.2 ā‰¤ j āˆ§ j ā‰¤ 2 ^ x.1

            Prefix invariant Z ā‰¤ j ā‰¤ 2 ^ n for countSystemPrefix along the 2 ^ n traversal.

            source
            theorem Cslib.GenericRAM.ExhaustiveCountFallback.countSystemExhaustive_eq_card_filter (n : ā„•) (sys : List (List (List ā„•))) :
            countSystemExhaustive (n, sys) = {Ļƒ : BitString n | (Complexity.evalSystem sys fun (v : ā„•) => (List.ofFn Ļƒ).getD v false) = true}.card

            countSystemExhaustive (n, sys) equals the cardinality of the BitString n assignments whose decoded word (List.ofFn Ļƒ).getD v false satisfies evalSystem sys.

            source
            theorem Cslib.GenericRAM.ExhaustiveCountFallback.countSystemExhaustive_eq_commonZeroCount {n : ā„•} {sys : List (List (List ā„•))} (hsys : āˆ€ eq āˆˆ sys, Complexity.IsCanonicalEquation eq āˆ§ āˆ€ m āˆˆ eq, āˆ€ v āˆˆ m, v < n) :
            countSystemExhaustive (n, sys) = BitString.commonZeroCount Finset.univ fun (i : Fin sys.length) => equationToFinset n sys[i]

            Semantic bridge to Cslib.BitString.commonZeroCount: when every equation in sys is canonical (IsCanonicalEquation) and all occurring variable indices satisfy v < n, countSystemExhaustive (n, sys) equals commonZeroCount of the projected Fin n equations.

            source
            @[simp]
            theorem Cslib.GenericRAM.ExhaustiveCountFallback.countSystemExhaustive_nil (n : ā„•) :
            countSystemExhaustive (n, []) = 2 ^ n

            An empty list of equations has 2 ^ n common zeros (Ā§5.5, p. 38).

            source
            theorem Cslib.GenericRAM.ExhaustiveCountFallback.countSystemExhaustive_eq_zero_of_nil_mem {n : ā„•} {sys : List (List (List ā„•))} (h : [[]] āˆˆ sys) :
            countSystemExhaustive (n, sys) = 0

            A system containing the contradictory constant equation [[]] (1 = 0) has 0 common zeros (Ā§5.5, p. 38).

            source
            theorem Cslib.GenericRAM.ExhaustiveCountFallback.computableInPolyTime_evalSystem_word :
            Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List (List (List ā„•)) Ɨ List Bool) => Complexity.evalSystem p.1 fun (v : ā„•) => p.2.getD v false) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

            Evaluating a sparse š”½ā‚‚ polynomial system sys on (word.getD v false) is polynomial-time in the pair encoding (encList (encList (encList encNat)), encBits).

            source
            noncomputable def Cslib.GenericRAM.ExhaustiveCountFallback.countSystemExhaustiveCertificate :
            NativeCertificate countSystemExhaustive (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat

            Native resource certificate for countSystemExhaustive over (encUnary, encSys) ā†’ encNat.

            Instances For
              source
              theorem Cslib.GenericRAM.ExhaustiveCountFallback.polyBounded_countSystemExhaustive_space :
              Turing.MultiTapeTM.PolyBounded (fun (x : ā„• Ɨ List (List (List ā„•))) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) x).length) countSystemExhaustiveCertificate.space

              countSystemExhaustiveCertificate uses polynomial workspace in the encoded input length.

              source
              theorem Cslib.GenericRAM.ExhaustiveCountFallback.exists_countSystemExhaustive_time_le :
              āˆƒ (P_ex : ā„• Ɨ List (List (List ā„•)) ā†’ ā„•) (Q_ex : ā„• Ɨ List (List (List ā„•)) ā†’ ā„•), Turing.MultiTapeTM.PolyBounded (fun (x : ā„• Ɨ List (List (List ā„•))) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) x).length) P_ex āˆ§ Turing.MultiTapeTM.PolyBounded (fun (x : ā„• Ɨ List (List (List ā„•))) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) x).length) Q_ex āˆ§ āˆ€ (x : ā„• Ɨ List (List (List ā„•))), countSystemExhaustiveCertificate.time x ā‰¤ (2 ^ x.1 + 1) * P_ex x + Q_ex x

              countSystemExhaustiveCertificate runs in (2 ^ n + 1) * P_ex x + Q_ex x steps for polynomially bounded P_ex, Q_ex.

              source
              theorem Cslib.GenericRAM.ExhaustiveCountFallback.computableInO_countSystemExhaustive :
              āˆƒ (d : ā„•) (S : ā„• Ɨ List (List (List ā„•)) ā†’ ā„•), Turing.MultiTapeTM.PolyBounded (fun (x : ā„• Ɨ List (List (List ā„•))) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) x).length) S āˆ§ Turing.MultiTapeTM.ComputableInO countSystemExhaustive (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat (fun (x : ā„• Ɨ List (List (List ā„•))) => 2 ^ x.1 * (((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) x).length + 1) ^ d) S

              countSystemExhaustive is computable in O((|x| + 1) ^ d * 2 ^ n) time and polynomial workspace.

              2. Streaming Declared-Variable CNF Model Counter (Ā§6.4, pp. 43ā€“44) #

              source
              def Cslib.GenericRAM.ExhaustiveCountFallback.countCNFPrefix (x : ā„• Ɨ Logic.PL.CNF ā„•) (j : ā„•) :
              ā„• Ɨ ā„• Ɨ (ā„• Ɨ Logic.PL.CNF ā„•) Ɨ ā„•

              Prefix state after visiting the first j assignments 0 ā‰¤ idx < j of the streaming declared-variable CNF ā„• model counter on (n, Ļ†). Variable indices v ā‰„ n default to false via (lowBits n idx).getD v false.

              Instances For
                source
                def Cslib.GenericRAM.ExhaustiveCountFallback.countCNFExhaustive (x : ā„• Ɨ Logic.PL.CNF ā„•) :
                ā„•

                Streaming polynomial-space $2^n$ declared-variable CNF model counter (Ā§6.4, pp. 43ā€“44): iterates over 0 ā‰¤ idx < 2 ^ n via BooleanFold.run without materializing enumList n, keeping live state ((n, Ļ†), Z) and incrementing Z when Ļ†.eval (fun v => (lowBits n idx).getD v false) is true. Variable indices v ā‰„ n default to false; to interpret countCNFExhaustive (n, Ļ†) as the satisfying-assignment count on n declared variables, require āˆ€ v āˆˆ Ļ†.vars, v < n.

                Instances For
                  source
                  @[simp]
                  theorem Cslib.GenericRAM.ExhaustiveCountFallback.countCNFPrefix_payload (x : ā„• Ɨ Logic.PL.CNF ā„•) (j : ā„•) :
                  (countCNFPrefix x j).2.2.1 = x

                  At every prefix j, the retained payload in countCNFPrefix x j equals x = (n, Ļ†).

                  source
                  theorem Cslib.GenericRAM.ExhaustiveCountFallback.countCNFPrefix_count_eq (x : ā„• Ɨ Logic.PL.CNF ā„•) (j : ā„•) :
                  (countCNFPrefix x j).2.2.2 = List.countP (fun (word : List Bool) => Logic.PL.CNF.eval (fun (v : ā„•) => word.getD v false) x.2) (List.map (BitString.lowBits x.1) (List.range j))

                  At every prefix j, the running count Z equals the number of indices idx < j whose decoded n-bit word satisfies Ļ†.

                  source
                  theorem Cslib.GenericRAM.ExhaustiveCountFallback.countCNFPrefix_le_index (x : ā„• Ɨ Logic.PL.CNF ā„•) (j : ā„•) :
                  (countCNFPrefix x j).2.2.2 ā‰¤ j

                  Unconditional prefix count bound Z ā‰¤ j for countCNFPrefix.

                  source
                  theorem Cslib.GenericRAM.ExhaustiveCountFallback.countCNFPrefix_invariant (x : ā„• Ɨ Logic.PL.CNF ā„•) {j : ā„•} (hj : j ā‰¤ 2 ^ x.1) :
                  (countCNFPrefix x j).2.2.2 ā‰¤ j āˆ§ j ā‰¤ 2 ^ x.1

                  Prefix invariant Z ā‰¤ j ā‰¤ 2 ^ n for countCNFPrefix along the 2 ^ n traversal.

                  source
                  theorem Cslib.GenericRAM.ExhaustiveCountFallback.countCNFExhaustive_eq_card_filter (n : ā„•) (Ļ† : Logic.PL.CNF ā„•) :
                  countCNFExhaustive (n, Ļ†) = {Ļƒ : BitString n | Logic.PL.CNF.eval (fun (v : ā„•) => (List.ofFn Ļƒ).getD v false) Ļ† = true}.card

                  countCNFExhaustive (n, Ļ†) equals the cardinality of the BitString n assignments whose decoded word (List.ofFn Ļƒ).getD v false satisfies Ļ†.

                  source
                  theorem Cslib.GenericRAM.ExhaustiveCountFallback.countCNFExhaustive_eq_modelCountOn_range (n : ā„•) (Ļ† : Logic.PL.CNF ā„•) :
                  countCNFExhaustive (n, Ļ†) = Ļ†.modelCountOn (Finset.range n)

                  Exact agreement with CNF.modelCountOn Ļ† (Finset.range n): both countCNFExhaustive (n, Ļ†) and CNF.modelCountOn Ļ† (Finset.range n) range over n-bit assignments on {0, ā€¦, n - 1} and extend variables v ā‰„ n by false.

                  source
                  theorem Cslib.GenericRAM.ExhaustiveCountFallback.countCNFExhaustive_eq_mul_modelCount {n : ā„•} {Ļ† : Logic.PL.CNF ā„•} (hvars : āˆ€ v āˆˆ Ļ†.vars, v < n) :
                  countCNFExhaustive (n, Ļ†) = 2 ^ (n - Ļ†.numVars) * Ļ†.modelCount

                  When all occurring variables of Ļ† satisfy v < n, countCNFExhaustive (n, Ļ†) equals 2 ^ (n - Ļ†.numVars) * Ļ†.modelCount, doubling for each unused declared variable < n.

                  source
                  @[simp]
                  theorem Cslib.GenericRAM.ExhaustiveCountFallback.countCNFExhaustive_nil (n : ā„•) :
                  countCNFExhaustive (n, []) = 2 ^ n

                  An empty formula [] has 2 ^ n satisfying assignments on n declared variables (Ā§6.4, p. 43), including n = 0.

                  source
                  theorem Cslib.GenericRAM.ExhaustiveCountFallback.countCNFExhaustive_eq_zero_of_nil_mem {n : ā„•} {Ļ† : Logic.PL.CNF ā„•} (h : [] āˆˆ Ļ†) :
                  countCNFExhaustive (n, Ļ†) = 0

                  A formula containing an empty clause [] has 0 satisfying assignments (Ā§6.4, p. 43).

                  source
                  theorem Cslib.GenericRAM.ExhaustiveCountFallback.computableInPolyTime_evalCNF_word :
                  Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Logic.PL.CNF ā„• Ɨ List Bool) => Logic.PL.CNF.eval (fun (v : ā„•) => p.2.getD v false) p.1) (Turing.MultiTapeTM.encPair Complexity.encCNF Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

                  Evaluating Ļ† : CNF ā„• on (word.getD v false) is polynomial-time in (encCNF, encBits).

                  source
                  noncomputable def Cslib.GenericRAM.ExhaustiveCountFallback.countCNFExhaustiveCertificate :
                  NativeCertificate countCNFExhaustive (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Complexity.encCNF) Turing.MultiTapeTM.encNat

                  Native resource certificate for countCNFExhaustive over (encUnary, encCNF) ā†’ encNat.

                  Instances For
                    source
                    theorem Cslib.GenericRAM.ExhaustiveCountFallback.polyBounded_countCNFExhaustive_space :
                    Turing.MultiTapeTM.PolyBounded (fun (x : ā„• Ɨ Logic.PL.CNF ā„•) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Complexity.encCNF) x).length) countCNFExhaustiveCertificate.space

                    countCNFExhaustiveCertificate uses polynomial workspace in the encoded input length.

                    source
                    theorem Cslib.GenericRAM.ExhaustiveCountFallback.exists_countCNFExhaustive_time_le :
                    āˆƒ (P_ex : ā„• Ɨ Logic.PL.CNF ā„• ā†’ ā„•) (Q_ex : ā„• Ɨ Logic.PL.CNF ā„• ā†’ ā„•), Turing.MultiTapeTM.PolyBounded (fun (x : ā„• Ɨ Logic.PL.CNF ā„•) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Complexity.encCNF) x).length) P_ex āˆ§ Turing.MultiTapeTM.PolyBounded (fun (x : ā„• Ɨ Logic.PL.CNF ā„•) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Complexity.encCNF) x).length) Q_ex āˆ§ āˆ€ (x : ā„• Ɨ Logic.PL.CNF ā„•), countCNFExhaustiveCertificate.time x ā‰¤ (2 ^ x.1 + 1) * P_ex x + Q_ex x

                    countCNFExhaustiveCertificate runs in (2 ^ n + 1) * P_ex x + Q_ex x steps for polynomially bounded P_ex, Q_ex.

                    source
                    theorem Cslib.GenericRAM.ExhaustiveCountFallback.computableInO_countCNFExhaustive :
                    āˆƒ (d : ā„•) (S : ā„• Ɨ Logic.PL.CNF ā„• ā†’ ā„•), Turing.MultiTapeTM.PolyBounded (fun (x : ā„• Ɨ Logic.PL.CNF ā„•) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Complexity.encCNF) x).length) S āˆ§ Turing.MultiTapeTM.ComputableInO countCNFExhaustive (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Complexity.encCNF) Turing.MultiTapeTM.encNat (fun (x : ā„• Ɨ Logic.PL.CNF ā„•) => 2 ^ x.1 * (((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Complexity.encCNF) x).length + 1) ^ d) S

                    countCNFExhaustive is computable in O((|x| + 1) ^ d * 2 ^ n) time and polynomial workspace.

                    3. Finite-Threshold Guard-Fallback Combinator & Constant Absorption (Ā§5.5 & Ā§6.4) #

                    source
                    theorem Cslib.GenericRAM.ExhaustiveCountFallback.ite_eq_of_agrees {Ī± Ī² : Type} {ok : Ī± ā†’ Bool} {f_fast f_exhaust f : Ī± ā†’ Ī²} (hfast : āˆ€ (x : Ī±), ok x = true ā†’ f_fast x = f x) (hex : āˆ€ (x : Ī±), ok x = false ā†’ f_exhaust x = f x) (x : Ī±) :
                    (if ok x = true then f_fast x else f_exhaust x) = f x

                    Pointwise agreement of if ok x then f_fast x else f_exhaust x with a target specification f whenever f_fast agrees with f on ok x = true and f_exhaust agrees with f on ok x = false.

                    source
                    noncomputable def Cslib.GenericRAM.ExhaustiveCountFallback.guardedBranchOfPolyTime {Ī± Ī² : Type} {ei : Ī± ā†Ŗ List Bool} {eo : Ī² ā†Ŗ List Bool} {ok : Ī± ā†’ Bool} {f_fast f_exhaust : Ī± ā†’ Ī²} (hok : Turing.MultiTapeTM.ComputableInPolyTime ok ei Turing.MultiTapeTM.encBool) (c_fast : NativeCertificate f_fast ei eo) (c_exhaust : NativeCertificate f_exhaust ei eo) :
                    NativeCertificate (fun (x : Ī±) => if ok x = true then f_fast x else f_exhaust x) ei eo

                    Build the selected-branch NativeCertificate for fun x => if ok x then f_fast x else f_exhaust x from a ComputableInPolyTime guard ok, evaluating only the selected branch.

                    Instances For
                      source
                      def Cslib.GenericRAM.ExhaustiveCountFallback.guardedTargetCertificate {Ī± Ī² : Type} {ei : Ī± ā†Ŗ List Bool} {eo : Ī² ā†Ŗ List Bool} {ok : Ī± ā†’ Bool} {f_fast f_exhaust f : Ī± ā†’ Ī²} (c_ok : NativeCertificate ok ei Turing.MultiTapeTM.encBool) (c_fast : NativeCertificate f_fast ei eo) (c_exhaust : NativeCertificate f_exhaust ei eo) (hfast : āˆ€ (x : Ī±), ok x = true ā†’ f_fast x = f x) (hex : āˆ€ (x : Ī±), ok x = false ā†’ f_exhaust x = f x) :
                      NativeCertificate f ei eo

                      Build a NativeCertificate directly for a target specification f : Ī± ā†’ Ī² via NativeCertificate.branch, charging only c_ok and the selected branch.

                      Instances For
                        source
                        @[simp]
                        theorem Cslib.GenericRAM.ExhaustiveCountFallback.guardedTargetCertificate_time {Ī± Ī² : Type} {ei : Ī± ā†Ŗ List Bool} {eo : Ī² ā†Ŗ List Bool} {ok : Ī± ā†’ Bool} {f_fast f_exhaust f : Ī± ā†’ Ī²} (c_ok : NativeCertificate ok ei Turing.MultiTapeTM.encBool) (c_fast : NativeCertificate f_fast ei eo) (c_exhaust : NativeCertificate f_exhaust ei eo) (hfast : āˆ€ (x : Ī±), ok x = true ā†’ f_fast x = f x) (hex : āˆ€ (x : Ī±), ok x = false ā†’ f_exhaust x = f x) (x : Ī±) :
                        (guardedTargetCertificate c_ok c_fast c_exhaust hfast hex).time x = c_ok.time x + if ok x = true then c_fast.time x else c_exhaust.time x
                        source
                        @[simp]
                        theorem Cslib.GenericRAM.ExhaustiveCountFallback.guardedTargetCertificate_space {Ī± Ī² : Type} {ei : Ī± ā†Ŗ List Bool} {eo : Ī² ā†Ŗ List Bool} {ok : Ī± ā†’ Bool} {f_fast f_exhaust f : Ī± ā†’ Ī²} (c_ok : NativeCertificate ok ei Turing.MultiTapeTM.encBool) (c_fast : NativeCertificate f_fast ei eo) (c_exhaust : NativeCertificate f_exhaust ei eo) (hfast : āˆ€ (x : Ī±), ok x = true ā†’ f_fast x = f x) (hex : āˆ€ (x : Ī±), ok x = false ā†’ f_exhaust x = f x) (x : Ī±) :
                        (guardedTargetCertificate c_ok c_fast c_exhaust hfast hex).space x = c_ok.space x + if ok x = true then c_fast.space x else c_exhaust.space x
                        source
                        noncomputable def Cslib.GenericRAM.ExhaustiveCountFallback.guardedTargetOfPolyTime {Ī± Ī² : Type} {ei : Ī± ā†Ŗ List Bool} {eo : Ī² ā†Ŗ List Bool} {ok : Ī± ā†’ Bool} {f_fast f_exhaust f : Ī± ā†’ Ī²} (hok : Turing.MultiTapeTM.ComputableInPolyTime ok ei Turing.MultiTapeTM.encBool) (c_fast : NativeCertificate f_fast ei eo) (c_exhaust : NativeCertificate f_exhaust ei eo) (hfast : āˆ€ (x : Ī±), ok x = true ā†’ f_fast x = f x) (hex : āˆ€ (x : Ī±), ok x = false ā†’ f_exhaust x = f x) :
                        NativeCertificate f ei eo

                        Build a NativeCertificate for target f from a ComputableInPolyTime guard ok, a fast certificate c_fast, and an exhaustive fallback certificate c_exhaust.

                        Instances For
                          source
                          theorem Cslib.GenericRAM.ExhaustiveCountFallback.polyBounded_branch_space {Ī± Ī² : Type} {ei : Ī± ā†Ŗ List Bool} {eo : Ī² ā†Ŗ List Bool} {ok : Ī± ā†’ Bool} {f_fast f_exhaust : Ī± ā†’ Ī²} (c_ok : NativeCertificate ok ei Turing.MultiTapeTM.encBool) (c_fast : NativeCertificate f_fast ei eo) (c_exhaust : NativeCertificate f_exhaust ei eo) (hok : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) c_ok.space) (hfast : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) c_fast.space) (hex : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) c_exhaust.space) :
                          Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) (c_ok.branch c_fast c_exhaust).space

                          Polynomial workspace preservation: NativeCertificate.branch has polynomial workspace whenever the guard, fast branch, and exhaustive fallback each have polynomial workspace (without assuming either branch runs in polynomial time).

                          source
                          theorem Cslib.GenericRAM.ExhaustiveCountFallback.exists_branch_time_le_of_finite_threshold {Ī± Ī² : Type} {ei : Ī± ā†Ŗ List Bool} {eo : Ī² ā†Ŗ List Bool} {ok : Ī± ā†’ Bool} {f_fast f_exhaust : Ī± ā†’ Ī²} {Ī¼ P_ex Q_ex : Ī± ā†’ ā„•} {Nā‚€ : ā„•} (c_ok : NativeCertificate ok ei Turing.MultiTapeTM.encBool) (c_fast : NativeCertificate f_fast ei eo) (c_exhaust : NativeCertificate f_exhaust ei eo) (hok : c_ok.IsPolynomial) (hs_fast : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) c_fast.space) (hs_ex : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) c_exhaust.space) (hthresh : āˆ€ (x : Ī±), ok x = false ā†’ Ī¼ x < Nā‚€) (hP : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) P_ex) (hQ : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) Q_ex) (ht_ex : āˆ€ (x : Ī±), ok x = false ā†’ c_exhaust.time x ā‰¤ (2 ^ Ī¼ x + 1) * P_ex x + Q_ex x) :
                          Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) (c_ok.branch c_fast c_exhaust).space āˆ§ āˆƒ (C : ā„•) (d : ā„•), āˆ€ (x : Ī±), (c_ok.branch c_fast c_exhaust).time x ā‰¤ (if ok x = true then c_fast.time x else 0) + C * ((ei x).length + 1) ^ d

                          Finite-threshold fallback time absorption on NativeCertificate.branch (Ā§5.5 p. 39, Ā§6.4 p. 44): if ok x = false ā†’ Ī¼ x < Nā‚€ for a constant threshold Nā‚€ and c_exhaust.time x ā‰¤ (2 ^ Ī¼ x + 1) * P_ex x + Q_ex x with PolyBounded P_ex, Q_ex, then the guarded branch preserves polynomial workspace and bounds total time by (if ok x then c_fast.time x else 0) + C * (|ei x| + 1) ^ d.

                          source
                          theorem Cslib.GenericRAM.ExhaustiveCountFallback.computableInO_of_guarded_fallback {Ī± Ī² : Type} {ei : Ī± ā†Ŗ List Bool} {eo : Ī² ā†Ŗ List Bool} {ok : Ī± ā†’ Bool} {f_fast f_exhaust f : Ī± ā†’ Ī²} {Ī¼ P_ex Q_ex T_fast : Ī± ā†’ ā„•} {Nā‚€ : ā„•} (hok : Turing.MultiTapeTM.ComputableInPolyTime ok ei Turing.MultiTapeTM.encBool) (c_fast : NativeCertificate f_fast ei eo) (c_exhaust : NativeCertificate f_exhaust ei eo) (hfast_eq : āˆ€ (x : Ī±), ok x = true ā†’ f_fast x = f x) (hex_eq : āˆ€ (x : Ī±), ok x = false ā†’ f_exhaust x = f x) (hs_fast : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) c_fast.space) (hs_ex : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) c_exhaust.space) (hthresh : āˆ€ (x : Ī±), ok x = false ā†’ Ī¼ x < Nā‚€) (hP : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) P_ex) (hQ : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) Q_ex) (ht_fast : āˆ€ (x : Ī±), ok x = true ā†’ c_fast.time x ā‰¤ T_fast x) (ht_ex : āˆ€ (x : Ī±), ok x = false ā†’ c_exhaust.time x ā‰¤ (2 ^ Ī¼ x + 1) * P_ex x + Q_ex x) :
                          āˆƒ (C : ā„•) (d : ā„•) (S : Ī± ā†’ ā„•), Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) S āˆ§ Turing.MultiTapeTM.ComputableInO f ei eo (fun (x : Ī±) => T_fast x + C * ((ei x).length + 1) ^ d) S

                          Combined ComputableInO theorem under a ComputableInPolyTime guard: when ok x = false ā†’ Ī¼ x < Nā‚€, the guarded machine computes f in polynomial workspace and time T_fast x + C * (|ei x| + 1) ^ d.

                          source
                          theorem Cslib.GenericRAM.ExhaustiveCountFallback.exists_nat_exp_bound_of_guarded_fallback {Ī± Ī² : Type} {ei : Ī± ā†Ŗ List Bool} {eo : Ī² ā†Ŗ List Bool} {ok : Ī± ā†’ Bool} {f_fast f_exhaust f : Ī± ā†’ Ī²} {Ī¼ P_ex Q_ex E : Ī± ā†’ ā„•} {Nā‚€ C_f d_f : ā„•} (hok : Turing.MultiTapeTM.ComputableInPolyTime ok ei Turing.MultiTapeTM.encBool) (c_fast : NativeCertificate f_fast ei eo) (c_exhaust : NativeCertificate f_exhaust ei eo) (hfast_eq : āˆ€ (x : Ī±), ok x = true ā†’ f_fast x = f x) (hex_eq : āˆ€ (x : Ī±), ok x = false ā†’ f_exhaust x = f x) (hs_fast : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) c_fast.space) (hs_ex : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) c_exhaust.space) (hthresh : āˆ€ (x : Ī±), ok x = false ā†’ Ī¼ x < Nā‚€) (hP : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) P_ex) (hQ : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) Q_ex) (ht_fast : āˆ€ (x : Ī±), ok x = true ā†’ c_fast.time x ā‰¤ C_f * ((ei x).length + 1) ^ d_f * 2 ^ E x) (ht_ex : āˆ€ (x : Ī±), ok x = false ā†’ c_exhaust.time x ā‰¤ (2 ^ Ī¼ x + 1) * P_ex x + Q_ex x) :
                          āˆƒ (C' : ā„•) (e : ā„•) (S : Ī± ā†’ ā„•), Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) S āˆ§ (āˆ€ (x : Ī±), (guardedTargetOfPolyTime hok c_fast c_exhaust hfast_eq hex_eq).time x ā‰¤ C' * ((ei x).length + 1) ^ e * 2 ^ E x) āˆ§ Turing.MultiTapeTM.ComputableInO f ei eo (fun (x : Ī±) => ((ei x).length + 1) ^ e * 2 ^ E x) S

                          Natural-exponent constant absorption: for any E : Ī± ā†’ ā„•, if the fast branch satisfies ok x = true ā†’ c_fast.time x ā‰¤ C_f * (|ei x| + 1) ^ d_f * 2 ^ E x and ok x = false ā†’ Ī¼ x < Nā‚€, then the finite exhaustive-fallback cases are absorbed into C' * (|ei x| + 1) ^ e * 2 ^ E x.

                          source
                          theorem Cslib.GenericRAM.ExhaustiveCountFallback.exists_real_exp_bound_of_guarded_fallback {Ī± Ī² : Type} {ei : Ī± ā†Ŗ List Bool} {eo : Ī² ā†Ŗ List Bool} {ok : Ī± ā†’ Bool} {f_fast f_exhaust f : Ī± ā†’ Ī²} {Ī¼ P_ex Q_ex : Ī± ā†’ ā„•} {E : Ī± ā†’ ā„} {Nā‚€ C_f d_f : ā„•} (hok : Turing.MultiTapeTM.ComputableInPolyTime ok ei Turing.MultiTapeTM.encBool) (c_fast : NativeCertificate f_fast ei eo) (c_exhaust : NativeCertificate f_exhaust ei eo) (hfast_eq : āˆ€ (x : Ī±), ok x = true ā†’ f_fast x = f x) (hex_eq : āˆ€ (x : Ī±), ok x = false ā†’ f_exhaust x = f x) (hs_fast : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) c_fast.space) (hs_ex : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) c_exhaust.space) (hthresh : āˆ€ (x : Ī±), ok x = false ā†’ Ī¼ x < Nā‚€) (hP : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) P_ex) (hQ : Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) Q_ex) (hE : āˆ€ (x : Ī±), 0 ā‰¤ E x) (ht_fast : āˆ€ (x : Ī±), ok x = true ā†’ ā†‘(c_fast.time x) ā‰¤ ā†‘C_f * (ā†‘(ei x).length + 1) ^ d_f * 2 ^ E x) (ht_ex : āˆ€ (x : Ī±), ok x = false ā†’ c_exhaust.time x ā‰¤ (2 ^ Ī¼ x + 1) * P_ex x + Q_ex x) :
                          āˆƒ (C' : ā„•) (e : ā„•) (S : Ī± ā†’ ā„•), Turing.MultiTapeTM.PolyBounded (fun (x : Ī±) => (ei x).length) S āˆ§ (āˆ€ (x : Ī±), ā†‘((guardedTargetOfPolyTime hok c_fast c_exhaust hfast_eq hex_eq).time x) ā‰¤ ā†‘C' * (ā†‘(ei x).length + 1) ^ e * 2 ^ E x) āˆ§ Turing.MultiTapeTM.ComputableInO f ei eo (fun (x : Ī±) => ((ei x).length + 1) ^ e * āŒˆ2 ^ E xāŒ‰ā‚Š) S

                          Real-exponent subexponential constant absorption (Ā§5.5 p. 39, Ā§6.4 p. 44): for any nonnegative real exponent E : Ī± ā†’ ā„ (āˆ€ x, 0 ā‰¤ E x, including subexponential exponents such as A * Ļ (Ī¼ x)), if ok x = true ā†’ (c_fast.time x : ā„) ā‰¤ C_f * (|ei x| + 1) ^ d_f * 2 ^ E x and ok x = false ā†’ Ī¼ x < Nā‚€, then the combined guarded certificate has polynomial workspace, satisfies (cert.time x : ā„) ā‰¤ C' * (|ei x| + 1) ^ e * (2 : ā„) ^ E x for all x, and runs in ComputableInO time (|ei x| + 1) ^ e * āŒˆ(2 : ā„) ^ E xāŒ‰ā‚Š.