Heavy-branched sparse 𝔽₂ polynomial-system zero counter (§5.5, Theorem 2.2)

Uniform native heavy-branched sparse 𝔽₂ common-zero counter of §5.5 (Proof of Theorem 2.2, pp. 38–39) and §6.3 parity-system wrapper (p. 43) of OpenAI, The Exponential Time Hypothesis is False, parameterized over a Proposition 5.3 branch evaluator (branchEval).

• Encoded algorithms vs. specifications: the checkers, metrics, schedule builders, and counters (prepareBranchEvalInput, mkPaperSparseInput, toBranchInput, compileContextParityInput, guardedBranchSolver, countSparsePolySystem, countContextParity) run on encBranchEvalInput, encSparseSystemInput, and encPair encC (encList encBits) with ComputableInPolyTime and NativeCertificate bounds (guardedBranchCertificate, guardedBranchingCertificate, sparsePolyCounterCertificate, contextParityCertificate), whereas branchNeutralScope and maxReducedCost are unencoded mathematical specification definitions.
• Out-of-range and fallback conventions: scopeWidthOn n eq ignores variables ≥ n; both checkTopFeasible = false and checkBranchFeasible = false fall back to ExhaustiveCountFallback.countSystemExhaustive, evaluating indices ≥ n (resp. ≥ n') as false and matching HeavyBranchFold.rootCount unconditionally on all inputs.

Main definitions

• checkVarsLt, checkCanonicalMonomial, checkCanonicalEquation, checkCanonicalSystem, scopeWidthOn, sysMaxDegree, branchMaxFactorIncidence, branchMaxFactorWidth, branchAugmentedIncidence: canonicality checkers and neutral-augmented scope metrics.
• BranchEvalInput, encBranchEvalInput, prepareBranchEvalInput, checkBranchFeasible, guardedBranchSolver, guardedBranchCertificate: Proposition 5.3 branch bundle, exact guard, fallback-guarded branch solver, and NativeCertificate.
• SparseSystemInput, encSparseSystemInput, mkPaperSparseInput, checkTopFeasible, toBranchInput, guardedBranchingCertificate, countSparsePolySystem, sparsePolyCounterCertificate: top-level §5.5 heavy-branched counter and native certificates.
• compileContextParityInput, countContextParity, contextParityCertificate: §6.3 context-carrying CNF parity-system counter and NativeCertificate for GreedyContext.
• branchNeutralScope, maxReducedCost: unencoded neutral-scope and reduced-branch cost specs.

Main results

• sum_card_branchNeutralScope, varIncidence_branchNeutralScope_le, card_branchNeutralScope_le, branchAugmentedIncidence_le_mul, feasible_of_checkBranchFeasible, exists_replacementDesign_of_checkBranchFeasible, emod_ediv_design_eq_rootCount_of_checkBranchFeasible, exists_threshold_checkBranchFeasible_eq_true: neutral-scope bounds, ReplacementDesign bridge, cleared parity-quotient exactness, and eventual feasibility.
• computableInPolyTime_prepareBranchEvalInput, computableInPolyTime_checkBranchFeasible, computableInPolyTime_checkTopFeasible, computableInPolyTime_toBranchInput, computableInPolyTime_mkPaperSparseInput, computableInPolyTime_compileContextParityInput: ComputableInPolyTime certificates for schedule builders and guards.
• countSystemExhaustive_eq_rootCount, guardedBranchSolver_eq_rootCount, countSparsePolySystem_eq_rootCount, countSparsePolySystem_eq_commonZeroCount, checkTopFeasible_mkPaperSparseInput_of_le, reduced_branch_invariants, clog_pow_le_clog_pow_two_mul, countContextParity_eq_numPassing: unconditional exactness, commonZeroCount / numPassing bridges, and heavy-branching invariants.
• polyBounded_guardedBranchCertificate_space, exists_guardedBranchCertificate_time_le, polyBounded_sparsePolyCounterCertificate_space, sparsePolyCounterCertificate_time_le_of_feasible, exists_real_exp_bound_countSparsePolySystem, polyBounded_contextParityCertificate_space: polynomial workspace and fallback-absorbed time.

References

• OpenAI, The Exponential Time Hypothesis is False, §5.5 (pp. 38–39) & §6.3.

1. Computable Checkers, Branch Preparation, and Heavy-Branched Counters

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkVarsLt (n : ℕ) (sys : List (List (List ℕ))) : Bool

Check that every variable occurring in sys satisfies v < n.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkCanonicalMonomial (m : List ℕ) : Bool

Check that a monomial m : List ℕ is strictly increasing (IsCanonicalMonomial m).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkCanonicalEquation (eq : List (List ℕ)) : Bool

Check that eq has duplicate-free strictly increasing monomials (IsCanonicalEquation eq).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkCanonicalSystem (sys : List (List (List ℕ))) : Bool

Check that every equation in sys satisfies IsCanonicalEquation.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.scopeWidthOn (n : ℕ) (eq : List (List ℕ)) : ℕ

Number of variables < n occurring in at least one monomial of eq.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.sysMaxDegree (sys : List (List (List ℕ))) : ℕ

Maximum monomial degree (List.length) across all equations in sys (0 if empty).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.branchMaxFactorIncidence (n' : ℕ) (eqs' : List (List (List ℕ))) : ℕ

Maximum neutral-augmented factor incidence b = max_{v < n'} (varDegree v eqs') + 1 (§5.5).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.branchMaxFactorWidth (n' : ℕ) (eqs' : List (List (List ℕ))) : ℕ

Maximum neutral-augmented factor scope width w = max (max_{eq ∈ eqs'} |I'_{eq}|) 1 (§5.5).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.branchAugmentedIncidence (n' : ℕ) (eqs' : List (List (List ℕ))) : ℕ

Total neutral-augmented factor–variable incidence M' = ∑_{eq ∈ eqs'} |I'_{eq}| + n' (§5.5).

@[reducible, inline]

abbrev Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.BranchEvalInput : Type

Input bundle ((n', k'), (b, w, M', β), (r, Q, R, A₀), eqs') for Proposition 5.3 (§5.4–5.5).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.encBranchEvalInput : BranchEvalInput ↪ List Bool

Native encoding of BranchEvalInput ((n', k') unary, parameter quadruples binary).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.prepareBranchEvalInput (p : ℕ × List (List (List ℕ))) : BranchEvalInput

Assemble the Proposition 5.3 branch input from a reduced system (n', eqs') (§5.5).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkBranchFeasible (N₀_branch : ℕ) (p : ℕ × List (List (List ℕ))) : Bool

Per-branch exact feasibility guard (§5.5): N₀_branch ≤ n', canonical < n', schedule ok.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.guardedBranchSolver (N₀_branch : ℕ) (branchEval : BranchEvalInput → ℕ) (n' : ℕ) (eqs' : List (List (List ℕ))) : ℕ

Guarded per-branch solver (§5.5): runs branchEval when feasible, else exhaustive fallback.

@[reducible, inline]

abbrev Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.SparseSystemInput : Type

Top-level input (n, (k_deg, s_div, b₀), eqs) to the heavy-branched sparse 𝔽₂ counter.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.encSparseSystemInput : SparseSystemInput ↪ List Bool

Native encoding of SparseSystemInput (n and k_deg unary, s_div and b₀ binary).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.mkPaperSparseInput (n k_deg : ℕ) (eqs : List (List (List ℕ))) : SparseSystemInput

Construct the canonical §5.5 SparseSystemInput (n, (k_deg, s_div, b₀), eqs) (p. 38).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkTopFeasible (N₀_top : ℕ) (inp : SparseSystemInput) : Bool

Top-level §5.5 feasibility guard: N₀_top ≤ n, 1 ≤ s_div, canonical < n, |S| ≤ n/s.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.toBranchInput (inp : SparseSystemInput) : GenericRAM.HeavyBranchFold.BranchInput

Assemble HeavyBranchFold.BranchInput (n, heavyVarList n b₀ eqs, eqs) from inp.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.countSparsePolySystem (N₀_top N₀_branch : ℕ) (branchEval : BranchEvalInput → ℕ) (inp : SparseSystemInput) : ℕ

Uniform heavy-branched sparse 𝔽₂ polynomial-system zero counter (§5.5, Theorem 2.2).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.compileContextParityInput {C : Type} (k_deg : ℕ) (nOf sDivOf b₀Of : C → ℕ) (φOf : C → Logic.PL.CNF ℕ) (p : C × List (List Bool)) : SparseSystemInput

Compile (ctx, rows) into SparseSystemInput via compileParitySystemBounded k_deg (§6.3).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.countContextParity {C : Type} (N₀_top N₀_branch k_deg : ℕ) (nOf sDivOf b₀Of : C → ℕ) (φOf : C → Logic.PL.CNF ℕ) (branchEval : BranchEvalInput → ℕ) (p : C × List (List Bool)) : ℕ

Context-carrying parity-system counter (ctx, rows) ↦ ℕ matching GreedyContext (§6.3).

2. Branch Scope Invariants and ReplacementDesign Bridge

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.branchNeutralScope (n' : ℕ) (eqs' : List (List (List ℕ))) : Fin eqs'.length ⊕ Fin n' → Finset (Fin n')

Neutral-augmented scope family on Fin eqs'.length ⊕ Fin n' associated to (n', eqs').

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkVarsLt_eq_true_iff {n : ℕ} {sys : List (List (List ℕ))} : checkVarsLt n sys = true ↔ ∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkCanonicalMonomial_eq_true_iff {m : List ℕ} : checkCanonicalMonomial m = true ↔ IsCanonicalMonomial m

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkCanonicalEquation_eq_true_iff {eq : List (List ℕ)} : checkCanonicalEquation eq = true ↔ IsCanonicalEquation eq

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkCanonicalSystem_eq_true_iff {sys : List (List (List ℕ))} : checkCanonicalSystem sys = true ↔ ∀ eq ∈ sys, IsCanonicalEquation eq

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.countSystemExhaustive_eq_rootCount (n : ℕ) (sys : List (List (List ℕ))) : GenericRAM.ExhaustiveCountFallback.countSystemExhaustive (n, sys) = GenericRAM.HeavyBranchFold.rootCount n sys

Unconditional agreement between countSystemExhaustive and HeavyBranchFold.rootCount.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.scopeWidthOn_eq_length_equationVars {n : ℕ} {eq : List (List ℕ)} (hvars : ∀ m ∈ eq, ∀ v ∈ m, v < n) : scopeWidthOn n eq = (equationVars eq).length

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.card_equationScope_toFinsetEquation (n : ℕ) (eq : List (List ℕ)) : (BitString.equationScope (GenericRAM.HeavyBranchFold.toFinsetEquation n eq)).card = scopeWidthOn n eq

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.length_mem_le_sysMaxDegree {sys : List (List (List ℕ))} {eq : List (List ℕ)} (heq : eq ∈ sys) {m : List ℕ} (hm : m ∈ eq) : m.length ≤ sysMaxDegree sys

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.sysMaxDegree_le_iff {sys : List (List (List ℕ))} {k : ℕ} : sysMaxDegree sys ≤ k ↔ ∀ eq ∈ sys, ∀ m ∈ eq, m.length ≤ k

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.one_le_branchMaxFactorIncidence (n' : ℕ) (eqs' : List (List (List ℕ))) : 1 ≤ branchMaxFactorIncidence n' eqs'

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.one_le_branchMaxFactorWidth (n' : ℕ) (eqs' : List (List (List ℕ))) : 1 ≤ branchMaxFactorWidth n' eqs'

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.le_branchAugmentedIncidence (n' : ℕ) (eqs' : List (List (List ℕ))) : n' ≤ branchAugmentedIncidence n' eqs'

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.sum_card_branchNeutralScope (n' : ℕ) (eqs' : List (List (List ℕ))) : ∑ f : Fin eqs'.length ⊕ Fin n', (branchNeutralScope n' eqs' f).card = branchAugmentedIncidence n' eqs'

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.varIncidence_branchNeutralScope_le (n' : ℕ) (eqs' : List (List (List ℕ))) (v : Fin n') : {f : Fin eqs'.length ⊕ Fin n' | v ∈ branchNeutralScope n' eqs' f}.card ≤ branchMaxFactorIncidence n' eqs'

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.card_branchNeutralScope_le (n' : ℕ) (eqs' : List (List (List ℕ))) (f : Fin eqs'.length ⊕ Fin n') : (branchNeutralScope n' eqs' f).card ≤ branchMaxFactorWidth n' eqs'

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.branchAugmentedIncidence_le_mul (n' : ℕ) (eqs' : List (List (List ℕ))) : branchAugmentedIncidence n' eqs' ≤ branchMaxFactorIncidence n' eqs' * n'

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.feasible_of_checkBranchFeasible {N₀_branch n' : ℕ} {eqs' : List (List (List ℕ))} (h : checkBranchFeasible N₀_branch (n', eqs') = true) : have out := prepareBranchEvalInput (n', eqs'); N₀_branch ≤ n' ∧ (∀ eq ∈ eqs', IsCanonicalEquation eq) ∧ (∀ eq ∈ eqs', ∀ m ∈ eq, ∀ v ∈ m, v < n') ∧ ReplacementParams.Feasible out.2.1.2.2.2 n' out.2.1.1 out.2.1.2.1 out.2.1.2.2.1

Soundness of checkBranchFeasible: passing certifies N₀_branch ≤ n', canonical < n' equations, and ReplacementParams.Feasible at prepareBranchEvalInput.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.exists_replacementDesign_of_checkBranchFeasible {N₀_branch n' : ℕ} {eqs' : List (List (List ℕ))} (h : checkBranchFeasible N₀_branch (n', eqs') = true) : have out := prepareBranchEvalInput (n', eqs'); have s := out.2.2.1; Nonempty (LinearAlgebra.ReplacementDesign (branchNeutralScope n' eqs') s.2.1 s.1 s.2.2.2 s.2.2.1 (ReplacementParams.tauRat n'))

Passing checkBranchFeasible yields a Section 4 ReplacementDesign on branchNeutralScope.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.emod_ediv_design_eq_rootCount_of_checkBranchFeasible {N₀_branch n' ℓ : ℕ} {eqs' : List (List (List ℕ))} (h : checkBranchFeasible N₀_branch (n', eqs') = true) (hℓ : n' < ℓ) (D : LinearAlgebra.ReplacementDesign (branchNeutralScope n' eqs') (prepareBranchEvalInput (n', eqs')).2.2.1.2.1 (prepareBranchEvalInput (n', eqs')).2.2.1.1 (prepareBranchEvalInput (n', eqs')).2.2.1.2.2.2 (prepareBranchEvalInput (n', eqs')).2.2.1.2.2.1 (ReplacementParams.tauRat n')) : have out := prepareBranchEvalInput (n', eqs'); have P := fun (i : Fin eqs'.length) => GenericRAM.HeavyBranchFold.toFinsetEquation n' eqs'[i]; Polynomial.eval 0 (BitString.univariateClearedParityTruncatedSum Finset.univ P (↑(LinearAlgebra.commonDenom out.2.2.1.2.1 out.2.2.1.2.2.1)) out.1.2 ℓ (BitString.designReplacementScaledIntMap D Sum.inl)) / BitString.clearedProductDenom (↑(LinearAlgebra.commonDenom out.2.2.1.2.1 out.2.2.1.2.2.1)) out.1.2 ℓ eqs'.length % 2 ^ ℓ = ↑(GenericRAM.HeavyBranchFold.rootCount n' eqs')

Proposition 5.3 / §5.4–5.5 semantic bridge: when checkBranchFeasible holds, n' < ℓ, and D is any ReplacementDesign at prepareBranchEvalInput (n', eqs'), the cleared integer truncated parity quotient modulo 2 ^ ℓ equals rootCount n' eqs'.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.exists_threshold_checkBranchFeasible_eq_true (N₀_branch : ℕ) {β₀ : ℕ} (hβ₀ : 1 ≤ β₀) : ∃ (N₁ : ℕ), max N₀_branch 20 ≤ N₁ ∧ ∀ {n' : ℕ} {eqs' : List (List (List ℕ))}, N₁ ≤ n' → (∀ eq ∈ eqs', IsCanonicalEquation eq) → (∀ eq ∈ eqs', ∀ m ∈ eq, ∀ v ∈ m, v < n') → branchMaxFactorIncidence n' eqs' ≤ Nat.clog 2 n' ^ β₀ → branchMaxFactorWidth n' eqs' ≤ Nat.clog 2 n' ^ β₀ → have β := ParameterCheck.chooseBeta (Nat.clog 2 n') (branchMaxFactorIncidence n' eqs') (branchMaxFactorWidth n' eqs'); 1 ≤ β ∧ β ≤ β₀ ∧ checkBranchFeasible N₀_branch (n', eqs') = true

Uniform eventual passage of checkBranchFeasible (Lemma 4.8 & §5.5): for every 1 ≤ β₀, above a constant threshold N₁ ≥ max N₀_branch 20, every canonical < n' system with b, w ≤ (clog 2 n') ^ β₀ passes checkBranchFeasible with 1 ≤ β ≤ β₀.

3. Polynomial-Time Certificates for Checkers and Schedule Builders

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_checkVarsLt : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List (List (List ℕ))) => checkVarsLt p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_checkCanonicalSystem : Turing.MultiTapeTM.ComputableInPolyTime checkCanonicalSystem (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_scopeWidthOn : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List (List ℕ)) => scopeWidthOn p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_sysMaxDegree : Turing.MultiTapeTM.ComputableInPolyTime sysMaxDegree (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_branchMaxFactorIncidence : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List (List (List ℕ))) => branchMaxFactorIncidence p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_branchMaxFactorWidth : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List (List (List ℕ))) => branchMaxFactorWidth p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_branchAugmentedIncidence : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List (List (List ℕ))) => branchAugmentedIncidence p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_prepareBranchEvalInput : Turing.MultiTapeTM.ComputableInPolyTime prepareBranchEvalInput (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) encBranchEvalInput

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_checkBranchFeasible (N₀_branch : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (checkBranchFeasible N₀_branch) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_checkTopFeasible (N₀_top : ℕ) : Turing.MultiTapeTM.ComputableInPolyTime (checkTopFeasible N₀_top) encSparseSystemInput Turing.MultiTapeTM.encBool

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_toBranchInput : Turing.MultiTapeTM.ComputableInPolyTime toBranchInput encSparseSystemInput GenericRAM.HeavyBranchFold.encBranchInput

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_mkPaperSparseInput : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × List (List (List ℕ))) => mkPaperSparseInput p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) encSparseSystemInput

