Heavy-branched sparse k-CNF leaf model counter (BranchedSparseCNFCounter)

Connects the heavy-branched sparse 𝔽₂ polynomial-system zero counter countSparsePolySystem (§5.5, Theorem 2.2, pp. 38–39) to sparseCNFDeclaredCounter / normalizeDeclaredLeaf (§6.3, p. 43) at the Proposition 6.4 leaf schedule (§6.4, pp. 43–44) of OpenAI, The Exponential Time Hypothesis is False, parameterized solely over branchEval : BranchEvalInput → ℕ:

• Encoded procedures vs. specification: leafDensityRatio (encPair encUnit encUnary → encUnary) and branchedPolyCounter, branchedSparseCNFDeclaredCounter, and branchedSparseCNFLeafCounter carry uniform NativeCertificate witnesses with global PolyBounded workspace; BranchPolylogTimeBound states the unencoded Proposition 5.3 runtime hypothesis on cBranch.
• Total fallback & exactness: valid dense formulas (leafDensityRatio k N * N < ψ.length, including [[]] at N = 0) dispatch to countCNFExhaustive, sparse formulas dispatch to sparseCNFDeclaredCounter backed by branchedPolyCounter, invalid inputs (validDeclaredInput = false) return 0. Assuming exact feasible-branch evaluation, exactness holds on all width-≤ k supported CNFs without a density restriction.

Main definitions

• leafSearchDivisor, leafThresholdBase, leafOccBound, leafDensityRatio
• branchedPolyCounter, branchedSparseCNFDeclaredCounter, branchedSparseCNFLeafCounter
• branchedPolyCertificate, branchedSparseCNFDeclaredCertificate, branchedSparseCNFLeafCertificate, BranchPolylogTimeBound

Main results

• leafOccBound_eq_sum, leafOccBound_eq_occBound, leafDensityRatio_eq_prop64LeafClauseRatio, exists_leafDensityRatio_le_mul_clog_pow, computableInPolyTime_leafDensityRatio
• branchedSparseCNFDeclaredCounter_le_two_pow, branchedSparseCNFLeafCounter_le_two_pow_numVars
• branchedPolyCounter_eq_commonZeroCount, branchedSparseCNFDeclaredCounter_eq_modelCountOn, branchedSparseCNFLeafCounter_eq_modelCount
• polyBounded_branchedSparseCNFDeclaredCertificate_space, polyBounded_branchedSparseCNFLeafCertificate_space
• exists_threshold_branchedSparseCNF_time_bound, exists_branchedSparseCNF_time_bound

References

• OpenAI, The Exponential Time Hypothesis is False, §5.4 (Proposition 5.3, pp. 37–38), §5.5 (Theorem 2.2, pp. 38–39), §6.3 (eq. (6.4), p. 43), §6.4 (Proposition 6.4, pp. 43–44).

1. Proposition 6.4 / Section 6.3 Leaf Parameters and Total Counters

def Cslib.Complexity.BranchedSparseCNFCounter.leafSearchDivisor (N : ℕ) : ℕ

Sparsification search divisor max 1 ⌊√⌈log₂ N⌉ / ⌈log₂ ⌈log₂ N⌉⌉²⌋ (§6.4, Proposition 6.4).

def Cslib.Complexity.BranchedSparseCNFCounter.leafThresholdBase (k N : ℕ) : ℕ

Appendix A.3 dyadic threshold base countingThresholdBase (max 2 k) (leafSearchDivisor N).

def Cslib.Complexity.BranchedSparseCNFCounter.leafOccBound (k N : ℕ) : ℕ

Sparse leaf clause-density sum 2 * ∑_{j < max 2 k} (leafThresholdBase k N) ^ j (§6.4).

def Cslib.Complexity.BranchedSparseCNFCounter.leafDensityRatio (k N : ℕ) : ℕ

Promised sparse leaf clause-to-variable ratio leafOccBound k N + 1 (§6.3–6.4).

