Heavy-variable branching and streaming common-zero accumulation

Implements the heavy-variable branching reduction and space-efficient streaming accumulator from §5.5 (Proof of Theorem 2.2, pp. 38–39) of OpenAI, The Exponential Time Hypothesis is False over SparsePolyCompile, bridged to SparseEquations and BooleanFold.

Main definitions

• extendAssignment, rootCount, toFinsetEquation, heavyVarList, relabelFreeVar, freeVarEquiv: common-zero count N(P), heavy-variable filter, and dense [n] \ S ≃ [n - |S|].
• substituteEquation, relabelEquation, BranchOutcome, prepareBranch, branchRootCount, branchCountOracle: simultaneous (S, vals) substitution, short-circuiting, and oracle dispatch.
• BranchInput, encBranchInput, branchBody, streamBranches, countByBranching, branchCountCertificate, branchBodyCertificate, certificate, countCertificate, stepOverhead: streaming BooleanFold combinator and native time/space certificates.

Main results

• rootCount_eq_commonZeroCount, toFinset_heavyVarList_eq_heavyVars, length_heavyVarList_le_div, prepareBranch_reduced_canonical, prepareBranch_reduced_degree_le, prepareBranch_reduced_length_le, prepareBranch_reduced_varDegree_le, length_enc_reduced_le.
• branchRootCount_prepareBranch, sum_branch_count_eq_rootCount, streamBranches_correct, countByBranching_eq_rootCount, runPrefix_sum_le_two_pow, computableInPolyTime_prepareBranch, streamBranches_computableInO, countByBranching_computableInO, polyBounded_branchWorkspace.

References

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

1. Common-Zero Counting, SparseEquations Bridges, and heavyVarList

def Cslib.GenericRAM.HeavyBranchFold.extendAssignment {n : ℕ} (σ : BitString n) (i : ℕ) : Bool

Extend a finite assignment σ : BitString n (Fin n → Bool) by false outside [n].

def Cslib.GenericRAM.HeavyBranchFold.rootCount (n : ℕ) (sys : List (List (List ℕ))) : ℕ

Exact number of common zeros N(P) of sys over BitString n (Fin n → Bool).

def Cslib.GenericRAM.HeavyBranchFold.toFinsetEquation (n : ℕ) (eq : List (List ℕ)) : Finset (Finset (Fin n))

Lift a sparse 𝔽₂ equation eq : List (List ℕ) to Finset (Finset (Fin n)).

def Cslib.GenericRAM.HeavyBranchFold.heavyVarList (n b₀ : ℕ) (sys : List (List (List ℕ))) : List ℕ

Sorted list of heavy variables v < n with b₀ < varDegree v sys (§5.5 of [OAI26c]).

@[simp]

theorem Cslib.GenericRAM.HeavyBranchFold.evalMonomialList_contradiction (σ : ℕ → Bool) : Complexity.evalMonomialList [[]] σ = true

@[simp]

theorem Cslib.GenericRAM.HeavyBranchFold.evalSystem_nil (σ : ℕ → Bool) : Complexity.evalSystem [] σ = true

@[simp]

theorem Cslib.GenericRAM.HeavyBranchFold.extendAssignment_coe {n : ℕ} (σ : BitString n) (i : Fin n) : extendAssignment σ ↑i = σ i

theorem Cslib.GenericRAM.HeavyBranchFold.rootCount_le_two_pow (n : ℕ) (sys : List (List (List ℕ))) : rootCount n sys ≤ 2 ^ n

theorem Cslib.GenericRAM.HeavyBranchFold.rootCount_eq_commonZeroCount {n : ℕ} {sys : List (List (List ℕ))} (hcan : ∀ eq ∈ sys, Complexity.IsCanonicalEquation eq) (hvars : ∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n) : rootCount n sys = BitString.commonZeroCount Finset.univ fun (i : Fin sys.length) => toFinsetEquation n sys[i]

Specification bridge to SparseEquations.commonZeroCount: for any canonical sparse 𝔽₂ system sys on < n variables, rootCount n sys agrees with Cslib.BitString.commonZeroCount.

theorem Cslib.GenericRAM.HeavyBranchFold.pairwise_lt_heavyVarList (n b₀ : ℕ) (sys : List (List (List ℕ))) : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (heavyVarList n b₀ sys)

theorem Cslib.GenericRAM.HeavyBranchFold.nodup_heavyVarList (n b₀ : ℕ) (sys : List (List (List ℕ))) : (heavyVarList n b₀ sys).Nodup

@[simp]

theorem Cslib.GenericRAM.HeavyBranchFold.mem_heavyVarList_iff {n b₀ v : ℕ} {sys : List (List (List ℕ))} : v ∈ heavyVarList n b₀ sys ↔ v < n ∧ b₀ < Complexity.varDegree v sys