4. Semantic Exactness & Heavy-Branching Invariants (§5.5, pp. 38–39)

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.guardedBranchSolver_eq_rootCount {N₀_branch : ℕ} {branchEval : BranchEvalInput → ℕ} (hbranch : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (prepareBranchEvalInput (n', eqs')) = GenericRAM.HeavyBranchFold.rootCount n' eqs') (n' : ℕ) (eqs' : List (List (List ℕ))) : guardedBranchSolver N₀_branch branchEval n' eqs' = GenericRAM.HeavyBranchFold.rootCount n' eqs'

When branchEval is exact on feasible branches, guardedBranchSolver = rootCount always.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.guardedBranchSolver_le_two_pow {N₀_branch : ℕ} {branchEval : BranchEvalInput → ℕ} (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') (n' : ℕ) (eqs' : List (List (List ℕ))) : guardedBranchSolver N₀_branch branchEval n' eqs' ≤ 2 ^ n'

When branchEval ≤ 2 ^ n' on feasible inputs, guardedBranchSolver ≤ 2 ^ n' everywhere.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkTopFeasible_eq_true_iff {N₀_top : ℕ} {inp : SparseSystemInput} : checkTopFeasible N₀_top inp = true ↔ N₀_top ≤ inp.1 ∧ 1 ≤ inp.2.1.2.1 ∧ (∀ eq ∈ inp.2.2, ∀ m ∈ eq, ∀ v ∈ m, v < inp.1) ∧ (∀ eq ∈ inp.2.2, IsCanonicalEquation eq) ∧ (∀ eq ∈ inp.2.2, ∀ m ∈ eq, m.length ≤ inp.2.1.1) ∧ (GenericRAM.HeavyBranchFold.heavyVarList inp.1 inp.2.1.2.2 inp.2.2).length ≤ inp.1 / inp.2.1.2.1

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.countSparsePolySystem_eq_rootCount {N₀_top N₀_branch : ℕ} {branchEval : BranchEvalInput → ℕ} (hbranch : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (prepareBranchEvalInput (n', eqs')) = GenericRAM.HeavyBranchFold.rootCount n' eqs') (inp : SparseSystemInput) : countSparsePolySystem N₀_top N₀_branch branchEval inp = GenericRAM.HeavyBranchFold.rootCount inp.1 inp.2.2

Pointwise unconditional exactness (§5.5): countSparsePolySystem = rootCount always.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.countSparsePolySystem_eq_commonZeroCount {N₀_top N₀_branch : ℕ} {branchEval : BranchEvalInput → ℕ} (hbranch : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (prepareBranchEvalInput (n', eqs')) = GenericRAM.HeavyBranchFold.rootCount n' eqs') (inp : SparseSystemInput) (hcan : ∀ eq ∈ inp.2.2, IsCanonicalEquation eq) (hvars : ∀ eq ∈ inp.2.2, ∀ m ∈ eq, ∀ v ∈ m, v < inp.1) : countSparsePolySystem N₀_top N₀_branch branchEval inp = BitString.commonZeroCount Finset.univ fun (i : Fin inp.2.2.length) => GenericRAM.HeavyBranchFold.toFinsetEquation inp.1 inp.2.2[i]

Semantic bridge to Cslib.BitString.commonZeroCount (§5.5, Theorem 2.2) on Fin n.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.length_heavyVarList_le_div_of_incidence {n b₀ s_div : ℕ} {eqs : List (List (List ℕ))} (hb₀ : 1 ≤ b₀) (hs : 1 ≤ s_div) (hvars : ∀ eq ∈ eqs, ∀ m ∈ eq, ∀ v ∈ m, v < n) (hM : (List.map (scopeWidthOn n) eqs).sum * s_div ≤ b₀ * n) : (GenericRAM.HeavyBranchFold.heavyVarList n b₀ eqs).length ≤ n / s_div

Markov heavy-variable bound (§5.5, p. 38): M_eqs * s_div ≤ b₀ * n → |S| ≤ n / s_div.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkTopFeasible_mkPaperSparseInput_of_le {N₀_top n k_deg : ℕ} {eqs : List (List (List ℕ))} (hn : max N₀_top 2 ≤ n) (hcan : ∀ eq ∈ eqs, IsCanonicalEquation eq) (hvars : ∀ eq ∈ eqs, ∀ m ∈ eq, ∀ v ∈ m, v < n) (hdeg : ∀ eq ∈ eqs, ∀ m ∈ eq, m.length ≤ k_deg) : checkTopFeasible N₀_top (mkPaperSparseInput n k_deg eqs) = true

checkTopFeasible N₀_top (mkPaperSparseInput n k_deg eqs) holds for canonical < n systems.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.reduced_branch_invariants {N₀_top : ℕ} {inp : SparseSystemInput} {vals : List Bool} {n' : ℕ} {sys' : List (List (List ℕ))} (htop : checkTopFeasible N₀_top inp = true) (hs2 : 2 ≤ inp.2.1.2.1) (hred : GenericRAM.HeavyBranchFold.prepareBranch inp.1 (GenericRAM.HeavyBranchFold.heavyVarList inp.1 inp.2.1.2.2 inp.2.2) vals inp.2.2 = GenericRAM.HeavyBranchFold.BranchOutcome.reduced n' sys') : n' = inp.1 - (GenericRAM.HeavyBranchFold.heavyVarList inp.1 inp.2.1.2.2 inp.2.2).length ∧ inp.1 ≤ 2 * n' ∧ (∀ eq' ∈ sys', IsCanonicalEquation eq') ∧ (∀ eq' ∈ sys', ∀ m' ∈ eq', ∀ v' ∈ m', v' < n') ∧ (∀ eq' ∈ sys', ∀ m' ∈ eq', m'.length ≤ inp.2.1.1) ∧ branchMaxFactorIncidence n' sys' ≤ inp.2.1.2.2 + 1 ∧ branchMaxFactorWidth n' sys' ≤ branchMaxFactorWidth inp.1 inp.2.2

Invariants of .reduced n' sys' branches (n ≤ 2 * n', canonical < n', b ≤ b₀ + 1).

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.clog_pow_le_clog_pow_two_mul {n n' : ℕ} (hn' : 4 ≤ n') (hn : n ≤ 2 * n') (α : ℕ) : Nat.clog 2 n ^ α ≤ Nat.clog 2 n' ^ (2 * α)

Polylogarithmic transfer (§5.5): (clog 2 n) ^ α ≤ (clog 2 n') ^ (2 * α) for n ≤ 2 * n'.

5. Native Resource Certificates & Split Time / Polynomial-Space Bounds

noncomputable def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.guardedBranchCertificate {branchEval : BranchEvalInput → ℕ} (N₀_branch : ℕ) (cBranch : GenericRAM.NativeCertificate branchEval encBranchEvalInput Turing.MultiTapeTM.encNat) : GenericRAM.NativeCertificate (fun (p : ℕ × List (List (List ℕ))) => guardedBranchSolver N₀_branch branchEval p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) Turing.MultiTapeTM.encNat

Selected-branch NativeCertificate for guardedBranchSolver N₀_branch branchEval.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.polyBounded_guardedBranchCertificate_space {branchEval : BranchEvalInput → ℕ} (N₀_branch : ℕ) (cBranch : GenericRAM.NativeCertificate branchEval encBranchEvalInput Turing.MultiTapeTM.encNat) (hs : Turing.MultiTapeTM.PolyBounded (fun (x : BranchEvalInput) => (encBranchEvalInput x).length) cBranch.space) : Turing.MultiTapeTM.PolyBounded (fun (p : ℕ × List (List (List ℕ))) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) p).length) (guardedBranchCertificate N₀_branch cBranch).space