def Cslib.Complexity.BranchedSparseCNFCounter.branchedPolyCounter (k N₀_top N₀_branch : ℕ) (branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ) (y : ℕ × List (List (List ℕ))) : ℕ

Heavy-branched sparse 𝔽₂ polynomial-system zero counter at mkPaperSparseInput y.1 k y.2.

def Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFDeclaredCounter (k N₀_leaf N₀_top N₀_branch : ℕ) (branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ) (x : (Unit × ℕ) × Logic.PL.CNF ℕ) : ℕ

Total declared-range sparse k-CNF leaf model counter (§6.3–6.4): dispatches valid dense formulas (leafDensityRatio k N * N < ψ.length, including [[]] at N = 0) to countCNFExhaustive and sparse formulas (ψ.length ≤ leafDensityRatio k N * N) to sparseCNFDeclaredCounter backed by branchedPolyCounter.

def Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFLeafCounter (k N₀_leaf N₀_top N₀_branch : ℕ) (branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ) (x : (Unit × ℕ) × Logic.PL.CNF ℕ) : ℕ

Total normalized occurring-support sparse k-CNF leaf model counter (§6.3–6.4).

2. Leaf Parameter Bounds & Unary ComputableInPolyTime Certificate

theorem Cslib.Complexity.BranchedSparseCNFCounter.leafOccBound_eq_sum (k N : ℕ) : leafOccBound k N = 2 * ∑ j ∈ Finset.range (max 2 k), leafThresholdBase k N ^ j

leafOccBound k N equals 2 * ∑ j ∈ Finset.range (max 2 k), leafThresholdBase k N ^ j.

theorem Cslib.Complexity.BranchedSparseCNFCounter.leafOccBound_eq_occBound (k N : ℕ) : leafOccBound k N = CountingSparsify.occBound (max 2 k) (leafThresholdBase k N)

leafOccBound k N agrees with CountingSparsify.occBound (max 2 k) (leafThresholdBase k N).

theorem Cslib.Complexity.BranchedSparseCNFCounter.leafDensityRatio_eq_prop64LeafClauseRatio {k N : ℕ} (hs : 1 ≤ SubexponentialSAT.ReplacementParams.numGroups N) : leafDensityRatio k N = Logic.PL.CNF.prop64LeafClauseRatio (max 2 k) N

When 1 ≤ ReplacementParams.numGroups N, leafDensityRatio equals prop64LeafClauseRatio.

theorem Cslib.Complexity.BranchedSparseCNFCounter.leafOccBound_mul_succ_le_leafDensityRatio_mul {k N : ℕ} (hN : 1 ≤ N) : leafOccBound k N * N + 1 ≤ leafDensityRatio k N * N

For 1 ≤ N, leafOccBound k N * N + 1 ≤ leafDensityRatio k N * N.

theorem Cslib.Complexity.BranchedSparseCNFCounter.exists_leafDensityRatio_le_mul_clog_pow (k : ℕ) : ∃ (C_B : ℕ), ∀ (N : ℕ), 2 ≤ N → leafDensityRatio k N ≤ C_B * Nat.clog 2 N ^ (2 * (max 2 k - 1))

Polylogarithmic leaf clause-density bound (§6.4, Proposition 6.4, p. 44): ∃ C_B, ∀ N ≥ 2, leafDensityRatio k N ≤ C_B * (Nat.clog 2 N) ^ (2 * (max 2 k - 1)).

theorem Cslib.Complexity.BranchedSparseCNFCounter.computableInPolyTime_leafDensityRatio (k : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : Unit × ℕ) => leafDensityRatio k p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.Universal.encUnit Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary

Unary ComputableInPolyTime certificate for leafDensityRatio on (Unit × ℕ) (encPair encUnit encUnary → encUnary), clamping the binary countingThresholdBase schedule by its polynomial unary upper bound via ComputableInPolyTime.binary_min_unary'.

3. Unconditional Output Caps & Semantic Exactness Across All Width-≤ k CNFs