theorem Cslib.GenericRAM.HeavyBranchFold.lt_of_mem_heavyVarList {n b₀ v : ℕ} {sys : List (List (List ℕ))} (hv : v ∈ heavyVarList n b₀ sys) : v < n

theorem Cslib.GenericRAM.HeavyBranchFold.varDegree_le_of_not_mem_heavyVarList {n b₀ u : ℕ} {sys : List (List (List ℕ))} (hun : u < n) (hu : u ∉ heavyVarList n b₀ sys) : Complexity.varDegree u sys ≤ b₀

theorem Cslib.GenericRAM.HeavyBranchFold.toFinset_heavyVarList_eq_heavyVars (n b₀ : ℕ) (sys : List (List (List ℕ))) : (heavyVarList n b₀ sys).toFinset = BitString.heavyVars (Finset.range n) Finset.univ (fun (i : Fin sys.length) => (Complexity.equationVars sys[i]).toFinset) b₀

Specification bridge to SparseEquations.heavyVars: heavyVarList n b₀ sys enumerates Cslib.BitString.heavyVars in strictly increasing order.

theorem Cslib.GenericRAM.HeavyBranchFold.length_heavyVarList_le_div {n b₀ : ℕ} {sys : List (List (List ℕ))} (hb₀ : 0 < b₀) (hvars : ∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n) : (heavyVarList n b₀ sys).length ≤ (List.map (fun (eq : List (List ℕ)) => (Complexity.equationVars eq).length) sys).sum / b₀

Markov heavy-variable bound (§5.5, p. 38): for 0 < b₀ and variables < n, (heavyVarList n b₀ sys).length ≤ (sys.map fun eq => (equationVars eq).length).sum / b₀.

2. Order-Preserving Dense Free-Variable Relabeling

def Cslib.GenericRAM.HeavyBranchFold.relabelFreeVar (S : List ℕ) (v : ℕ) : ℕ

Densely relabel a free variable v : ℕ outside S as v - (S.filter (· < v)).length (defined totally for all v : ℕ, with natural subtraction truncated at 0 if (S.filter (· < v)).length is at least v).

theorem Cslib.GenericRAM.HeavyBranchFold.relabelFreeVar_strictMono {S : List ℕ} (hS : S.Nodup) {u v : ℕ} (hu : u ∉ S) (huv : u < v) : relabelFreeVar S u < relabelFreeVar S v

For S.Nodup, relabelFreeVar S is strictly increasing from u ∉ S to any larger v.

theorem Cslib.GenericRAM.HeavyBranchFold.relabelFreeVar_lt_sub {n : ℕ} {S : List ℕ} (hS : S.Nodup) (hSn : ∀ s ∈ S, s < n) {u : ℕ} (hu : u ∉ S) (hun : u < n) : relabelFreeVar S u < n - S.length

For S.Nodup in < n, every free variable u < n outside S maps below n - S.length.

theorem Cslib.GenericRAM.HeavyBranchFold.relabelFreeVar_injOn {S : List ℕ} (hS : S.Nodup) {u v : ℕ} (hu : u ∉ S) (hv : v ∉ S) (heq : relabelFreeVar S u = relabelFreeVar S v) : u = v

For S.Nodup, relabelFreeVar S is injective on all variables outside S.