Polynomial workspace preservation for guardedBranchCertificate.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.exists_guardedBranchCertificate_time_le {branchEval : BranchEvalInput → ℕ} (N₀_branch N₁ : ℕ) (cBranch : GenericRAM.NativeCertificate branchEval encBranchEvalInput Turing.MultiTapeTM.encNat) : ∃ (C_br : ℕ) (d_br : ℕ), ∀ (p : ℕ × List (List (List ℕ))), (checkBranchFeasible N₀_branch p = false → p.1 < N₁) → (guardedBranchCertificate N₀_branch cBranch).time p ≤ (if checkBranchFeasible N₀_branch p = true then cBranch.time (prepareBranchEvalInput p) else 0) + C_br * (((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) p).length + 1) ^ d_br

Constant-threshold branch-fallback time bound when checkBranchFeasible = false → p.1 < N₁.

noncomputable def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.maxReducedCost (cost : ℕ × List (List (List ℕ)) → ℕ) (inp : GenericRAM.HeavyBranchFold.BranchInput) : ℕ

Maximum per-branch solver cost across all .reduced branches of inp : BranchInput.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.maxReducedCost_le {cost : ℕ × List (List (List ℕ)) → ℕ} {inp : GenericRAM.HeavyBranchFold.BranchInput} {B : ℕ} (hB : ∀ idx < 2 ^ inp.2.1.length, ∀ (n' : ℕ) (sys' : List (List (List ℕ))), GenericRAM.HeavyBranchFold.prepareBranch inp.1 inp.2.1 (BitString.lowBits inp.2.1.length idx) inp.2.2 = GenericRAM.HeavyBranchFold.BranchOutcome.reduced n' sys' → cost (n', sys') ≤ B) : maxReducedCost cost inp ≤ B