theorem Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFDeclaredCounter_le_two_pow (k N₀_leaf N₀_top N₀_branch : ℕ) (branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ) (x : (Unit × ℕ) × Logic.PL.CNF ℕ) : branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval x ≤ 2 ^ x.1.2

Unconditional declared-range output cap: branchedSparseCNFDeclaredCounter ≤ 2 ^ x.1.2.

theorem Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFLeafCounter_le_two_pow_numVars (k N₀_leaf N₀_top N₀_branch : ℕ) (branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ) (x : (Unit × ℕ) × Logic.PL.CNF ℕ) : branchedSparseCNFLeafCounter k N₀_leaf N₀_top N₀_branch branchEval x ≤ 2 ^ x.2.numVars

Unconditional occurring-support output cap: branchedSparseCNFLeafCounter ≤ 2 ^ x.2.numVars.

theorem Cslib.Complexity.BranchedSparseCNFCounter.branchedPolyCounter_eq_commonZeroCount {k N₀_top N₀_branch N maxEqs maxTerms : ℕ} {branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ} (hbranch : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), SubexponentialSAT.SparsePolyCounter.checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (SubexponentialSAT.SparsePolyCounter.prepareBranchEvalInput (n', eqs')) = GenericRAM.HeavyBranchFold.rootCount n' eqs') {sys : List (List (List ℕ))} (hsys : SparseCNFLeafCounter.IsCompiledSparseSystem k N maxEqs maxTerms sys) : branchedPolyCounter k N₀_top N₀_branch branchEval (N, sys) = BitString.commonZeroCount Finset.univ fun (i : Fin sys.length) => GenericRAM.ExhaustiveCountFallback.equationToFinset N sys[i]

Semantic bridge for branchedPolyCounter (§5.5 & §6.3): under exact feasible branch evaluation, branchedPolyCounter equals commonZeroCount on IsCompiledSparseSystem.

theorem Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFDeclaredCounter_eq_modelCountOn {k N₀_leaf N₀_top N₀_branch : ℕ} {branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ} (hbranch : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), SubexponentialSAT.SparsePolyCounter.checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (SubexponentialSAT.SparsePolyCounter.prepareBranchEvalInput (n', eqs')) = GenericRAM.HeavyBranchFold.rootCount n' eqs') (c : Unit) (N : ℕ) (ψ : Logic.PL.CNF ℕ) (hw : ∀ cl ∈ ψ, List.length cl ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range N) : branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval ((c, N), ψ) = ψ.modelCountOn (Finset.range N)

Exactness of branchedSparseCNFDeclaredCounter without a density restriction (§5.5, §6.3, §6.4), assuming exact feasible-branch evaluation, on all width-≤ k formulas ψ with ψ.vars.toFinset ⊆ Finset.range N.

theorem Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFLeafCounter_eq_modelCount {k N₀_leaf N₀_top N₀_branch : ℕ} {branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ} (hbranch : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), SubexponentialSAT.SparsePolyCounter.checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (SubexponentialSAT.SparsePolyCounter.prepareBranchEvalInput (n', eqs')) = GenericRAM.HeavyBranchFold.rootCount n' eqs') (c : Unit) (N : ℕ) (ψ : Logic.PL.CNF ℕ) (hw : ∀ cl ∈ ψ, List.length cl ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range N) : branchedSparseCNFLeafCounter k N₀_leaf N₀_top N₀_branch branchEval ((c, N), ψ) = ψ.modelCount

Exactness of branchedSparseCNFLeafCounter without a density restriction (§5.5, §6.3, §6.4), assuming exact feasible-branch evaluation, on all width-≤ k formulas ψ with ψ.vars.toFinset ⊆ Finset.range N.

theorem Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFDeclaredCounter_exhaustive_eq_modelCountOn (k N₀_leaf N₀_top N₀_branch : ℕ) (c : Unit) (N : ℕ) (ψ : Logic.PL.CNF ℕ) (hw : ∀ cl ∈ ψ, List.length cl ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range N) : branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch (fun (inp : SubexponentialSAT.SparsePolyCounter.BranchEvalInput) => GenericRAM.ExhaustiveCountFallback.countSystemExhaustive (inp.1.1, inp.2.2.2)) ((c, N), ψ) = ψ.modelCountOn (Finset.range N)