noncomputable def Cslib.GenericRAM.HeavyBranchFold.freeVarEquiv {n : ℕ} {S : List ℕ} (hS : S.Nodup) (hSn : ∀ s ∈ S, s < n) : { i : Fin n // ↑i ∉ S } ≃ Fin (n - S.length)

Order-preserving bijection [n] \ S ≃ Fin (n - S.length) for S.Nodup in < n.

3. Multi-Variable Substitution, Canonicalization, and prepareBranch

def Cslib.GenericRAM.HeavyBranchFold.substituteEquation (S : List ℕ) (vals : List Bool) (eq : List (List ℕ)) : List (List ℕ)

Substitute (S, vals) across eq and cancel duplicate monomials modulo 2 (looking up the first index S.idxOf v if S has duplicates, defaulting missing entries ≥ vals.length to false, and ignoring trailing vals entries past S.length).

def Cslib.GenericRAM.HeavyBranchFold.relabelEquation (S : List ℕ) (eq : List (List ℕ)) : List (List ℕ)

Relabel all free variables in an equation using relabelFreeVar S.

inductive Cslib.GenericRAM.HeavyBranchFold.BranchOutcome : Type

Outcome of preparing a single heavy-variable branch (S ↦ vals) (§5.5 of [OAI26c]).

• contradiction : BranchOutcome

  Contradictory constant equation 1 = 0 ([[]]) appeared; 0 satisfying completions.

• tautology (freeVars : ℕ) : BranchOutcome

  All equations simplified to 0 = 0; all 2 ^ freeVars completions satisfy the system.

• reduced (freeVars : ℕ) (sys : List (List (List ℕ))) : BranchOutcome

  Non-empty reduced system on freeVars = n - |S| densely relabeled free variables.

@[instance_reducible]

instance Cslib.GenericRAM.HeavyBranchFold.instDecidableEqBranchOutcome : DecidableEq BranchOutcome

def Cslib.GenericRAM.HeavyBranchFold.instDecidableEqBranchOutcome.decEq (x✝ x✝¹ : BranchOutcome) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.GenericRAM.HeavyBranchFold.instReprBranchOutcome : Repr BranchOutcome

def Cslib.GenericRAM.HeavyBranchFold.instReprBranchOutcome.repr : BranchOutcome → ℕ → Std.Format

def Cslib.GenericRAM.HeavyBranchFold.BranchOutcome.toOption : BranchOutcome → Option (ℕ × Option (List (List (List ℕ))))

Structural option view of BranchOutcome for native encoding and option elimination.

theorem Cslib.GenericRAM.HeavyBranchFold.BranchOutcome.toOption_injective : Function.Injective toOption

@[irreducible]

def Cslib.GenericRAM.HeavyBranchFold.encBranchOutcome : BranchOutcome ↪ List Bool

Native binary encoding of BranchOutcome (n' in unary, sys' as framed nested lists).

def Cslib.GenericRAM.HeavyBranchFold.prepareBranch (n : ℕ) (S : List ℕ) (vals : List Bool) (sys : List (List (List ℕ))) : BranchOutcome

Restrict sys to S ↦ vals, drop 0 = 0 ([]), short-circuit 1 = 0 ([[]]) and empty systems, or densely relabel [n] \ S ≃ [n - S.length] (truncated at 0 if n < |S|).

theorem Cslib.GenericRAM.HeavyBranchFold.nodup_substituteEquation (S : List ℕ) (vals : List Bool) (eq : List (List ℕ)) : (substituteEquation S vals eq).Nodup

theorem Cslib.GenericRAM.HeavyBranchFold.length_substituteEquation_le (S : List ℕ) (vals : List Bool) (eq : List (List ℕ)) : (substituteEquation S vals eq).length ≤ eq.length

theorem Cslib.GenericRAM.HeavyBranchFold.mem_substituteEquation_exists {S : List ℕ} {vals : List Bool} {eq : List (List ℕ)} {m' : List ℕ} (hm' : m' ∈ substituteEquation S vals eq) : ∃ m ∈ eq, m' = List.filter (fun (v : ℕ) => decide (v ∉ S)) m

theorem Cslib.GenericRAM.HeavyBranchFold.isCanonicalEquation_substituteEquation (S : List ℕ) (vals : List Bool) {eq : List (List ℕ)} (heq : Complexity.IsCanonicalEquation eq) : Complexity.IsCanonicalEquation (substituteEquation S vals eq)

theorem Cslib.GenericRAM.HeavyBranchFold.isCanonicalEquation_relabelEquation {S : List ℕ} (hS : S.Nodup) {eq : List (List ℕ)} (heq : Complexity.IsCanonicalEquation eq) (hfree : ∀ m ∈ eq, ∀ u ∈ m, u ∉ S) : Complexity.IsCanonicalEquation (relabelEquation S eq)

theorem Cslib.GenericRAM.HeavyBranchFold.prepareBranch_freeVars_eq {n n' : ℕ} {S : List ℕ} {vals : List Bool} {sys : List (List (List ℕ))} : (prepareBranch n S vals sys = BranchOutcome.tautology n' → n' = n - S.length) ∧ ∀ (sys' : List (List (List ℕ))), prepareBranch n S vals sys = BranchOutcome.reduced n' sys' → n' = n - S.length

theorem Cslib.GenericRAM.HeavyBranchFold.prepareBranch_eq_reduced_iff {n n' : ℕ} {S : List ℕ} {vals : List Bool} {sys sys' : List (List (List ℕ))} : prepareBranch n S vals sys = BranchOutcome.reduced n' sys' ↔ have nonZero := List.filter (fun (eq : List (List ℕ)) => !eq.isEmpty) (List.map (substituteEquation S vals) sys); [[]] ∉ nonZero ∧ nonZero ≠ [] ∧ n' = n - S.length ∧ sys' = List.map (relabelEquation S) nonZero

theorem Cslib.GenericRAM.HeavyBranchFold.prepareBranch_reduced_canonical {n : ℕ} {S : List ℕ} {vals : List Bool} {sys sys' : List (List (List ℕ))} {n' : ℕ} (hS : S.Nodup) (hSn : ∀ s ∈ S, s < n) (hcan : ∀ eq ∈ sys, Complexity.IsCanonicalEquation eq) (hvars : ∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n) (hred : prepareBranch n S vals sys = BranchOutcome.reduced n' sys') : n' = n - S.length ∧ sys' ≠ [] ∧ [] ∉ sys' ∧ [[]] ∉ sys' ∧ (∀ eq' ∈ sys', Complexity.IsCanonicalEquation eq') ∧ ∀ eq' ∈ sys', ∀ m' ∈ eq', ∀ v' ∈ m', v' < n'

For S.Nodup in < n and canonical sys on < n, any .reduced n' sys' branch has n' = n - S.length, sys' ≠ [], [] ∉ sys', [[]] ∉ sys', and canonical < n' equations.

theorem Cslib.GenericRAM.HeavyBranchFold.prepareBranch_reduced_degree_le {n k : ℕ} {S : List ℕ} {vals : List Bool} {sys sys' : List (List (List ℕ))} {n' : ℕ} (hdeg : ∀ eq ∈ sys, ∀ m ∈ eq, m.length ≤ k) (hred : prepareBranch n S vals sys = BranchOutcome.reduced n' sys') (eq' : List (List ℕ)) : eq' ∈ sys' → ∀ m' ∈ eq', m'.length ≤ k

Degree preservation: if sys has degree at most k, so does any reduced branch sys'.

theorem Cslib.GenericRAM.HeavyBranchFold.prepareBranch_reduced_length_le {n : ℕ} {S : List ℕ} {vals : List Bool} {sys sys' : List (List (List ℕ))} {n' : ℕ} (hred : prepareBranch n S vals sys = BranchOutcome.reduced n' sys') : sys'.length ≤ sys.length ∧ ∀ eq' ∈ sys', ∃ eq ∈ sys, eq'.length ≤ eq.length ∧ (Complexity.equationVars eq').length ≤ (Complexity.equationVars eq).length

Monomial-count and scope-width preservation across prepareBranch.

theorem Cslib.GenericRAM.HeavyBranchFold.varDegree_relabelFreeVar_le {n : ℕ} {S : List ℕ} {vals : List Bool} {sys sys' : List (List (List ℕ))} {n' : ℕ} (hS : S.Nodup) {u : ℕ} (hu : u ∉ S) (hred : prepareBranch n S vals sys = BranchOutcome.reduced n' sys') : Complexity.varDegree (relabelFreeVar S u) sys' ≤ Complexity.varDegree u sys

Per-variable incidence preservation: for S.Nodup and u ∉ S, varDegree (relabelFreeVar S u) on any .reduced branch sys' never exceeds varDegree u sys.

theorem Cslib.GenericRAM.HeavyBranchFold.prepareBranch_reduced_varDegree_le {n b₀ : ℕ} {S : List ℕ} {vals : List Bool} {sys sys' : List (List (List ℕ))} {n' : ℕ} (hS : S.Nodup) (hSn : ∀ s ∈ S, s < n) (hinc : ∀ u < n, u ∉ S → Complexity.varDegree u sys ≤ b₀) (hred : prepareBranch n S vals sys = BranchOutcome.reduced n' sys') (u' : ℕ) : u' < n' → Complexity.varDegree u' sys' ≤ b₀

Uniform free-variable incidence preservation (§5.5 of [OAI26c]): for S.Nodup in < n, if every u < n outside S has varDegree u sys ≤ b₀, every u' < n' in sys' has ≤ b₀.

4. Exact Common-Zero Count Preservation

def Cslib.GenericRAM.HeavyBranchFold.branchRootCount : BranchOutcome → ℕ

Exact common-zero count represented by a BranchOutcome.

def Cslib.GenericRAM.HeavyBranchFold.branchCountOracle (solver : ℕ → List (List (List ℕ)) → ℕ) : BranchOutcome → ℕ

Dispatch a BranchOutcome to an external counting oracle solver on .reduced branches.

@[simp]

theorem Cslib.GenericRAM.HeavyBranchFold.branchCountOracle_rootCount : branchCountOracle rootCount = branchRootCount

theorem Cslib.GenericRAM.HeavyBranchFold.branchRootCount_prepareBranch {n : ℕ} {S : List ℕ} {vals : List Bool} {sys : List (List (List ℕ))} (hS : S.Nodup) (hSn : ∀ s ∈ S, s < n) (hvars : ∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n) (hvals : vals.length = S.length) : branchRootCount (prepareBranch n S vals sys) = {σ : BitString n | List.map (extendAssignment σ) S = vals ∧ Complexity.evalSystem sys (extendAssignment σ) = true}.card

Single-branch exactness: for S.Nodup in < n, sys on < n, and vals.length = S.length, branchRootCount (prepareBranch n S vals sys) counts common zeros extending (S, vals).

theorem Cslib.GenericRAM.HeavyBranchFold.sum_branch_count_eq_rootCount {n : ℕ} {S : List ℕ} {sys : List (List (List ℕ))} {solver : ℕ → List (List (List ℕ)) → ℕ} (hS : S.Nodup) (hSn : ∀ s ∈ S, s < n) (hvars : ∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n) (hsolver : ∀ (vals : List Bool), vals.length = S.length → ∀ (n' : ℕ) (sys' : List (List (List ℕ))), prepareBranch n S vals sys = BranchOutcome.reduced n' sys' → solver n' sys' = rootCount n' sys') : (List.map (fun (idx : ℕ) => branchCountOracle solver (prepareBranch n S (BitString.lowBits S.length idx) sys)) (List.range (2 ^ S.length))).sum = rootCount n sys

Exponential-branching decomposition identity: for S.Nodup in < n and sys on < n, summing branchCountOracle solver over 0 ≤ idx < 2 ^ S.length via lowBits S.length idx equals rootCount n sys whenever solver is exact on .reduced branches.

5. Plain Polynomial-Time Certificates for heavyVarList and prepareBranch

theorem Cslib.GenericRAM.HeavyBranchFold.computableInPolyTime_heavyVarList : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × List (List (List ℕ))) => heavyVarList p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Computing heavyVarList n b₀ sys (n in unary, b₀ in binary) is polynomial-time.

theorem Cslib.GenericRAM.HeavyBranchFold.computableInPolyTime_heavyVarList_comp {α : Type} {encIn : α ↪ List Bool} {fn fb : α → ℕ} {fsys : α → List (List (List ℕ))} (hn : Turing.MultiTapeTM.ComputableInPolyTime fn encIn Turing.MultiTapeTM.encUnary) (hb : Turing.MultiTapeTM.ComputableInPolyTime fb encIn Turing.MultiTapeTM.encNat) (hsys : Turing.MultiTapeTM.ComputableInPolyTime fsys encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => heavyVarList (fn a) (fb a) (fsys a)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

theorem Cslib.GenericRAM.HeavyBranchFold.computableInPolyTime_relabelFreeVar : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List ℕ × ℕ) => relabelFreeVar p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat

relabelFreeVar is computable in polynomial time.

theorem Cslib.GenericRAM.HeavyBranchFold.computableInPolyTime_relabelFreeVar_comp {α : Type} {encIn : α ↪ List Bool} {S : α → List ℕ} {v : α → ℕ} (hS : Turing.MultiTapeTM.ComputableInPolyTime S encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hv : Turing.MultiTapeTM.ComputableInPolyTime v encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => relabelFreeVar (S a) (v a)) encIn Turing.MultiTapeTM.encNat

theorem Cslib.GenericRAM.HeavyBranchFold.computableInPolyTime_relabelEquation : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List ℕ × List (List ℕ)) => relabelEquation p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

relabelEquation is computable in polynomial time.

theorem Cslib.GenericRAM.HeavyBranchFold.computableInPolyTime_relabelEquation_comp {α : Type} {encIn : α ↪ List Bool} {S : α → List ℕ} {eq : α → List (List ℕ)} (hS : Turing.MultiTapeTM.ComputableInPolyTime S encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (heq : Turing.MultiTapeTM.ComputableInPolyTime eq encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => relabelEquation (S a) (eq a)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

theorem Cslib.GenericRAM.HeavyBranchFold.computableInPolyTime_substituteEquation : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List ℕ × List Bool × List (List ℕ)) => substituteEquation p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

substituteEquation is computable in polynomial time.

theorem Cslib.GenericRAM.HeavyBranchFold.computableInPolyTime_substituteEquation_comp {α : Type} {encIn : α ↪ List Bool} {S : α → List ℕ} {vals : α → List Bool} {eq : α → List (List ℕ)} (hS : Turing.MultiTapeTM.ComputableInPolyTime S encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hvals : Turing.MultiTapeTM.ComputableInPolyTime vals encIn Turing.MultiTapeTM.encBits) (heq : Turing.MultiTapeTM.ComputableInPolyTime eq encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => substituteEquation (S a) (vals a) (eq a)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

theorem Cslib.GenericRAM.HeavyBranchFold.computableInPolyTime_prepareBranch : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List ℕ × List Bool × List (List (List ℕ))) => prepareBranch p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))))) encBranchOutcome

