Native Resource Bounds for the Bounded-Incidence Branch Evaluator (Proposition 5.3)

This file establishes the native multi-tape Turing machine resource certificate, global polynomial workspace bound across all raw BranchEvalInput tuples, and subexponential $O^*(2^{O(\mathrm{interpolationScale}(n'))})$ runtime bound for the Proposition 5.3 bounded-incidence, bounded-width $\mathbb{F}_2$ polynomial-system branch evaluator evalBoundedIncidenceBranch of OpenAI, The Exponential Time Hypothesis is False (§§3.4–3.5, §4.7, §§5.3–5.5, Proposition 5.3, and Appendix B.2–B.3, pp. 24–26, 34–35, 37–39, 48–50).

Main definitions

• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.boundedIncidenceBranchCertificate: uniform NativeCertificate for evalBoundedIncidenceBranch on encBranchEvalInput.

Main results

• SparsePolyCounter.auxDim_lt_self_of_two_le: ReplacementParams.auxDim n' < n' for 2 ≤ n'.
• SparsePolyCounter.polyBounded_boundedIncidenceBranchCertificate_space: global PolyBounded workspace bound across all raw BranchEvalInput tuples.
• SparsePolyCounter.exists_boundedIncidenceBranchCertificate_time_bound: subexponential $O^*(2^{O(\mathrm{interpolationScale}(n'))})$ branch runtime bound on prepareBranchEvalInput (n', sys') under polylogarithmic factor incidence and scope width (Proposition 5.3, pp. 37–39).
• SparsePolyCounter.branchPolylogTimeBound_boundedIncidenceBranchCertificate: discharges Cslib.Complexity.BranchedSparseCNFCounter.BranchPolylogTimeBound for boundedIncidenceBranchCertificate.

References

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

1. Asymptotic Branch Step-Count Transfer to interpolationScale

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.auxDim_lt_self_of_two_le {n' : ℕ} (hn' : 2 ≤ n') : ReplacementParams.auxDim n' < n'

For 2 ≤ n', the Section 4.7 auxiliary dimension auxDim n' = r ^ (2 * Q) is strictly bounded by n' itself (since D ≤ 2 ^ (λ / 128) ≤ 2 ^ (λ - 1) < n').

2. Outer Loop Certificates and Global Polynomial Workspace

3. Public Branch Certificate, Polynomial Workspace, and Subexponential Runtime Bound

noncomputable def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.boundedIncidenceBranchCertificate : GenericRAM.NativeCertificate evalBoundedIncidenceBranch encBranchEvalInput Turing.MultiTapeTM.encNat

Proposition 5.3 native branch certificate: uniform multi-tape Turing machine resource certificate for evalBoundedIncidenceBranch on encBranchEvalInput (OpenAI, The Exponential Time Hypothesis is False, §§5.3–5.5, Proposition 5.3, pp. 37–39).

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.polyBounded_boundedIncidenceBranchCertificate_space : Turing.MultiTapeTM.PolyBounded (fun (x : BranchEvalInput) => (encBranchEvalInput x).length) boundedIncidenceBranchCertificate.space

Global polynomial workspace bound: boundedIncidenceBranchCertificate.space is polynomially bounded in (encBranchEvalInput x).length across all raw BranchEvalInput tuples x (including malformed or unfeasible inputs).

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.exists_boundedIncidenceBranchCertificate_time_bound (N₀_branch k_deg β C_inc : ℕ) : ∃ (N₀_br : ℕ) (C_br : ℕ) (d_br : ℕ) (A_br : ℕ), ∀ (n' : ℕ) (sys' : List (List (List ℕ))), checkBranchFeasible N₀_branch (n', sys') = true → N₀_br ≤ n' → sysMaxDegree sys' ≤ k_deg → sys'.length ≤ C_inc * n' → branchMaxFactorIncidence n' sys' ≤ C_inc * Nat.clog 2 n' ^ β → branchMaxFactorWidth n' sys' ≤ C_inc * Nat.clog 2 n' ^ β → ↑(boundedIncidenceBranchCertificate.time (prepareBranchEvalInput (n', sys'))) ≤ ↑C_br * (↑((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)))) (n', sys')).length + 1) ^ d_br * 2 ^ (↑A_br * interpolationScale n')

Proposition 5.3 subexponential branch runtime bound: for every degree bound k_deg, polylogarithmic exponent β, and constant C_inc, above N₀_br, every feasible reduced branch (n', sys') with sysMaxDegree sys' ≤ k_deg, sys'.length ≤ C_inc * n', and neutral-augmented factor incidence and scope width at most C_inc * (Nat.clog 2 n') ^ β runs in O^*(2^{O(interpolationScale n')}) native TM steps.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.branchPolylogTimeBound_boundedIncidenceBranchCertificate (N₀_branch : ℕ) : BranchedSparseCNFCounter.BranchPolylogTimeBound N₀_branch boundedIncidenceBranchCertificate

Instantiation of BranchPolylogTimeBound: boundedIncidenceBranchCertificate satisfies Cslib.Complexity.BranchedSparseCNFCounter.BranchPolylogTimeBound for every N₀_branch.