Concrete instantiation of branchedSparseCNFDeclaredCounter_eq_modelCountOn with countSystemExhaustive.

theorem Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFLeafCounter_exhaustive_eq_modelCount (k N₀_leaf N₀_top N₀_branch : ℕ) (c : Unit) (N : ℕ) (ψ : Logic.PL.CNF ℕ) (hw : ∀ cl ∈ ψ, List.length cl ≤ k) (hsub : ψ.vars.toFinset ⊆ Finset.range N) : branchedSparseCNFLeafCounter k N₀_leaf N₀_top N₀_branch (fun (inp : SubexponentialSAT.SparsePolyCounter.BranchEvalInput) => GenericRAM.ExhaustiveCountFallback.countSystemExhaustive (inp.1.1, inp.2.2.2)) ((c, N), ψ) = ψ.modelCount

Concrete instantiation of branchedSparseCNFLeafCounter_eq_modelCount with countSystemExhaustive.

4. Uniform Native Certificates & Global PolyBounded Workspace

noncomputable def Cslib.Complexity.BranchedSparseCNFCounter.branchedPolyCertificate (k N₀_top N₀_branch : ℕ) {branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ} (cBranch : GenericRAM.NativeCertificate branchEval SubexponentialSAT.SparsePolyCounter.encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), SubexponentialSAT.SparsePolyCounter.checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (SubexponentialSAT.SparsePolyCounter.prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') : GenericRAM.NativeCertificate (branchedPolyCounter k N₀_top N₀_branch branchEval) (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 branchedPolyCounter (§5.5).

theorem Cslib.Complexity.BranchedSparseCNFCounter.polyBounded_branchedPolyCertificate_space (k N₀_top N₀_branch : ℕ) {branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ} (cBranch : GenericRAM.NativeCertificate branchEval SubexponentialSAT.SparsePolyCounter.encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), SubexponentialSAT.SparsePolyCounter.checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (SubexponentialSAT.SparsePolyCounter.prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') (hs_br : Turing.MultiTapeTM.PolyBounded (fun (x : SubexponentialSAT.SparsePolyCounter.BranchEvalInput) => (SubexponentialSAT.SparsePolyCounter.encBranchEvalInput x).length) cBranch.space) : 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) (branchedPolyCertificate k N₀_top N₀_branch cBranch hbound).space

Polynomial workspace preservation for branchedPolyCertificate.

noncomputable def Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFDeclaredCertificate (k N₀_leaf N₀_top N₀_branch : ℕ) {branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ} (cBranch : GenericRAM.NativeCertificate branchEval SubexponentialSAT.SparsePolyCounter.encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), SubexponentialSAT.SparsePolyCounter.checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (SubexponentialSAT.SparsePolyCounter.prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') : GenericRAM.NativeCertificate (branchedSparseCNFDeclaredCounter k N₀_leaf N₀_top N₀_branch branchEval) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.Universal.encUnit Turing.MultiTapeTM.encUnary) encCNF) Turing.MultiTapeTM.encNat

Uniform NativeCertificate for branchedSparseCNFDeclaredCounter (§6.3–6.4).

noncomputable def Cslib.Complexity.BranchedSparseCNFCounter.branchedSparseCNFLeafCertificate (k N₀_leaf N₀_top N₀_branch : ℕ) {branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ} (cBranch : GenericRAM.NativeCertificate branchEval SubexponentialSAT.SparsePolyCounter.encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), SubexponentialSAT.SparsePolyCounter.checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (SubexponentialSAT.SparsePolyCounter.prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') : GenericRAM.NativeCertificate (branchedSparseCNFLeafCounter k N₀_leaf N₀_top N₀_branch branchEval) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.Universal.encUnit Turing.MultiTapeTM.encUnary) encCNF) Turing.MultiTapeTM.encNat

Uniform NativeCertificate for branchedSparseCNFLeafCounter (§6.3–6.4).

theorem Cslib.Complexity.BranchedSparseCNFCounter.polyBounded_branchedSparseCNFDeclaredCertificate_space (k N₀_leaf N₀_top N₀_branch : ℕ) {branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ} (cBranch : GenericRAM.NativeCertificate branchEval SubexponentialSAT.SparsePolyCounter.encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), SubexponentialSAT.SparsePolyCounter.checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (SubexponentialSAT.SparsePolyCounter.prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') (hs_br : Turing.MultiTapeTM.PolyBounded (fun (x : SubexponentialSAT.SparsePolyCounter.BranchEvalInput) => (SubexponentialSAT.SparsePolyCounter.encBranchEvalInput x).length) cBranch.space) : Turing.MultiTapeTM.PolyBounded (fun (x : (Unit × ℕ) × Logic.PL.CNF ℕ) => ((Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.Universal.encUnit Turing.MultiTapeTM.encUnary) encCNF) x).length) (branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound).space

Global PolyBounded workspace for branchedSparseCNFDeclaredCertificate.

theorem Cslib.Complexity.BranchedSparseCNFCounter.polyBounded_branchedSparseCNFLeafCertificate_space (k N₀_leaf N₀_top N₀_branch : ℕ) {branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ} (cBranch : GenericRAM.NativeCertificate branchEval SubexponentialSAT.SparsePolyCounter.encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), SubexponentialSAT.SparsePolyCounter.checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (SubexponentialSAT.SparsePolyCounter.prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') (hs_br : Turing.MultiTapeTM.PolyBounded (fun (x : SubexponentialSAT.SparsePolyCounter.BranchEvalInput) => (SubexponentialSAT.SparsePolyCounter.encBranchEvalInput x).length) cBranch.space) : Turing.MultiTapeTM.PolyBounded (fun (x : (Unit × ℕ) × Logic.PL.CNF ℕ) => ((Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.Universal.encUnit Turing.MultiTapeTM.encUnary) encCNF) x).length) (branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound).space

Global PolyBounded workspace for branchedSparseCNFLeafCertificate.

5. Fast-Regime 2 ^ {O_k(interpolationScale N)} Runtime Envelope (§5.5, §6.3, §6.4)

def Cslib.Complexity.BranchedSparseCNFCounter.BranchPolylogTimeBound (N₀_branch : ℕ) {branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ} (cBranch : GenericRAM.NativeCertificate branchEval SubexponentialSAT.SparsePolyCounter.encBranchEvalInput Turing.MultiTapeTM.encNat) : Prop

Proposition 5.3 per-branch subexponential runtime hypothesis (BranchPolylogTimeBound): for every degree cap k_deg, polylogarithmic exponent β, and prefactor C_inc, above a constant threshold N₀_br, every feasible reduced branch (n', sys') with sysMaxDegree sys' ≤ k_deg, sys'.length ≤ C_inc * n', and neutral-augmented incidence and scope width ≤ C_inc * ⌈log₂ n'⌉ ^ β runs in at most C_br * (|enc (n', sys')| + 1) ^ d_br * 2 ^ (A_br * interpolationScale n') steps.

theorem Cslib.Complexity.BranchedSparseCNFCounter.exists_threshold_branchedSparseCNF_time_bound (k N₀_top N₀_branch : ℕ) {branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ} (cBranch : GenericRAM.NativeCertificate branchEval SubexponentialSAT.SparsePolyCounter.encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), SubexponentialSAT.SparsePolyCounter.checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (SubexponentialSAT.SparsePolyCounter.prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') (hs_br : Turing.MultiTapeTM.PolyBounded (fun (x : SubexponentialSAT.SparsePolyCounter.BranchEvalInput) => (SubexponentialSAT.SparsePolyCounter.encBranchEvalInput x).length) cBranch.space) (hbr_time : BranchPolylogTimeBound N₀_branch cBranch) : ∃ (N_min : ℕ), 16384 ≤ N_min ∧ ∀ (N₀_leaf : ℕ), N_min ≤ N₀_leaf → ∃ (C_t : ℕ) (d_t : ℕ) (A_t : ℕ), 1 ≤ A_t ∧ ∀ (x : (Unit × ℕ) × Logic.PL.CNF ℕ), List.length x.2 ≤ leafOccBound k x.1.2 * x.1.2 + 1 → ↑((branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound).time x) ≤ ↑C_t * (↑((Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.Universal.encUnit Turing.MultiTapeTM.encUnary) encCNF) x).length + 1) ^ d_t * 2 ^ (↑A_t * SubexponentialSAT.interpolationScale x.1.2) ∧ ↑((branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound).time x) ≤ ↑C_t * (↑((Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.Universal.encUnit Turing.MultiTapeTM.encUnary) encCNF) x).length + 1) ^ d_t * 2 ^ (↑A_t * SubexponentialSAT.interpolationScale x.1.2)

Threshold-parametric fast-regime 2 ^ {O_k(interpolationScale N)} runtime bound (§5.5, §6.3 eq. (6.4), §6.4 Proposition 6.4): above N_min ≥ 16384, both leaf certificates run in C_t * (|enc x| + 1) ^ d_t * 2 ^ (A_t * interpolationScale x.1.2) steps on x.2.length ≤ leafOccBound k x.1.2 * x.1.2 + 1 (for all N : ℕ, including N = 0).

theorem Cslib.Complexity.BranchedSparseCNFCounter.exists_branchedSparseCNF_time_bound (k N₀_branch : ℕ) {branchEval : SubexponentialSAT.SparsePolyCounter.BranchEvalInput → ℕ} (cBranch : GenericRAM.NativeCertificate branchEval SubexponentialSAT.SparsePolyCounter.encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), SubexponentialSAT.SparsePolyCounter.checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (SubexponentialSAT.SparsePolyCounter.prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') (hs_br : Turing.MultiTapeTM.PolyBounded (fun (x : SubexponentialSAT.SparsePolyCounter.BranchEvalInput) => (SubexponentialSAT.SparsePolyCounter.encBranchEvalInput x).length) cBranch.space) (hbr_time : BranchPolylogTimeBound N₀_branch cBranch) : ∃ (N₀_leaf : ℕ) (N₀_top : ℕ) (C_t : ℕ) (d_t : ℕ) (A_t : ℕ), 1 ≤ A_t ∧ ∀ (x : (Unit × ℕ) × Logic.PL.CNF ℕ), List.length x.2 ≤ leafOccBound k x.1.2 * x.1.2 + 1 → ↑((branchedSparseCNFDeclaredCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound).time x) ≤ ↑C_t * (↑((Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.Universal.encUnit Turing.MultiTapeTM.encUnary) encCNF) x).length + 1) ^ d_t * 2 ^ (↑A_t * SubexponentialSAT.interpolationScale x.1.2) ∧ ↑((branchedSparseCNFLeafCertificate k N₀_leaf N₀_top N₀_branch cBranch hbound).time x) ≤ ↑C_t * (↑((Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.Universal.encUnit Turing.MultiTapeTM.encUnary) encCNF) x).length + 1) ^ d_t * 2 ^ (↑A_t * SubexponentialSAT.interpolationScale x.1.2)

Existential fast-regime 2 ^ {O_k(interpolationScale N)} runtime bound (§5.5, §6.3 eq. (6.4), §6.4 Proposition 6.4): under BranchPolylogTimeBound N₀_branch cBranch and polynomial branch workspace hs_br, there exist N₀_leaf N₀_top C_t d_t A_t : ℕ (1 ≤ A_t) bounding both leaf certificates across all x = ((c, N), ψ) satisfying ψ.length ≤ leafOccBound k N * N + 1 (including N = 0).