prepareBranch is computable in polynomial time.

theorem Cslib.GenericRAM.HeavyBranchFold.computableInPolyTime_prepareBranch_comp {α : Type} {encIn : α ↪ List Bool} {n : α → ℕ} {S : α → List ℕ} {vals : α → List Bool} {sys : α → List (List (List ℕ))} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hS : Turing.MultiTapeTM.ComputableInPolyTime S encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hvals : Turing.MultiTapeTM.ComputableInPolyTime vals encIn Turing.MultiTapeTM.encBits) (hsys : Turing.MultiTapeTM.ComputableInPolyTime sys encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => prepareBranch (n a) (S a) (vals a) (sys a)) encIn encBranchOutcome

6. Space-Efficient Streaming BooleanFold Combinator

@[reducible, inline]

abbrev Cslib.GenericRAM.HeavyBranchFold.BranchInput : Type

Input tuple (n, S, sys) for streaming heavy-variable branching.

@[instance_reducible]

instance Cslib.GenericRAM.HeavyBranchFold.instDecidableEqBranchInput : DecidableEq BranchInput

def Cslib.GenericRAM.HeavyBranchFold.encBranchInput : BranchInput ↪ List Bool

Native encoding of BranchInput (n in unary, S and sys as framed lists).

theorem Cslib.GenericRAM.HeavyBranchFold.length_enc_reduced_le {n n' : ℕ} {S : List ℕ} {vals : List Bool} {sys sys' : List (List (List ℕ))} (hred : prepareBranch n S vals sys = BranchOutcome.reduced n' sys') : ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) (n', sys')).length ≤ (encBranchInput (n, S, sys)).length

