Executable bounded-incidence branch evaluator and Stage-1 design refinement (Proposition 5.3)

Pure executable bounded-incidence branch evaluator evalBoundedIncidenceBranch : BranchEvalInput → ℕ, entry and design-shape guards (validBranchEvalParams, validDesignShape), unconditional cube bound evalBoundedIncidenceBranch_le_two_pow, Stage-1 parameter unclamping and ReplacementDesign refinement on feasible prepared inputs (prepareBranchEvalInput (n', eqs') under checkBranchFeasible N₀_branch (n', eqs') = true), and Stage-2 local assignment/cube bridges for Proposition 5.3 of OpenAI, The Exponential Time Hypothesis is False (§§3.4–3.5, §4.6, §§5.3–5.5, Proposition 5.3, and Appendix B.2–B.3, pp. 24–26, 33–34, 37–39, 48–50). Invalid raw inputs return 0, validDesignShape enforces unary resource-dimension bounds rather than semantic validity of arbitrary designs, and exact root-count recovery on feasible prepared inputs follows in BoundedIncidenceExactness.

Given inp = ((n', k'), (b, w, M', β), (r, Q, R, A₀), eqs') : BranchEvalInput:

1. Entry guard and unary-clamped parameters: validBranchEvalParams checks the structural and schedule range invariants (including r_u ^ (2 * Q_u) ≤ n', variable bounds < n', canonicality, and sysMaxDegree eqs' ≤ k'), clamping (Q, R, r, A₀, D) from the left against unary expressions in n' so resource certificates remain uniform across all BranchEvalInput tuples.
2. Greedy balanced schedule and Lemma 4.7 replacement design: augments equation scopes with neutral singletons via withNeutralScopesList, constructs balanced variable/factor schedules via BalancedSchedules.constructBalancedSchedules, builds ReplacementDesignData via buildReplacementDesignData, and precomputes per-equation replacement-row lookup tables.
3. Two-pass measurement-fiber jet accumulation and Hermite–Cramer recovery: for each node t < Q_u (node = t + 1), folds over subset pairs (E, U, oddSign) via SubsetPairFold.run and signed measurement tuples via MeasurementFold.run; Pass 1 finds unrestricted local fiber representatives via BooleanMeasurements.search, Pass 2 streams restricted local fiber jet sums via CommonCountingAccum.streamGroupJetSum using evalAffineInputZJetTable and evalEquationParityFactorJet, multiplies group jets via CommonCountingAccum.prodJet, and recovers the count modulo 2 ^ (n' + 1) via CommonCountingAccum.recoverOuterJetSumModPowTwo.

Main definitions

• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.validBranchEvalParams, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.validDesignShape: Boolean entry and unary design-shape guards on BranchEvalInput and ReplacementDesignData.
• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.applyGroupBits, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.buildBaseAssignment, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkRestrictedGroup, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.buildEqRowTables, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.groupEquationsAt: local group bit overrides, restricted-cube test, and precomputed per-equation replacement-row tables.
• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.GroupEvalCtx, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.MeasStepCtx, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.SubsetStepCtx, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.evalGroupFactorJet, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.measurementStepBody, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.subsetPairStepBody: closed step contexts and step bodies for CommonCountingAccum.streamGroupJetSum, MeasurementFold.run, and SubsetPairFold.run.
• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.evalBoundedIncidenceBranch: executable Proposition 5.3 branch evaluator BranchEvalInput → ℕ.

Main results

• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.evalBoundedIncidenceBranch_le_two_pow: unconditional upper bound evalBoundedIncidenceBranch inp ≤ 2 ^ inp.1.1.
• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.validBranchEvalParams_prepare_of_feasible: passing checkBranchFeasible implies validBranchEvalParams on prepareBranchEvalInput.
• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.exists_refines_prepare_of_feasible: Stage-1 ReplacementDesignData.Refines witness and unclamped parameter identities on feasible prepared inputs.

References

• OpenAI, The Exponential Time Hypothesis is False, §§3.4–3.5, §4.6, §§5.3–5.5, Proposition 5.3, and Appendix B.2–B.3.

1. Entry Guard, Clamped Parameters, and Stage-1/Stage-2 Helpers

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.validBranchEvalParams (inp : BranchEvalInput) : Bool

Entry guard on inp = ((n', k'), (b, w, M', β), (r, Q, R, A₀), eqs') : BranchEvalInput verifying structural nondegeneracy, unary parameter bounds against n', auxiliary dimension bound r_u ^ (2 * Q_u) ≤ n', variable range < n', canonicality, and degree bound ≤ k'.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.validDesignShape (n' r_u m_eq : ℕ) (data : LinearAlgebra.ReplacementDesignData) : Bool

Design-shape guard checking unary measurement-dimension and local-group size bounds on ReplacementDesignData (both hold automatically under ReplacementParams.Feasible).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.applyGroupBits (n' : ℕ) (Vg : List ℕ) (ug base : List Bool) : List Bool

Override coordinates v ∈ Vg of base (of length n') using local bits ug.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.buildBaseAssignment (n' r_u : ℕ) (vGroups_t : List (List ℕ)) (reps : List (List Bool)) : List Bool

Assemble the baseline length-n' assignment x^* from per-group representatives reps.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.checkRestrictedGroup (n' : ℕ) (indE : List Bool) (Vg : List ℕ) (ug : List Bool) : Bool

Check restrictedLocalCube membership on Vg: every Vg[j] marked in indE has ug[j] = true.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.buildEqRowTables (n' : ℕ) (eqs' : List (List (List ℕ))) (data : LinearAlgebra.ReplacementDesignData) : List (List (List (List ℤ)))

Precompute for each equation f < eqs'.length and variable v < n' the cleared replacement row table data.lookupReplacementRow f v.

@[reducible, inline]

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

Context bundle for evalGroupFactorJet inside CommonCountingAccum.streamGroupJetSum: ((n', J, ℓ, k'), (node, denom), (Vg, Ctg, yg), (indE, indU, xStar), groupEqsWithTables) where each pair in groupEqsWithTables is (eq, rowsCoeffs_f) for an equation in group g at t.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.evalGroupFactorJet (p : GroupEvalCtx × ℕ × List Bool) : JetRows

Closed local-cube summand for CommonCountingAccum.streamGroupJetSum: returns 0 unless ug belongs to the indE-restricted local cube and matches measurement slice yg, in which case it evaluates the product of cleared parity-factor jets over equations assigned to group g at t.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.groupEquationsAt (eqs' : List (List (List ℕ))) (factorGroups : List (List ℕ)) (eqRowTables : List (List (List (List ℤ)))) (t g : ℕ) : List (List (List ℕ) × List (List (List ℤ)))

Precollect (eq, rowsCoeffs_f) for equations f < eqs'.length assigned to group g at t.

@[reducible, inline]

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

Context bundle carried unchanged through MeasurementFold.run at fixed (t, E, U): ((n', r_u, m_rows), (J, ℓ, k'), (node, dDen), (vGroups_t, grpMeas_t), (indE, indU), grpEqs).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.measurementStepBody (inp : ((ℕ × ℕ) × List ℤ) × MeasStepCtx × JetRows) : MeasStepCtx × JetRows

Closed step body for MeasurementFold.run: slices word into per-group targets yg, runs Pass 1 (BooleanMeasurements.search) across all g < r_u, and when all fibers are nonempty runs Pass 2 (CommonCountingAccum.streamGroupJetSum) across all g < r_u and adds their prodJet.

@[reducible, inline]

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

Context bundle carried unchanged through SubsetPairFold.run at fixed node t: ((n', r_u, m_rows), (c_meas, D_cap), (J, ℓ, k'), (node, dDen), (vGroups_t, grpMeas_t), eqs).

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.subsetPairStepBody (inp : GenericRAM.SubsetPairFold.DecodedPair × SubsetStepCtx × JetRows) : SubsetStepCtx × JetRows

Closed step body for SubsetPairFold.run: accumulates the signed measurement-fiber jet sum at (indE, indU, oddSign) via MeasurementFold.run.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.evalBoundedIncidenceBranch (inp : BranchEvalInput) : ℕ

Proposition 5.3 executable bounded-incidence branch evaluator (OpenAI, The Exponential Time Hypothesis is False, §§5.3–5.5, Proposition 5.3, pp. 37–39): on feasible prepared inputs (prepareBranchEvalInput (n', eqs') when checkBranchFeasible N₀_branch (n', eqs') = true), evaluates the exact number of common 𝔽₂ roots of eqs' on {0, 1}^{n'} via greedy balanced scheduling, Lemma 4.7 replacement-design construction, two-pass measurement-fiber Taylor jet accumulation, and Hermite–Cramer modular recovery. Invalid raw BranchEvalInput tuples fail validBranchEvalParams or the unary resource-dimension guard validDesignShape (which bounds measurement and group dimensions rather than certifying arbitrary designs) and return 0.

2. Unconditional Cube Upper Bound

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.evalBoundedIncidenceBranch_le_two_pow (inp : BranchEvalInput) : evalBoundedIncidenceBranch inp ≤ 2 ^ inp.1.1

evalBoundedIncidenceBranch inp never exceeds the ambient Boolean cube size 2 ^ n'.

3. Stage-1 Parameter Unclamping and ReplacementDesignData Refinement

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.validBranchEvalParams_prepare_of_feasible {N₀_branch n' : ℕ} {eqs' : List (List (List ℕ))} (hfeas : checkBranchFeasible N₀_branch (n', eqs') = true) : validBranchEvalParams (prepareBranchEvalInput (n', eqs')) = true

Passing checkBranchFeasible implies validBranchEvalParams on prepareBranchEvalInput.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.exists_refines_prepare_of_feasible {N₀_branch n' : ℕ} {eqs' : List (List (List ℕ))} (hfeas : checkBranchFeasible N₀_branch (n', eqs') = true) : have inp := prepareBranchEvalInput (n', eqs'); have b := inp.2.1.1; have w := inp.2.1.2.1; have r := inp.2.2.1.1; have Q := inp.2.2.1.2.1; have R := inp.2.2.1.2.2.1; have A₀ := inp.2.2.1.2.2.2; have augScopes := LinearAlgebra.withNeutralScopesList (List.map equationVars eqs') n'; have edges := LinearAlgebra.scopeIncidencesList n' augScopes; have scheds := BalancedSchedules.constructBalancedSchedules n' augScopes.length (min n' Q) (min n' r) (b + w) edges; have data := LinearAlgebra.buildReplacementDesignData n' (min n' (min n' r ^ (2 * min n' Q))) (min n' Q) (min n' r) (min (n' + 1) A₀) (min n' R) augScopes scheds.1 scheds.2; Q ≤ n' ∧ R ≤ n' ∧ r ≤ n' ∧ A₀ ≤ n' + 1 ∧ r ^ (2 * Q) ≤ n' ∧ validDesignShape n' (min n' r) eqs'.length data = true ∧ ∃ (D : LinearAlgebra.ReplacementDesign (LinearAlgebra.listScopeFamily n' augScopes) Q r A₀ R (ReplacementParams.tauRat n')), LinearAlgebra.ReplacementDesignData.Refines augScopes data D ∧ data.measurementMatrix.length = D.h * (LinearAlgebra.measurementIndices Q r A₀ R).card ∧ r * data.measurementMatrix.length ≤ n'

Under checkBranchFeasible N₀_branch (n', eqs') = true, the clamped schedule parameters in evalBoundedIncidenceBranch (prepareBranchEvalInput (n', eqs')) equal the unclamped schedule parameters, buildReplacementDesignData refines a concrete ReplacementDesign on withNeutralScopesList (eqs'.map equationVars) n', its measurement matrix has D.h * #(measurementIndices Q r A₀ R) rows with r * data.measurementMatrix.length ≤ n', and validDesignShape returns true.

4. Stage-2 Local Group Overrides, Measurement Fibers, and Jet Fold Equivalence