Documentation

Complexity.Computability.PolyTime.CNF.SparseCNFLeafCounter

Native sparse k-CNF leaf model counter and occurring-support normalization #

Implements the deterministic sparse k-CNF model-counting algorithm of Section 6.3 (equation (6.4), printed p. 43) of OpenAI, The Exponential Time Hypothesis is False on native multi-tape Turing machines, parameterized over a sparse 𝔽₂ polynomial-system counter:

Main definitions #

Main results #

References #

1. Guards, Compiled-System Invariant, and Core Definitions #

source
def Cslib.Complexity.SparseCNFLeafCounter.hasEmptyClause (ψ : Logic.PL.CNF β„•) :
Bool

Boolean check for whether ψ contains an empty clause [].

Instances For
    source
    def Cslib.Complexity.SparseCNFLeafCounter.entersSparseFastPath (k Nβ‚€ N B : β„•) (ψ : Logic.PL.CNF β„•) :
    Bool

    Guard characterizing inputs (N, B, ψ) entering the Section 6.3 parity-test fast path.

    Instances For
      source
      def Cslib.Complexity.SparseCNFLeafCounter.IsCompiledSparseSystem (k N maxEqs maxTerms : β„•) (sys : List (List (List β„•))) :
      Prop

      Sparsity, canonicality, degree, and variable-range invariant for compiled 𝔽₂ systems.

      Instances For
        source
        def Cslib.Complexity.SparseCNFLeafCounter.compiledRowCounter (k : β„•) (polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•) (q : (β„• Γ— Logic.PL.CNF β„•) Γ— List (List Bool)) :
        β„•

        Evaluates polyCounter (N, compileParitySystemBounded k ψ rows) when rows.length ≀ 6 * N.

        Instances For
          source
          def Cslib.Complexity.SparseCNFLeafCounter.sparseCNFFastPath (k N B : β„•) (polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•) (ψ : Logic.PL.CNF β„•) :
          β„•

          Deterministic Section 6.3 fast path: initial Tanner rows via initialTestsRows, 3 * N rounds of greedyParityRows, and one final compiledRowCounter call capped at 2 ^ N.

          Instances For
            source
            def Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCounter {P : Type u_1} (NOf BOf : P β†’ β„•) (k Nβ‚€ : β„•) (polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•) (x : P Γ— Logic.PL.CNF β„•) :
            β„•

            Section 6.3 declared-range sparse k-CNF model counter. Returns 0 if invalid, 2 ^ N on [], 0 if [] ∈ ψ, countCNFExhaustive (N, ψ) if N < Nβ‚€, sparseCNFFastPath k N B polyCounter ψ if ψ.length ≀ B * N, and 0 otherwise.

            Instances For
              source
              def Cslib.Complexity.SparseCNFLeafCounter.sparseCNFLeafCounter {P : Type u_1} (NOf BOf : P β†’ β„•) (k Nβ‚€ : β„•) (polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•) (x : P Γ— Logic.PL.CNF β„•) :
              β„•

              Normalized Section 6.3 sparse k-CNF leaf provider. Returns ψ.modelCount on valid sparse or below-threshold inputs, as well as empty formulas and formulas containing an empty clause. The supplied polyCounter must be exact on the compiled sparse systems required by sparseCNFLeafCounter_eq_modelCount.

              Instances For
                source
                theorem Cslib.Complexity.SparseCNFLeafCounter.hasEmptyClause_eq_true_iff {ψ : Logic.PL.CNF β„•} :
                hasEmptyClause ψ = true ↔ [] ∈ ψ
                source
                theorem Cslib.Complexity.SparseCNFLeafCounter.entersSparseFastPath_eq_true_iff {k Nβ‚€ N B : β„•} {ψ : Logic.PL.CNF β„•} :
                entersSparseFastPath k Nβ‚€ N B ψ = true ↔ Logic.PL.CNF.validDeclaredInput k N ψ = true ∧ List.isEmpty ψ = false ∧ hasEmptyClause ψ = false ∧ Nβ‚€ ≀ N ∧ List.length ψ ≀ B * N
                source
                theorem Cslib.Complexity.SparseCNFLeafCounter.isCompiledSparseSystem_compileParitySystemBounded {k N maxEqs W : β„•} {ψ : Logic.PL.CNF β„•} (hw : βˆ€ c ∈ ψ, List.length c ≀ k) (hsub : ψ.vars.toFinset βŠ† Finset.range N) {rows : List (List Bool)} (hlen : rows.length ≀ maxEqs) (hwt : βˆ€ r ∈ rows, List.count true r ≀ W) :
                IsCompiledSparseSystem k N maxEqs (W * 2 ^ k) (compileParitySystemBounded k ψ rows)

                Every compileParitySystemBounded k ψ rows on a width-≀ k formula with variables < N, rows.length ≀ maxEqs, and row Hamming weights ≀ W satisfies IsCompiledSparseSystem.

                source
                theorem Cslib.Complexity.SparseCNFLeafCounter.commonZeroCount_compileParitySystemBounded_eq_numPassing {k N : β„•} (hN : 1 ≀ N) {ψ : Logic.PL.CNF β„•} (hw : βˆ€ c ∈ ψ, List.length c ≀ k) (hsub : ψ.vars.toFinset βŠ† Finset.range N) (rows : List (List Bool)) :
                let sys := compileParitySystemBounded k ψ rows; have ψFin := Logic.PL.CNF.relabel (fun (v : β„•) => ⟨v % N, β‹―βŸ©) ψ; (BitString.commonZeroCount Finset.univ fun (i : Fin sys.length) => GenericRAM.ExhaustiveCountFallback.equationToFinset N sys[i]) = BitString.numPassing ψFin.violations (List.map (BitString.ofList (List.length ψFin)) rows) ∧ (BitString.commonZeroCount Finset.univ fun (i : Fin sys.length) => GenericRAM.ExhaustiveCountFallback.equationToFinset N sys[i]) = BitString.commonZeroCount Finset.univ (ψFin.parityRowSystem (List.map (BitString.ofList (List.length ψFin)) rows))

                Semantic bridge to equationToFinset and CNF.parityRowSystem: on a width-≀ k formula ψ with variables < N (1 ≀ N), commonZeroCount on compileParitySystemBounded k ψ rows equals both numPassing and commonZeroCount on (relabel ... ψ).parityRowSystem.

                source
                theorem Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCounter_le_two_pow {P : Type u_1} (NOf BOf : P β†’ β„•) (k Nβ‚€ : β„•) (polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•) (x : P Γ— Logic.PL.CNF β„•) :
                sparseCNFDeclaredCounter NOf BOf k Nβ‚€ polyCounter x ≀ 2 ^ NOf x.1

                Unconditional upper bound: sparseCNFDeclaredCounter never exceeds 2 ^ NOf x.1.

                source
                theorem Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCounter_eq_modelCountOn {P : Type u_1} {NOf BOf : P β†’ β„•} {k Nβ‚€ : β„•} {polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•} {p : P} {ψ : Logic.PL.CNF β„•} (hw : βˆ€ c ∈ ψ, List.length c ≀ k) (hsub : ψ.vars.toFinset βŠ† Finset.range (NOf p)) (hdom : List.length ψ ≀ BOf p * NOf p ∨ ψ = [] ∨ [] ∈ ψ ∨ NOf p < Nβ‚€) (hpoly : Nβ‚€ ≀ NOf p β†’ βˆ€ (sys : List (List (List β„•))), IsCompiledSparseSystem k (NOf p) (6 * NOf p) (BitString.initialRowWeightBound (BOf p) (List.length ψ) * 2 ^ k) sys β†’ polyCounter (NOf p, sys) = BitString.commonZeroCount Finset.univ fun (i : Fin sys.length) => GenericRAM.ExhaustiveCountFallback.equationToFinset (NOf p) sys[i]) :
                sparseCNFDeclaredCounter NOf BOf k Nβ‚€ polyCounter (p, ψ) = ψ.modelCountOn (Finset.range (NOf p))

                Exactness of sparseCNFDeclaredCounter (Β§6.3, Lemmas 6.1–6.2).

                source
                theorem Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCounter_exhaustive_eq_modelCountOn {P : Type u_1} {NOf BOf : P β†’ β„•} {k Nβ‚€ : β„•} {p : P} {ψ : Logic.PL.CNF β„•} (hw : βˆ€ c ∈ ψ, List.length c ≀ k) (hsub : ψ.vars.toFinset βŠ† Finset.range (NOf p)) (hdom : List.length ψ ≀ BOf p * NOf p ∨ ψ = [] ∨ [] ∈ ψ ∨ NOf p < Nβ‚€) :
                sparseCNFDeclaredCounter NOf BOf k Nβ‚€ GenericRAM.ExhaustiveCountFallback.countSystemExhaustive (p, ψ) = ψ.modelCountOn (Finset.range (NOf p))

                Instantiation of sparseCNFDeclaredCounter with countSystemExhaustive computes ψ.modelCountOn (Finset.range (NOf p)) unconditionally on every valid sparse formula.

                3. Normalized Leaf Provider (sparseCNFLeafCounter) #

                source
                theorem Cslib.Complexity.SparseCNFLeafCounter.sparseCNFLeafCounter_le_two_pow_numVars {P : Type u_1} (NOf BOf : P β†’ β„•) (k Nβ‚€ : β„•) (polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•) (x : P Γ— Logic.PL.CNF β„•) :
                sparseCNFLeafCounter NOf BOf k Nβ‚€ polyCounter x ≀ 2 ^ x.2.numVars

                Unconditional leaf-accumulator bound: sparseCNFLeafCounter never exceeds 2 ^ ψ.numVars on any input (p, ψ), regardless of polyCounter.

                source
                theorem Cslib.Complexity.SparseCNFLeafCounter.sparseCNFLeafCounter_eq_modelCount {P : Type u_1} {NOf BOf : P β†’ β„•} {k Nβ‚€ : β„•} {polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•} {p : P} {ψ : Logic.PL.CNF β„•} (hw : βˆ€ c ∈ ψ, List.length c ≀ k) (hsub : ψ.vars.toFinset βŠ† Finset.range (NOf p)) (hdom : List.length ψ ≀ BOf p * NOf p ∨ ψ = [] ∨ [] ∈ ψ ∨ NOf p < Nβ‚€) (hpoly : Nβ‚€ ≀ NOf p β†’ βˆ€ (sys : List (List (List β„•))), IsCompiledSparseSystem k (NOf p) (6 * NOf p) (BitString.initialRowWeightBound (BOf p) (List.length ψ) * 2 ^ k) sys β†’ polyCounter (NOf p, sys) = BitString.commonZeroCount Finset.univ fun (i : Fin sys.length) => GenericRAM.ExhaustiveCountFallback.equationToFinset (NOf p) sys[i]) :
                sparseCNFLeafCounter NOf BOf k Nβ‚€ polyCounter (p, ψ) = ψ.modelCount

                Exactness of sparseCNFLeafCounter: returns ψ.modelCount on every valid width-≀ k sparse leaf ψ with variables in Finset.range (NOf p).

                source
                theorem Cslib.Complexity.SparseCNFLeafCounter.sparseCNFLeafCounter_exhaustive_eq_modelCount {P : Type u_1} {NOf BOf : P β†’ β„•} {k Nβ‚€ : β„•} {p : P} {ψ : Logic.PL.CNF β„•} (hw : βˆ€ c ∈ ψ, List.length c ≀ k) (hsub : ψ.vars.toFinset βŠ† Finset.range (NOf p)) (hdom : List.length ψ ≀ BOf p * NOf p ∨ ψ = [] ∨ [] ∈ ψ ∨ NOf p < Nβ‚€) :
                sparseCNFLeafCounter NOf BOf k Nβ‚€ GenericRAM.ExhaustiveCountFallback.countSystemExhaustive (p, ψ) = ψ.modelCount

                Instantiation of sparseCNFLeafCounter with countSystemExhaustive computes ψ.modelCount.

                4. Native Machine Certificates and Split Time / Polynomial-Space Bounds #

                source
                def Cslib.Complexity.SparseCNFLeafCounter.sparseCNFTimeBound {P : Type} (encP : P β†ͺ List Bool) (NOf BOf : P β†’ β„•) (k Nβ‚€ : β„•) (poly qInit : β„• β†’ β„•) (R : P Γ— Logic.PL.CNF β„• β†’ β„•) (x : P Γ— Logic.PL.CNF β„•) :
                β„•

                Split Section 6.3 runtime upper bound: poly L outside entersSparseFastPath, and initial Tanner search plus (3 * N + 1) * ((2 * m) ^ P + 1) candidate system evaluations inside.

                Instances For
                  source
                  def Cslib.Complexity.SparseCNFLeafCounter.ValidPolyTimeBound {P : Type} (encP : P β†ͺ List Bool) (NOf BOf : P β†’ β„•) (k Nβ‚€ : β„•) {polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•} (cPoly : GenericRAM.NativeCertificate polyCounter (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat) (polySys : β„• β†’ β„•) (R : P Γ— Logic.PL.CNF β„• β†’ β„•) :
                  Prop

                  Hypothesis bounding cPoly.time (NOf x.1, sys) ≀ R x on every compiled sparse system of at most 6 * NOf x.1 equations and polynomial encoded length produced on the Section 6.3 fast path.

                  Instances For
                    source
                    noncomputable def Cslib.Complexity.SparseCNFLeafCounter.sparseCNFDeclaredCertificate {P : Type} {encP : P β†ͺ List Bool} {NOf BOf : P β†’ β„•} (k Nβ‚€ : β„•) (hNOf : Turing.MultiTapeTM.ComputableInPolyTime NOf encP Turing.MultiTapeTM.encUnary) (hBOf : Turing.MultiTapeTM.ComputableInPolyTime BOf encP Turing.MultiTapeTM.encUnary) {polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•} (cPoly : GenericRAM.NativeCertificate polyCounter (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat) :
                    GenericRAM.NativeCertificate (sparseCNFDeclaredCounter NOf BOf k Nβ‚€ polyCounter) (Turing.MultiTapeTM.encPair encP encCNF) Turing.MultiTapeTM.encNat

                    Native resource certificate for sparseCNFDeclaredCounter.

                    Instances For
                      source
                      theorem Cslib.Complexity.SparseCNFLeafCounter.polyBounded_sparseCNFDeclaredCertificate_space {P : Type} {encP : P β†ͺ List Bool} {NOf BOf : P β†’ β„•} (k Nβ‚€ : β„•) (hNOf : Turing.MultiTapeTM.ComputableInPolyTime NOf encP Turing.MultiTapeTM.encUnary) (hBOf : Turing.MultiTapeTM.ComputableInPolyTime BOf encP Turing.MultiTapeTM.encUnary) {polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•} (cPoly : GenericRAM.NativeCertificate polyCounter (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (y : β„• Γ— List (List (List β„•))) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) y).length) cPoly.space) :
                      Turing.MultiTapeTM.PolyBounded (fun (x : P Γ— Logic.PL.CNF β„•) => ((Turing.MultiTapeTM.encPair encP encCNF) x).length) (sparseCNFDeclaredCertificate k Nβ‚€ hNOf hBOf cPoly).space

                      Polynomial workspace of sparseCNFDeclaredCertificate.

                      source
                      theorem Cslib.Complexity.SparseCNFLeafCounter.exists_sparseCNFDeclaredCertificate_bounds {P : Type} {encP : P β†ͺ List Bool} {NOf BOf : P β†’ β„•} (k Nβ‚€ : β„•) (hNOf : Turing.MultiTapeTM.ComputableInPolyTime NOf encP Turing.MultiTapeTM.encUnary) (hBOf : Turing.MultiTapeTM.ComputableInPolyTime BOf encP Turing.MultiTapeTM.encUnary) {polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•} (cPoly : GenericRAM.NativeCertificate polyCounter (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (y : β„• Γ— List (List (List β„•))) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) y).length) cPoly.space) :
                      βˆƒ (poly : β„• β†’ β„•) (qInit : β„• β†’ β„•) (polySys : β„• β†’ β„•), PolynomiallyBounded poly ∧ PolynomiallyBounded qInit ∧ PolynomiallyBounded polySys ∧ (βˆ€ (x : P Γ— Logic.PL.CNF β„•), (sparseCNFDeclaredCertificate k Nβ‚€ hNOf hBOf cPoly).space x ≀ poly ((Turing.MultiTapeTM.encPair encP encCNF) x).length) ∧ βˆ€ (R : P Γ— Logic.PL.CNF β„• β†’ β„•), ValidPolyTimeBound encP NOf BOf k Nβ‚€ cPoly polySys R β†’ βˆ€ (x : P Γ— Logic.PL.CNF β„•), (sparseCNFDeclaredCertificate k Nβ‚€ hNOf hBOf cPoly).time x ≀ 2 * (sparseCNFTimeBound encP NOf BOf k Nβ‚€ poly qInit R x + 1)

                      Explicit certificate-level workspace and split-time bounds for sparseCNFDeclaredCertificate.

                      source
                      theorem Cslib.Complexity.SparseCNFLeafCounter.computableInO_sparseCNFDeclaredCounter {P : Type} {encP : P β†ͺ List Bool} {NOf BOf : P β†’ β„•} (k Nβ‚€ : β„•) (hNOf : Turing.MultiTapeTM.ComputableInPolyTime NOf encP Turing.MultiTapeTM.encUnary) (hBOf : Turing.MultiTapeTM.ComputableInPolyTime BOf encP Turing.MultiTapeTM.encUnary) {polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•} (cPoly : GenericRAM.NativeCertificate polyCounter (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (y : β„• Γ— List (List (List β„•))) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) y).length) cPoly.space) :
                      βˆƒ (poly : β„• β†’ β„•) (qInit : β„• β†’ β„•) (polySys : β„• β†’ β„•), PolynomiallyBounded poly ∧ PolynomiallyBounded qInit ∧ PolynomiallyBounded polySys ∧ βˆ€ (R : P Γ— Logic.PL.CNF β„• β†’ β„•), ValidPolyTimeBound encP NOf BOf k Nβ‚€ cPoly polySys R β†’ Turing.MultiTapeTM.ComputableInO (sparseCNFDeclaredCounter NOf BOf k Nβ‚€ polyCounter) (Turing.MultiTapeTM.encPair encP encCNF) Turing.MultiTapeTM.encNat (sparseCNFTimeBound encP NOf BOf k Nβ‚€ poly qInit R) fun (x : P Γ— Logic.PL.CNF β„•) => poly ((Turing.MultiTapeTM.encPair encP encCNF) x).length

                      Split ComputableInO time and polynomial-workspace bound for sparseCNFDeclaredCounter.

                      Right-Shift Normalization Certificate #

                      source
                      noncomputable def Cslib.Complexity.SparseCNFLeafCounter.normalizeDeclaredLeafCertificate {P : Type} {encP : P β†ͺ List Bool} {NOf : P β†’ β„•} (hNOf : Turing.MultiTapeTM.ComputableInPolyTime NOf encP Turing.MultiTapeTM.encUnary) {h : P Γ— Logic.PL.CNF β„• β†’ β„•} (cLeaf : GenericRAM.NativeCertificate h (Turing.MultiTapeTM.encPair encP encCNF) Turing.MultiTapeTM.encNat) :
                      GenericRAM.NativeCertificate (Logic.PL.CNF.normalizeDeclaredLeaf NOf h) (Turing.MultiTapeTM.encPair encP encCNF) Turing.MultiTapeTM.encNat

                      Native resource certificate for normalizeDeclaredLeaf NOf h, composing cLeaf with ComputableInPolyTime.binary_shiftRight on NOf x.1 - x.2.distinctVars.length.

                      Instances For
                        source
                        theorem Cslib.Complexity.SparseCNFLeafCounter.polyBounded_normalizeDeclaredLeafCertificate_space {P : Type} {encP : P β†ͺ List Bool} {NOf : P β†’ β„•} (hNOf : Turing.MultiTapeTM.ComputableInPolyTime NOf encP Turing.MultiTapeTM.encUnary) {h : P Γ— Logic.PL.CNF β„• β†’ β„•} (cLeaf : GenericRAM.NativeCertificate h (Turing.MultiTapeTM.encPair encP encCNF) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (x : P Γ— Logic.PL.CNF β„•) => ((Turing.MultiTapeTM.encPair encP encCNF) x).length) cLeaf.space) :
                        Turing.MultiTapeTM.PolyBounded (fun (x : P Γ— Logic.PL.CNF β„•) => ((Turing.MultiTapeTM.encPair encP encCNF) x).length) (normalizeDeclaredLeafCertificate hNOf cLeaf).space

                        Polynomial workspace preservation for normalizeDeclaredLeafCertificate.

                        source
                        theorem Cslib.Complexity.SparseCNFLeafCounter.exists_normalizeDeclaredLeafCertificate_bounds {P : Type} {encP : P β†ͺ List Bool} {NOf : P β†’ β„•} (hNOf : Turing.MultiTapeTM.ComputableInPolyTime NOf encP Turing.MultiTapeTM.encUnary) {h : P Γ— Logic.PL.CNF β„• β†’ β„•} (cLeaf : GenericRAM.NativeCertificate h (Turing.MultiTapeTM.encPair encP encCNF) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (x : P Γ— Logic.PL.CNF β„•) => ((Turing.MultiTapeTM.encPair encP encCNF) x).length) cLeaf.space) :
                        βˆƒ (poly : β„• β†’ β„•), PolynomiallyBounded poly ∧ (βˆ€ (x : P Γ— Logic.PL.CNF β„•), (normalizeDeclaredLeafCertificate hNOf cLeaf).space x ≀ poly ((Turing.MultiTapeTM.encPair encP encCNF) x).length) ∧ βˆ€ (x : P Γ— Logic.PL.CNF β„•), (normalizeDeclaredLeafCertificate hNOf cLeaf).time x ≀ cLeaf.time x + poly ((Turing.MultiTapeTM.encPair encP encCNF) x).length

                        Explicit certificate-level workspace and additive polynomial-time overhead bounds for normalizeDeclaredLeafCertificate.

                        source
                        theorem Cslib.Complexity.SparseCNFLeafCounter.computableInO_normalizeDeclaredLeaf {P : Type} {encP : P β†ͺ List Bool} {NOf : P β†’ β„•} (hNOf : Turing.MultiTapeTM.ComputableInPolyTime NOf encP Turing.MultiTapeTM.encUnary) {h : P Γ— Logic.PL.CNF β„• β†’ β„•} (cLeaf : GenericRAM.NativeCertificate h (Turing.MultiTapeTM.encPair encP encCNF) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (x : P Γ— Logic.PL.CNF β„•) => ((Turing.MultiTapeTM.encPair encP encCNF) x).length) cLeaf.space) :
                        βˆƒ (poly : β„• β†’ β„•), PolynomiallyBounded poly ∧ Turing.MultiTapeTM.ComputableInO (Logic.PL.CNF.normalizeDeclaredLeaf NOf h) (Turing.MultiTapeTM.encPair encP encCNF) Turing.MultiTapeTM.encNat (fun (x : P Γ— Logic.PL.CNF β„•) => cLeaf.time x + poly ((Turing.MultiTapeTM.encPair encP encCNF) x).length) fun (x : P Γ— Logic.PL.CNF β„•) => poly ((Turing.MultiTapeTM.encPair encP encCNF) x).length

                        Split ComputableInO time and polynomial-workspace bound for normalizeDeclaredLeaf.

                        source
                        noncomputable def Cslib.Complexity.SparseCNFLeafCounter.sparseCNFLeafCertificate {P : Type} {encP : P β†ͺ List Bool} {NOf BOf : P β†’ β„•} (k Nβ‚€ : β„•) (hNOf : Turing.MultiTapeTM.ComputableInPolyTime NOf encP Turing.MultiTapeTM.encUnary) (hBOf : Turing.MultiTapeTM.ComputableInPolyTime BOf encP Turing.MultiTapeTM.encUnary) {polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•} (cPoly : GenericRAM.NativeCertificate polyCounter (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat) :
                        GenericRAM.NativeCertificate (sparseCNFLeafCounter NOf BOf k Nβ‚€ polyCounter) (Turing.MultiTapeTM.encPair encP encCNF) Turing.MultiTapeTM.encNat

                        Native resource certificate for sparseCNFLeafCounter.

                        Instances For
                          source
                          theorem Cslib.Complexity.SparseCNFLeafCounter.polyBounded_sparseCNFLeafCertificate_space {P : Type} {encP : P β†ͺ List Bool} {NOf BOf : P β†’ β„•} (k Nβ‚€ : β„•) (hNOf : Turing.MultiTapeTM.ComputableInPolyTime NOf encP Turing.MultiTapeTM.encUnary) (hBOf : Turing.MultiTapeTM.ComputableInPolyTime BOf encP Turing.MultiTapeTM.encUnary) {polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•} (cPoly : GenericRAM.NativeCertificate polyCounter (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (y : β„• Γ— List (List (List β„•))) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) y).length) cPoly.space) :
                          Turing.MultiTapeTM.PolyBounded (fun (x : P Γ— Logic.PL.CNF β„•) => ((Turing.MultiTapeTM.encPair encP encCNF) x).length) (sparseCNFLeafCertificate k Nβ‚€ hNOf hBOf cPoly).space

                          Polynomial workspace of sparseCNFLeafCertificate.

                          source
                          theorem Cslib.Complexity.SparseCNFLeafCounter.exists_sparseCNFLeafCertificate_bounds {P : Type} {encP : P β†ͺ List Bool} {NOf BOf : P β†’ β„•} (k Nβ‚€ : β„•) (hNOf : Turing.MultiTapeTM.ComputableInPolyTime NOf encP Turing.MultiTapeTM.encUnary) (hBOf : Turing.MultiTapeTM.ComputableInPolyTime BOf encP Turing.MultiTapeTM.encUnary) {polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•} (cPoly : GenericRAM.NativeCertificate polyCounter (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (y : β„• Γ— List (List (List β„•))) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) y).length) cPoly.space) :
                          βˆƒ (poly : β„• β†’ β„•) (qInit : β„• β†’ β„•) (polySys : β„• β†’ β„•), PolynomiallyBounded poly ∧ PolynomiallyBounded qInit ∧ PolynomiallyBounded polySys ∧ (βˆ€ (x : P Γ— Logic.PL.CNF β„•), (sparseCNFLeafCertificate k Nβ‚€ hNOf hBOf cPoly).space x ≀ poly ((Turing.MultiTapeTM.encPair encP encCNF) x).length) ∧ βˆ€ (R : P Γ— Logic.PL.CNF β„• β†’ β„•), ValidPolyTimeBound encP NOf BOf k Nβ‚€ cPoly polySys R β†’ βˆ€ (x : P Γ— Logic.PL.CNF β„•), (sparseCNFLeafCertificate k Nβ‚€ hNOf hBOf cPoly).time x ≀ 2 * (sparseCNFTimeBound encP NOf BOf k Nβ‚€ poly qInit R x + 1)

                          Certificate-level workspace and split-time bounds for sparseCNFLeafCertificate.

                          source
                          theorem Cslib.Complexity.SparseCNFLeafCounter.computableInO_sparseCNFLeafCounter {P : Type} {encP : P β†ͺ List Bool} {NOf BOf : P β†’ β„•} (k Nβ‚€ : β„•) (hNOf : Turing.MultiTapeTM.ComputableInPolyTime NOf encP Turing.MultiTapeTM.encUnary) (hBOf : Turing.MultiTapeTM.ComputableInPolyTime BOf encP Turing.MultiTapeTM.encUnary) {polyCounter : β„• Γ— List (List (List β„•)) β†’ β„•} (cPoly : GenericRAM.NativeCertificate polyCounter (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat) (hSpace : Turing.MultiTapeTM.PolyBounded (fun (y : β„• Γ— List (List (List β„•))) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) y).length) cPoly.space) :
                          βˆƒ (poly : β„• β†’ β„•) (qInit : β„• β†’ β„•) (polySys : β„• β†’ β„•), PolynomiallyBounded poly ∧ PolynomiallyBounded qInit ∧ PolynomiallyBounded polySys ∧ βˆ€ (R : P Γ— Logic.PL.CNF β„• β†’ β„•), ValidPolyTimeBound encP NOf BOf k Nβ‚€ cPoly polySys R β†’ Turing.MultiTapeTM.ComputableInO (sparseCNFLeafCounter NOf BOf k Nβ‚€ polyCounter) (Turing.MultiTapeTM.encPair encP encCNF) Turing.MultiTapeTM.encNat (sparseCNFTimeBound encP NOf BOf k Nβ‚€ poly qInit R) fun (x : P Γ— Logic.PL.CNF β„•) => poly ((Turing.MultiTapeTM.encPair encP encCNF) x).length

                          Split ComputableInO time and polynomial-workspace bound for sparseCNFLeafCounter.