Encoded-size non-expansion: every .reduced n' sys' branch produced by prepareBranch has encoded solver input (n', sys') no longer than the parent encBranchInput (n, S, sys).

def Cslib.GenericRAM.HeavyBranchFold.branchBody (solver : ℕ → List (List (List ℕ)) → ℕ) (p : (ℕ × List Bool) × BranchInput × ℕ) : BranchInput × ℕ

Single streaming step of heavy-variable branching.

def Cslib.GenericRAM.HeavyBranchFold.streamBranches (solver : ℕ → List (List (List ℕ)) → ℕ) (inp : BranchInput) : ℕ × ℕ × BranchInput × ℕ

Stream all 2 ^ |S| heavy-variable assignments via BooleanFold.run without materializing the assignment list, returning (finalIdx, (|S|, (inp, totalCount))).

def Cslib.GenericRAM.HeavyBranchFold.countByBranching (solver : ℕ → List (List (List ℕ)) → ℕ) (inp : BranchInput) : ℕ

Total common-zero count computed by streaming 2 ^ |S| heavy-variable branches.

theorem Cslib.GenericRAM.HeavyBranchFold.runPrefix_branchBody_accumulator (solver : ℕ → List (List (List ℕ)) → ℕ) (inp : BranchInput) (j : ℕ) : (BooleanFold.runPrefix (branchBody solver) inp.2.1.length j (inp, 0)).2.2 = (inp, (List.map (fun (idx : ℕ) => branchCountOracle solver (prepareBranch inp.1 inp.2.1 (BitString.lowBits inp.2.1.length idx) inp.2.2)) (List.range j)).sum)