noncomputable def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.guardedBranchingCertificate {branchEval : BranchEvalInput → ℕ} (N₀_branch : ℕ) (cBranch : GenericRAM.NativeCertificate branchEval encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') : GenericRAM.NativeCertificate (GenericRAM.HeavyBranchFold.countByBranching (guardedBranchSolver N₀_branch branchEval)) GenericRAM.HeavyBranchFold.encBranchInput Turing.MultiTapeTM.encNat

Native certificate for HeavyBranchFold.countByBranching (guardedBranchSolver ...).

noncomputable def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.sparsePolyCounterCertificate {branchEval : BranchEvalInput → ℕ} (N₀_top N₀_branch : ℕ) (cBranch : GenericRAM.NativeCertificate branchEval encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') : GenericRAM.NativeCertificate (countSparsePolySystem N₀_top N₀_branch branchEval) encSparseSystemInput Turing.MultiTapeTM.encNat

Full native certificate for countSparsePolySystem N₀_top N₀_branch branchEval (§5.5).

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.polyBounded_sparsePolyCounterCertificate_space {branchEval : BranchEvalInput → ℕ} (N₀_top N₀_branch : ℕ) (cBranch : GenericRAM.NativeCertificate branchEval encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') (hs : Turing.MultiTapeTM.PolyBounded (fun (x : BranchEvalInput) => (encBranchEvalInput x).length) cBranch.space) : Turing.MultiTapeTM.PolyBounded (fun (inp : SparseSystemInput) => (encSparseSystemInput inp).length) (sparsePolyCounterCertificate N₀_top N₀_branch cBranch hbound).space

Independent polynomial workspace (§5.5, p. 39) for sparsePolyCounterCertificate.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.sparsePolyCounterCertificate_time_le_of_feasible {branchEval : BranchEvalInput → ℕ} (N₀_top N₀_branch : ℕ) (cBranch : GenericRAM.NativeCertificate branchEval encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') : ∃ (C_ov : ℕ) (d_ov : ℕ), ∀ (inp : SparseSystemInput) (R_branch : ℕ), checkTopFeasible N₀_top inp = true → (∀ idx < 2 ^ (GenericRAM.HeavyBranchFold.heavyVarList inp.1 inp.2.1.2.2 inp.2.2).length, ∀ (n' : ℕ) (sys' : List (List (List ℕ))), GenericRAM.HeavyBranchFold.prepareBranch inp.1 (GenericRAM.HeavyBranchFold.heavyVarList inp.1 inp.2.1.2.2 inp.2.2) (BitString.lowBits (GenericRAM.HeavyBranchFold.heavyVarList inp.1 inp.2.1.2.2 inp.2.2).length idx) inp.2.2 = GenericRAM.HeavyBranchFold.BranchOutcome.reduced n' sys' → (guardedBranchCertificate N₀_branch cBranch).time (n', sys') ≤ R_branch) → (sparsePolyCounterCertificate N₀_top N₀_branch cBranch hbound).time inp ≤ (2 ^ (GenericRAM.HeavyBranchFold.heavyVarList inp.1 inp.2.1.2.2 inp.2.2).length + 1) * (C_ov * ((encSparseSystemInput inp).length + 1) ^ d_ov + R_branch)

Feasible-regime multi-branch time bound (§5.5): ≤ (2 ^ |S| + 1) * (poly + R).

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.exists_real_exp_bound_countSparsePolySystem {branchEval : BranchEvalInput → ℕ} {ι : Type} {encI : ι ↪ List Bool} {mk : ι → SparseSystemInput} (N₀_top N₀_branch N_lim : ℕ) (cBranch : GenericRAM.NativeCertificate branchEval encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') (hs : Turing.MultiTapeTM.PolyBounded (fun (y : BranchEvalInput) => (encBranchEvalInput y).length) cBranch.space) (hmk : Turing.MultiTapeTM.ComputableInPolyTime mk encI encSparseSystemInput) {E : ι → ℝ} {C_f d_f : ℕ} (hE : ∀ (x : ι), 0 ≤ E x) (hthresh : ∀ (x : ι), checkTopFeasible N₀_top (mk x) = false → (mk x).1 < N_lim) (ht_fast : ∀ (x : ι), checkTopFeasible N₀_top (mk x) = true → ↑(((guardedBranchingCertificate N₀_branch cBranch hbound).comp (GenericRAM.NativeCertificate.ofPolyTime computableInPolyTime_toBranchInput)).time (mk x)) ≤ ↑C_f * (↑(encI x).length + 1) ^ d_f * 2 ^ E x) : ∃ (e : ℕ) (S : ι → ℕ), Turing.MultiTapeTM.PolyBounded (fun (x : ι) => (encI x).length) S ∧ Turing.MultiTapeTM.ComputableInO (fun (x : ι) => countSparsePolySystem N₀_top N₀_branch branchEval (mk x)) encI Turing.MultiTapeTM.encNat (fun (x : ι) => ((encI x).length + 1) ^ e * ⌈2 ^ E x⌉₊) S

Subexponential real-exponent constant absorption across families (§5.5, p. 39): absorbs bounded-n fallback regimes into O((|encI x| + 1) ^ e * ⌈(2 : ℝ) ^ E x⌉₊) time and poly space.

6. Context-Carrying §6.3 Parity-System Wrapper (countContextParity)

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_compileContextParityInput {C : Type} {encC : C ↪ List Bool} {nOf sDivOf b₀Of : C → ℕ} {φOf : C → Logic.PL.CNF ℕ} (k_deg : ℕ) (hn : Turing.MultiTapeTM.ComputableInPolyTime nOf encC Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime sDivOf encC Turing.MultiTapeTM.encNat) (hb : Turing.MultiTapeTM.ComputableInPolyTime b₀Of encC Turing.MultiTapeTM.encNat) (hφ : Turing.MultiTapeTM.ComputableInPolyTime φOf encC encCNF) : Turing.MultiTapeTM.ComputableInPolyTime (compileContextParityInput k_deg nOf sDivOf b₀Of φOf) (Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) encSparseSystemInput

compileContextParityInput is computable in polynomial time from poly-time projections.

noncomputable def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.contextParityCertificate {C : Type} {encC : C ↪ List Bool} {nOf sDivOf b₀Of : C → ℕ} {φOf : C → Logic.PL.CNF ℕ} {branchEval : BranchEvalInput → ℕ} (N₀_top N₀_branch k_deg : ℕ) (hn : Turing.MultiTapeTM.ComputableInPolyTime nOf encC Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime sDivOf encC Turing.MultiTapeTM.encNat) (hb : Turing.MultiTapeTM.ComputableInPolyTime b₀Of encC Turing.MultiTapeTM.encNat) (hφ : Turing.MultiTapeTM.ComputableInPolyTime φOf encC encCNF) (cBranch : GenericRAM.NativeCertificate branchEval encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') : GenericRAM.NativeCertificate (countContextParity N₀_top N₀_branch k_deg nOf sDivOf b₀Of φOf branchEval) (Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encNat

Uniform NativeCertificate for countContextParity matching GreedyContext (§6.3).

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.polyBounded_contextParityCertificate_space {C : Type} {encC : C ↪ List Bool} {nOf sDivOf b₀Of : C → ℕ} {φOf : C → Logic.PL.CNF ℕ} {branchEval : BranchEvalInput → ℕ} (N₀_top N₀_branch k_deg : ℕ) (hn : Turing.MultiTapeTM.ComputableInPolyTime nOf encC Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime sDivOf encC Turing.MultiTapeTM.encNat) (hb : Turing.MultiTapeTM.ComputableInPolyTime b₀Of encC Turing.MultiTapeTM.encNat) (hφ : Turing.MultiTapeTM.ComputableInPolyTime φOf encC encCNF) (cBranch : GenericRAM.NativeCertificate branchEval encBranchEvalInput Turing.MultiTapeTM.encNat) (hbound : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (prepareBranchEvalInput (n', eqs')) ≤ 2 ^ n') (hs_br : Turing.MultiTapeTM.PolyBounded (fun (x : BranchEvalInput) => (encBranchEvalInput x).length) cBranch.space) : Turing.MultiTapeTM.PolyBounded (fun (p : C × List (List Bool)) => ((Turing.MultiTapeTM.encPair encC (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) p).length) (contextParityCertificate N₀_top N₀_branch k_deg hn hs hb hφ cBranch hbound).space

Polynomial workspace preservation for contextParityCertificate (§6.3).

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.countContextParity_eq_numPassing {C : Type} {nOf sDivOf b₀Of : C → ℕ} {φOf : C → Logic.PL.CNF ℕ} {branchEval : BranchEvalInput → ℕ} {N₀_top N₀_branch k_deg : ℕ} (hbranch : ∀ (n' : ℕ) (eqs' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', eqs') = true → branchEval (prepareBranchEvalInput (n', eqs')) = GenericRAM.HeavyBranchFold.rootCount n' eqs') (ctx : C) (φFin : Logic.PL.CNF (Fin (nOf ctx))) (rows : List (List Bool)) (hφ_eq : φOf ctx = List.map (List.map fun (l : Logic.PL.Literal (Fin (nOf ctx))) => (↑l.1, l.2)) φFin) (hk : ∀ c ∈ φFin, List.length c ≤ k_deg) : countContextParity N₀_top N₀_branch k_deg nOf sDivOf b₀Of φOf branchEval (ctx, rows) = BitString.numPassing φFin.violations (List.map (BitString.ofList (List.length φFin)) rows)

Exact agreement with numPassing (§6.3, Lemma 6.2) on Fin (nOf ctx).