Native Step and Measurement-Payload Certificates for Bounded-Incidence Branch Evaluation

This file establishes polynomial-time stage certificates and uniform ComputableInO / PolyBounded-workspace bounds for the inner group-cube and two-pass measurement-fiber payload evaluators of the bounded-incidence $\mathbb{F}_2$ polynomial-system branch algorithm of OpenAI, The Exponential Time Hypothesis is False (§3.3, Lemma 3.2, p. 23; §§5.3–5.4, Proposition 5.3, pp. 37–38; Appendix B.2–B.3, pp. 48–50).

Specifically, we define explicit bit-list encodings for the closed stage contexts GroupEvalCtx, MeasStepCtx, and SubsetStepCtx, certify validBranchEvalParams, validDesignShape, and evalGroupFactorJet in polynomial time, and compose BooleanMeasurements.searchCertificate (Pass 1) with CommonCountingAccum.computableInO_streamGroupJetSum and CommonCountingAccum.computableInPolyTime_prodJet (Pass 2) across the $r_u$ variable groups to certify the per-measurement-word payload evalMeasPayload in $O\bigl((r_u (2^{d_{\max}} + 1) + 1) \cdot \operatorname{poly}(|\mathrm{input}|)\bigr)$ time and globally polynomial workspace.

Main definitions

• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.encGroupEvalCtx, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.encMeasStepCtx, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.encSubsetStepCtx: bit-list encodings for the closed step contexts of CommonCountingAccum.streamGroupJetSum, MeasurementFold.run, and SubsetPairFold.run.
• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.maxGroupDim, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.maxAllGroupDim: unary-clamped maximum variable-group dimensions at a single interpolation node and across all $Q_u$ nodes.
• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.evalMeasPayload: standalone two-pass measurement-word payload returning some prodJet when all $r_u$ group fibers are nonempty and none otherwise.

Main results

• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_validBranchEvalParams, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_validDesignShape, Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_evalGroupFactorJet: polynomial-time certificates for the entry guard, design-shape guard, and restricted local-cube group factor-jet summand.
• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.measurementStepBody_eq: decomposition of measurementStepBody through evalMeasPayload and Option.elim.
• Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.exists_computableInO_measPayload: uniform ComputableInO time and PolyBounded workspace bound for evalMeasPayload.

References

• OpenAI, The Exponential Time Hypothesis is False, §3.3 (Lemma 3.2, p. 23), §§5.3–5.4 (Proposition 5.3, pp. 37–38), and Appendix B.2–B.3 (pp. 48–50).

1. Stage Encodings and Polynomial-Time Step Helpers

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.encGroupEvalCtx : GroupEvalCtx ↪ List Bool

Bit-list encoding for GroupEvalCtx, encoding (n', J, ℓ, k') in unary, (node, dDen) and measurement vectors in signed binary, bit masks via encBits, and precollected group equations with replacement-row tables as nested lists.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.encMeasStepCtx : MeasStepCtx ↪ List Bool

Bit-list encoding for MeasStepCtx, encoding (n', r_u, m_rows) and (J, ℓ, k') in unary together with node parameters, per-group variable/measurement slices, subset bit masks, and precollected group equations.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.encSubsetStepCtx : SubsetStepCtx ↪ List Bool

Bit-list encoding for SubsetStepCtx, encoding (n', r_u, m_rows) and (J, ℓ, k') in unary, (c_meas, D_cap) as (encUnary, encNat), and the fixed per-node group and equation tables.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_validBranchEvalParams : Turing.MultiTapeTM.ComputableInPolyTime validBranchEvalParams encBranchEvalInput Turing.MultiTapeTM.encBool

validBranchEvalParams is computable in polynomial time on encBranchEvalInput.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_validDesignShape {α : Type} {encIn : α ↪ List Bool} {n' r_u m_eq : α → ℕ} {data : α → LinearAlgebra.ReplacementDesignData} (hn' : Turing.MultiTapeTM.ComputableInPolyTime n' encIn Turing.MultiTapeTM.encUnary) (hru : Turing.MultiTapeTM.ComputableInPolyTime r_u encIn Turing.MultiTapeTM.encUnary) (hmeq : Turing.MultiTapeTM.ComputableInPolyTime m_eq encIn Turing.MultiTapeTM.encUnary) (hdata : Turing.MultiTapeTM.ComputableInPolyTime data encIn LinearAlgebra.encReplacementDesignData) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => validDesignShape (n' x) (r_u x) (m_eq x) (data x)) encIn Turing.MultiTapeTM.encBool

validDesignShape is computable in polynomial time when (n', r_u, m_eq) are given in unary and data is encoded via encReplacementDesignData.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.computableInPolyTime_evalGroupFactorJet : Turing.MultiTapeTM.ComputableInPolyTime evalGroupFactorJet (Turing.MultiTapeTM.encPair encGroupEvalCtx (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

evalGroupFactorJet is computable in polynomial time on encPair encGroupEvalCtx (encPair encUnary encBits), matching the body-certificate obligation of CommonCountingAccum.computableInO_streamGroupJetSum.

2. Bounded-Range Loop Combinators and Measurement-Payload Certificate

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.maxGroupDim (n' r_u : ℕ) (vGroups_t : List (List ℕ)) : ℕ

Maximum unary-clamped variable-group dimension min (2 * n') |V_{t,g}| across g < r_u at a fixed interpolation node t.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.maxAllGroupDim (n' Q_u r_u : ℕ) (varGroups : List (List (List ℕ))) : ℕ

Maximum unary-clamped variable-group dimension across all nodes t < Q_u and groups g < r_u.

def Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.evalMeasPayload (wc : List ℤ × MeasStepCtx) : Option JetRows

Standalone per-measurement-word two-pass payload: slices word across the r_u variable groups, searches each unrestricted group fiber via BooleanMeasurements.search (Pass 1), and when every fiber is nonempty streams restricted local-cube factor-jet sums via CommonCountingAccum.streamGroupJetSum and returns some (prodJet J ℓ groupJets) (Pass 2).

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.measurementStepBody_eq (inp : ((ℕ × ℕ) × List ℤ) × MeasStepCtx × JetRows) : measurementStepBody inp = (evalMeasPayload (inp.1.2, inp.2.1)).elim inp.2 fun (y : JetRows) => (inp.2.1, addJet inp.2.1.2.1.1 inp.2.1.2.1.2.1 inp.2.2 y)

measurementStepBody factors into evalMeasPayload followed by optional addJet accumulation.

theorem Cslib.Complexity.SubexponentialSAT.SparsePolyCounter.exists_computableInO_measPayload : ∃ (P : List ℤ × MeasStepCtx → ℕ), Turing.MultiTapeTM.PolyBounded (fun (wc : List ℤ × MeasStepCtx) => ((Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) encMeasStepCtx) wc).length) P ∧ Turing.MultiTapeTM.ComputableInO evalMeasPayload (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) encMeasStepCtx) (Turing.MultiTapeTM.encOption (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (fun (wc : List ℤ × MeasStepCtx) => (wc.2.1.2.1 * (2 ^ maxGroupDim wc.2.1.1 wc.2.1.2.1 wc.2.2.2.2.1.1 + 1) + 1) * P wc) P

Uniform ComputableInO runtime and global PolyBounded workspace bound for evalMeasPayload, running in (r_u * (2 ^ maxGroupDim + 1) + 1) * P steps and P workspace.