Prefix invariant of BooleanFold.runPrefix: inp is preserved and the accumulator holds the sum of the first j decoded branch counts.

theorem Cslib.GenericRAM.HeavyBranchFold.streamBranches_correct {n : ℕ} {S : List ℕ} {sys : List (List (List ℕ))} {solver : ℕ → List (List (List ℕ)) → ℕ} (hS : S.Nodup) (hSn : ∀ s ∈ S, s < n) (hvars : ∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n) (hsolver : ∀ (vals : List Bool), vals.length = S.length → ∀ (n' : ℕ) (sys' : List (List (List ℕ))), prepareBranch n S vals sys = BranchOutcome.reduced n' sys' → solver n' sys' = rootCount n' sys') : (streamBranches solver (n, S, sys)).2.2 = ((n, S, sys), rootCount n sys)

Streaming correctness: for S.Nodup in < n and sys on < n, (streamBranches solver (n, S, sys)).2.2 = ((n, S, sys), rootCount n sys) when solver is exact on .reduced branches.

theorem Cslib.GenericRAM.HeavyBranchFold.countByBranching_eq_rootCount {n : ℕ} {S : List ℕ} {sys : List (List (List ℕ))} {solver : ℕ → List (List (List ℕ)) → ℕ} (hS : S.Nodup) (hSn : ∀ s ∈ S, s < n) (hvars : ∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n) (hsolver : ∀ (vals : List Bool), vals.length = S.length → ∀ (n' : ℕ) (sys' : List (List (List ℕ))), prepareBranch n S vals sys = BranchOutcome.reduced n' sys' → solver n' sys' = rootCount n' sys') : countByBranching solver (n, S, sys) = rootCount n sys

Streaming count correctness: for S.Nodup in < n and sys on < n, countByBranching solver (n, S, sys) = rootCount n sys when solver is exact on .reduced branches.

