Exact root-count correctness for the bounded-incidence branch evaluator (Proposition 5.3)

Proves the Stage-2 measurement-fiber Taylor-jet equivalence and Hermite–Cramer modular recovery theorem evalBoundedIncidenceBranch_eq_rootCount for the executable bounded-incidence branch evaluator evalBoundedIncidenceBranch from Complexity.Computability.PolyTime.BooleanAnalysis.BoundedIncidenceSemantics, formalizing the semantic correctness half of 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). The measurement-fiber step instantiates the generic decoupled sum–product identity Cslib.SharedSummaries.sum_prod_eq_sum_measurement_fibers on the executable group data.

Exactness holds on feasible prepared inputs (prepareBranchEvalInput (n', eqs') when checkBranchFeasible N₀_branch (n', eqs') = true). 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.

Main results

• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.evalBoundedIncidenceBranch_eq_rootCount: whenever checkBranchFeasible N₀_branch (n', eqs') = true, evalBoundedIncidenceBranch (prepareBranchEvalInput (n', eqs')) equals HeavyBranchFold.rootCount n' eqs'.

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. Formal Cleared Parity-Factor Polynomials and Graded Degree Subring

2. Per-Equation Jet Evaluation and Measurement-Fiber Baseline Invariance

3. Measurement-Tuple Coverage and Two-Pass Fiber Jet Fold Equivalence

4. Restricted Subset-Pair Möbius Fold and Exact Node Taylor-Jet Identity

5. Exact Root-Count Recovery (evalBoundedIncidenceBranch_eq_rootCount)

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.evalBoundedIncidenceBranch_eq_rootCount {N₀_branch n' : ℕ} {eqs' : List (List (List ℕ))} (hfeas : checkBranchFeasible N₀_branch (n', eqs') = true) : evalBoundedIncidenceBranch (prepareBranchEvalInput (n', eqs')) = GenericRAM.HeavyBranchFold.rootCount n' eqs'

Proposition 5.3 exact root-count correctness (OpenAI, The Exponential Time Hypothesis is False, §§5.3–5.5, Proposition 5.3, pp. 37–39): whenever a reduced system (n', eqs') passes checkBranchFeasible N₀_branch, evalBoundedIncidenceBranch (prepareBranchEvalInput (n', eqs')) equals HeavyBranchFold.rootCount n' eqs'.