noncomputable def Cslib.GenericRAM.HeavyBranchFold.branchCountCertificate {solver : ℕ → List (List (List ℕ)) → ℕ} (csolver : NativeCertificate (fun (p : ℕ × List (List (List ℕ))) => solver 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) : NativeCertificate (branchCountOracle solver) encBranchOutcome Turing.MultiTapeTM.encNat

Selected-branch native certificate for branchCountOracle solver: a fixed csolver runs ONLY on .reduced n' sys' outcomes, while .contradiction emits 0 and .tautology n' emits 2 ^ n' via BooleanFold.clock in linear time and space.

theorem Cslib.GenericRAM.HeavyBranchFold.computableInPolyTime_prepareStep : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × List Bool) × BranchInput × ℕ) => prepareBranch p.2.1.1 p.2.1.2.1 p.1.2 p.2.1.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair encBranchInput Turing.MultiTapeTM.encNat)) encBranchOutcome

noncomputable def Cslib.GenericRAM.HeavyBranchFold.branchBodyCertificate {solver : ℕ → List (List (List ℕ)) → ℕ} (csolver : NativeCertificate (fun (p : ℕ × List (List (List ℕ))) => solver 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) : NativeCertificate (branchBody solver) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair encBranchInput Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encPair encBranchInput Turing.MultiTapeTM.encNat)

Per-branch native callback certificate for branchBody solver (for a fixed solver).

noncomputable def Cslib.GenericRAM.HeavyBranchFold.certificate {solver : ℕ → List (List (List ℕ)) → ℕ} (csolver : NativeCertificate (fun (p : ℕ × List (List (List ℕ))) => solver 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) : NativeCertificate (streamBranches solver) encBranchInput (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair encBranchInput Turing.MultiTapeTM.encNat)))

Full streaming native certificate for streamBranches solver (for a fixed solver).

noncomputable def Cslib.GenericRAM.HeavyBranchFold.countCertificate {solver : ℕ → List (List (List ℕ)) → ℕ} (csolver : NativeCertificate (fun (p : ℕ × List (List (List ℕ))) => solver 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) : NativeCertificate (countByBranching solver) encBranchInput Turing.MultiTapeTM.encNat

Full streaming native certificate for countByBranching solver (for a fixed solver).

theorem Cslib.GenericRAM.HeavyBranchFold.runPrefix_sum_le {solver : ℕ → List (List (List ℕ)) → ℕ} {inp : BranchInput} (hbound : ∀ idx < 2 ^ inp.2.1.length, ∀ (n' : ℕ) (sys' : List (List (List ℕ))), prepareBranch inp.1 inp.2.1 (BitString.lowBits inp.2.1.length idx) inp.2.2 = BranchOutcome.reduced n' sys' → solver n' sys' ≤ 2 ^ n') {j : ℕ} (hj : j ≤ 2 ^ inp.2.1.length) : (BooleanFold.runPrefix (branchBody solver) inp.2.1.length j (inp, 0)).2.2.2 ≤ j * 2 ^ (inp.1 - inp.2.1.length)

Prefix sum bound: when solver n' sys' ≤ 2 ^ n' on reduced branches of inp, every streaming prefix j ≤ 2 ^ |S| keeps the running sum at most j * 2 ^ (n - |S|).

theorem Cslib.GenericRAM.HeavyBranchFold.runPrefix_sum_le_two_pow {solver : ℕ → List (List (List ℕ)) → ℕ} {inp : BranchInput} (hSn : inp.2.1.length ≤ inp.1) (hbound : ∀ idx < 2 ^ inp.2.1.length, ∀ (n' : ℕ) (sys' : List (List (List ℕ))), prepareBranch inp.1 inp.2.1 (BitString.lowBits inp.2.1.length idx) inp.2.2 = BranchOutcome.reduced n' sys' → solver n' sys' ≤ 2 ^ n') {j : ℕ} (hj : j ≤ 2 ^ inp.2.1.length) : (BooleanFold.runPrefix (branchBody solver) inp.2.1.length j (inp, 0)).2.2.2 ≤ 2 ^ inp.1

When |S| ≤ n and solver n' sys' ≤ 2 ^ n' on reduced branches, the running sum satisfies Z ≤ 2 ^ n throughout the entire streaming traversal (§5.5 p. 39 of [OAI26c]).

noncomputable def Cslib.GenericRAM.HeavyBranchFold.stepOverhead (L : ℕ) : ℕ

Solver-independent polynomial overhead per streaming round and for initialization.

theorem Cslib.GenericRAM.HeavyBranchFold.polynomiallyBounded_stepOverhead : PolynomiallyBounded stepOverhead

stepOverhead is polynomially bounded in the encoded input length.

theorem Cslib.GenericRAM.HeavyBranchFold.streamBranches_computableInO {solver : ℕ → List (List (List ℕ)) → ℕ} (csolver : NativeCertificate (fun (p : ℕ × List (List (List ℕ))) => solver 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) (R_solver Q_solver : BranchInput → ℕ) (hbound : ∀ (inp : BranchInput), ∀ idx < 2 ^ inp.2.1.length, ∀ (n' : ℕ) (sys' : List (List (List ℕ))), prepareBranch inp.1 inp.2.1 (BitString.lowBits inp.2.1.length idx) inp.2.2 = BranchOutcome.reduced n' sys' → solver n' sys' ≤ 2 ^ n') (hR : ∀ (inp : BranchInput), ∀ idx < 2 ^ inp.2.1.length, ∀ (n' : ℕ) (sys' : List (List (List ℕ))), prepareBranch inp.1 inp.2.1 (BitString.lowBits inp.2.1.length idx) inp.2.2 = BranchOutcome.reduced n' sys' → csolver.time (n', sys') ≤ R_solver inp) (hQ : ∀ (inp : BranchInput), ∀ idx < 2 ^ inp.2.1.length, ∀ (n' : ℕ) (sys' : List (List (List ℕ))), prepareBranch inp.1 inp.2.1 (BitString.lowBits inp.2.1.length idx) inp.2.2 = BranchOutcome.reduced n' sys' → csolver.space (n', sys') ≤ Q_solver inp) : Turing.MultiTapeTM.ComputableInO (streamBranches solver) encBranchInput (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair encBranchInput Turing.MultiTapeTM.encNat))) (fun (inp : BranchInput) => stepOverhead (encBranchInput inp).length + (2 ^ inp.2.1.length + 1) * (stepOverhead (encBranchInput inp).length + R_solver inp)) fun (inp : BranchInput) => stepOverhead (encBranchInput inp).length + Q_solver inp

Space-efficient streaming ComputableInO bound for streamBranches (§5.5 of [OAI26c]): for fixed solver bounded by 2 ^ n' with time ≤ R_solver and space ≤ Q_solver on .reduced branches, runs in time O(stepOverhead |inp| + (2 ^ |S| + 1) * (stepOverhead |inp| + R_solver inp)) and workspace O(stepOverhead |inp| + Q_solver inp).

theorem Cslib.GenericRAM.HeavyBranchFold.countByBranching_computableInO {solver : ℕ → List (List (List ℕ)) → ℕ} (csolver : NativeCertificate (fun (p : ℕ × List (List (List ℕ))) => solver 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) (R_solver Q_solver : BranchInput → ℕ) (hbound : ∀ (inp : BranchInput), ∀ idx < 2 ^ inp.2.1.length, ∀ (n' : ℕ) (sys' : List (List (List ℕ))), prepareBranch inp.1 inp.2.1 (BitString.lowBits inp.2.1.length idx) inp.2.2 = BranchOutcome.reduced n' sys' → solver n' sys' ≤ 2 ^ n') (hR : ∀ (inp : BranchInput), ∀ idx < 2 ^ inp.2.1.length, ∀ (n' : ℕ) (sys' : List (List (List ℕ))), prepareBranch inp.1 inp.2.1 (BitString.lowBits inp.2.1.length idx) inp.2.2 = BranchOutcome.reduced n' sys' → csolver.time (n', sys') ≤ R_solver inp) (hQ : ∀ (inp : BranchInput), ∀ idx < 2 ^ inp.2.1.length, ∀ (n' : ℕ) (sys' : List (List (List ℕ))), prepareBranch inp.1 inp.2.1 (BitString.lowBits inp.2.1.length idx) inp.2.2 = BranchOutcome.reduced n' sys' → csolver.space (n', sys') ≤ Q_solver inp) : Turing.MultiTapeTM.ComputableInO (countByBranching solver) encBranchInput Turing.MultiTapeTM.encNat (fun (inp : BranchInput) => stepOverhead (encBranchInput inp).length + (2 ^ inp.2.1.length + 1) * (stepOverhead (encBranchInput inp).length + R_solver inp)) fun (inp : BranchInput) => stepOverhead (encBranchInput inp).length + Q_solver inp

Space-efficient streaming ComputableInO bound for countByBranching (§5.5 of [OAI26c]): for fixed solver bounded by 2 ^ n' with time ≤ R_solver and space ≤ Q_solver on .reduced branches, returns the total count in time O(stepOverhead |inp| + (2 ^ |S| + 1) * (stepOverhead |inp| + R_solver inp)) and workspace O(stepOverhead |inp| + Q_solver inp) (with no 2 ^ |S| factor in workspace).

theorem Cslib.GenericRAM.HeavyBranchFold.polyBounded_branchWorkspace {Q_solver : BranchInput → ℕ} (hQ : Turing.MultiTapeTM.PolyBounded (fun (inp : BranchInput) => (encBranchInput inp).length) Q_solver) : Turing.MultiTapeTM.PolyBounded (fun (inp : BranchInput) => (encBranchInput inp).length) fun (inp : BranchInput) => stepOverhead (encBranchInput inp).length + Q_solver inp

Polynomial-workspace preservation: whenever Q_solver is polynomially bounded in the encoded input length, the total streaming workspace stepOverhead |inp| + Q_solver inp is also polynomially bounded (independent of 2 ^ |S|).