Streaming group-sum and outer Taylor-jet accumulators with Cramer recovery

Proposition 3.4 (§3.3–3.5, pp. 22–26), Proposition 5.3 (§5.3–5.4, pp. 37–38), and Appendix B.2–B.3 (pp. 48–50) of OpenAI, The Exponential Time Hypothesis is False evaluate H_t(z) = H(t + z) mod z^J over ℚ[V]/(V^ℓ)[z]/(z^J) in streaming stages over fixed-denominator J × ℓ integer arrays (JetRows), followed by confluent Hermite Cramer recovery.

toJetTable, ofJetTable, taylorOuterVJet, groupSumBody, streamGroupJetSumPrefix, combineOuterRound, outerAccumBody, and streamOuterJetAccumPrefix provide unencoded algebraic and prefix-fold specifications (JetRows ↔ JetTable J ℓ ℤ, R[T][V] →+* JetTable J ℓ R), whereas extractCoordNodeJets, extractAllCoordNodeJets, prodJet, weightedProdJet, and recoverOuterJetSumModPowTwo carry plain ComputableInPolyTime (@[fun_prop]) certificates, and streamGroupJetSum / streamOuterJetAccum carry uniform NativeCertificate, ComputableInO, and plain ComputableInPolySpace bounds (never claiming whole-loop PolyTime). Out-of-range entry and node lookups return 0 and []; ofJetTable returns [] for J = 0 and List.replicate J [] for ℓ = 0; prodJet returns constJet J ℓ 1 on []; weightedProdJet returns zeroJet J ℓ when w = 0; clearing theorems hold in any CommRing K; and Cramer recovery requires Ω ≠ 0 and nodes.Nodup, returning 0 via Int.ediv when Ω = 0, ℓ = 0, or detRows = 0.

Main definitions

• Cslib.CommonCountingAccum.toJetTable, Cslib.CommonCountingAccum.ofJetTable, Cslib.CommonCountingAccum.taylorOuterVJet: JetRows ↔ JetTable J ℓ ℤ bridge and Taylor-jet homomorphism R[T][V] →+* JetTable J ℓ R.
• Cslib.CommonCountingAccum.extractCoordNodeJets, Cslib.CommonCountingAccum.prodJet, Cslib.CommonCountingAccum.weightedProdJet, Cslib.CommonCountingAccum.extractAllCoordNodeJets: per-coordinate Q × J node-jet slicing, truncated r-fold Cauchy product, and scalar weighting.
• Cslib.CommonCountingAccum.streamGroupJetSum, Cslib.CommonCountingAccum.groupJetSumCertificate, Cslib.CommonCountingAccum.streamOuterJetAccum, Cslib.CommonCountingAccum.outerJetAccumCertificate: streaming 2 ^ d group sum (BooleanFold) and T_rounds outer round accumulator (IndexFold) with uniform NativeCertificates.
• Cslib.CommonCountingAccum.recoverOuterJetSumModPowTwo: multi-coordinate Hermite Cramer count recovery (∑_{u < ℓ} H_u(0)).modPowTwo ℓ across Q evaluation nodes.

Main results

• Cslib.CommonCountingAccum.toJetTable_ofJetTable, Cslib.CommonCountingAccum.ofJetTable_toJetTable, Cslib.CommonCountingAccum.length_encJetRows_le_of_l1Norm_le, Cslib.CommonCountingAccum.rowEntry_extractCoordNodeJets_eq_taylor, Cslib.CommonCountingAccum.cast_prodJet_ofFn_cleared, Cslib.CommonCountingAccum.computableInPolyTime_prodJet: Stage-2 bridge, clearing, & PolyTime.
• Cslib.CommonCountingAccum.cast_streamGroupJetSum_cleared, Cslib.CommonCountingAccum.toJetTable_prodJet_streamGroupJetSum, Cslib.CommonCountingAccum.length_encJetRows_streamGroupJetSumPrefix_le, Cslib.CommonCountingAccum.computableInO_streamGroupJetSum, Cslib.CommonCountingAccum.computableInPolySpace_streamGroupJetSum: Stage-3 local group sum.
• Cslib.CommonCountingAccum.cast_streamOuterJetAccum_taylorOuterVJet, Cslib.CommonCountingAccum.length_encJetRows_streamOuterJetAccumPrefix_le, Cslib.CommonCountingAccum.computableInO_outerJetAccumCertificate, Cslib.CommonCountingAccum.computableInPolySpace_streamOuterJetAccum: Stage-4 outer accumulation.
• Cslib.CommonCountingAccum.hermiteRecoverZero_extractCoordNodeJets_eq, Cslib.CommonCountingAccum.recoverOuterJetSumModPowTwo_eq, Cslib.CommonCountingAccum.recoverOuterJetSumModPowTwo_streamOuterJetAccum_eq, Cslib.CommonCountingAccum.computableInPolyTime_recoverOuterJetSumModPowTwo: Cramer recovery.

References

• OpenAI, The Exponential Time Hypothesis is False, §3.3–3.5, §5.3–5.4, B.2–B.3

1. JetRows ↔ JetTable bridge, taylorOuterVJet, node slicing, and prodJet

def Cslib.CommonCountingAccum.toJetTable (J ℓ : ℕ) (A : JetRows) : JetTable J ℓ ℤ

Interpret A : JetRows as a (J × ℓ) JetTable via Cslib.rowEntry (out-of-range = 0).

@[simp]

theorem Cslib.CommonCountingAccum.toJetTable_apply (J ℓ : ℕ) (A : JetRows) (j : Fin J) (u : Fin ℓ) : toJetTable J ℓ A j u = rowEntry A ↑j ↑u

def Cslib.CommonCountingAccum.ofJetTable {J ℓ : ℕ} (T : JetTable J ℓ ℤ) : JetRows

Tabulate T : JetTable J ℓ ℤ into a dense (J × ℓ) integer table ([] when J = 0, and List.replicate J [] when ℓ = 0).

theorem Cslib.CommonCountingAccum.isTableShape_ofJetTable {J ℓ : ℕ} (T : JetTable J ℓ ℤ) : IsTableShape J ℓ (ofJetTable T)

@[simp]

theorem Cslib.CommonCountingAccum.ofJetTable_zero_rows {ℓ : ℕ} (T : JetTable 0 ℓ ℤ) : ofJetTable T = []

@[simp]

theorem Cslib.CommonCountingAccum.ofJetTable_zero_cols {J : ℕ} (T : JetTable J 0 ℤ) : ofJetTable T = List.replicate J []

theorem Cslib.CommonCountingAccum.rowEntry_ofJetTable_of_lt {J ℓ : ℕ} (T : JetTable J ℓ ℤ) {j u : ℕ} (hj : j < J) (hu : u < ℓ) : rowEntry (ofJetTable T) j u = T ⟨j, hj⟩ ⟨u, hu⟩

@[simp]

theorem Cslib.CommonCountingAccum.toJetTable_ofJetTable {J ℓ : ℕ} (T : JetTable J ℓ ℤ) : toJetTable J ℓ (ofJetTable T) = T

theorem Cslib.CommonCountingAccum.ofJetTable_toJetTable {J ℓ : ℕ} {A : JetRows} (hA : IsTableShape J ℓ A) : ofJetTable (toJetTable J ℓ A) = A

theorem Cslib.CommonCountingAccum.eq_of_isTableShape_of_toJetTable_eq {J ℓ : ℕ} {A B : JetRows} (hA : IsTableShape J ℓ A) (hB : IsTableShape J ℓ B) (h : toJetTable J ℓ A = toJetTable J ℓ B) : A = B

@[simp]

theorem Cslib.CommonCountingAccum.toJetTable_zeroJet (J ℓ : ℕ) : toJetTable J ℓ (zeroJet J ℓ) = 0

theorem Cslib.CommonCountingAccum.toJetTable_constJet (J ℓ : ℕ) (c : ℤ) : toJetTable J ℓ (constJet J ℓ c) = JetTable.const c

@[simp]

theorem Cslib.CommonCountingAccum.toJetTable_constJet_one (J ℓ : ℕ) : toJetTable J ℓ (constJet J ℓ 1) = 1

@[simp]

theorem Cslib.CommonCountingAccum.toJetTable_addJet (J ℓ : ℕ) (A B : JetRows) : toJetTable J ℓ (addJet J ℓ A B) = toJetTable J ℓ A + toJetTable J ℓ B

@[simp]

theorem Cslib.CommonCountingAccum.toJetTable_smulJet (J ℓ : ℕ) (c : ℤ) (A : JetRows) : toJetTable J ℓ (smulJet J ℓ c A) = c • toJetTable J ℓ A

@[simp]

theorem Cslib.CommonCountingAccum.toJetTable_convJet (J ℓ : ℕ) (A B : JetRows) : toJetTable J ℓ (convJet J ℓ A B) = toJetTable J ℓ A * toJetTable J ℓ B

theorem Cslib.CommonCountingAccum.l1Norm_toJetTable_eq {J ℓ : ℕ} {A : JetRows} (hA : IsTableShape J ℓ A) : (toJetTable J ℓ A).l1Norm = jetL1Norm A

theorem Cslib.CommonCountingAccum.length_encJetRows_le_of_size_le {J ℓ b : ℕ} {A : JetRows} (hA : IsTableShape J ℓ A) (hb : ∀ j < J, ∀ u < ℓ, (rowEntry A j u).natAbs.size ≤ b) : ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) A).length ≤ J * (2 * (ℓ * (2 * b + 3)) + 1)

Encoded bit-length bound for (J, ℓ)-shaped A (hA) with entry natAbs.size ≤ b.

theorem Cslib.CommonCountingAccum.length_encJetRows_le_of_natAbs_le {J ℓ M : ℕ} {A : JetRows} (hA : IsTableShape J ℓ A) (hM : ∀ j < J, ∀ u < ℓ, (rowEntry A j u).natAbs ≤ M) : ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) A).length ≤ J * (2 * (ℓ * (2 * M.size + 3)) + 1)

theorem Cslib.CommonCountingAccum.length_encJetRows_le_of_l1Norm_le {J ℓ L : ℕ} {A : JetRows} (hA : IsTableShape J ℓ A) (hL : (toJetTable J ℓ A).l1Norm ≤ L) : ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) A).length ≤ J * (2 * (ℓ * (2 * L.size + 3)) + 1)

Encoded bit-length bound from (toJetTable J ℓ A).l1Norm ≤ L under IsTableShape J ℓ A.

theorem Cslib.CommonCountingAccum.size_natAbs_le_length_encJetRows {A : JetRows} {row : List ℤ} (hrow : row ∈ A) {z : ℤ} (hz : z ∈ row) : z.natAbs.size ≤ ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) A).length

theorem Cslib.CommonCountingAccum.size_natAbs_rowEntry_le_length_encJetRows (A : JetRows) (j u : ℕ) : (rowEntry A j u).natAbs.size ≤ ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) A).length

noncomputable def Cslib.CommonCountingAccum.taylorOuterVJet (J ℓ : ℕ) {R : Type u_1} [CommRing R] (t : R) : Polynomial (Polynomial R) →+* JetTable J ℓ R

Taylor jet extraction homomorphism R[T][V] →+* JetTable J ℓ R at node t : R (outer indeterminate V, inner indeterminate T).

@[simp]

theorem Cslib.CommonCountingAccum.taylorOuterVJet_apply (J ℓ : ℕ) {R : Type u_1} [CommRing R] (t : R) (P : Polynomial (Polynomial R)) (j : Fin J) (u : Fin ℓ) : (taylorOuterVJet J ℓ t) P j u = ((Polynomial.taylor t) (P.coeff ↑u)).coeff ↑j

def Cslib.CommonCountingAccum.extractCoordNodeJets (J u : ℕ) (nodeJets : List JetRows) : JetRows

Extract the nodeJets.length × J Taylor-jet table at V ^ u across per-node J × ℓ arrays nodeJets, indexed (nodeIdx, derivOrder) (out-of-range node/entry lookups default to []/0; OpenAI, The Exponential Time Hypothesis is False, Appendix B.3, p. 50).

def Cslib.CommonCountingAccum.extractAllCoordNodeJets (J ℓ : ℕ) (nodeJets : List JetRows) : List JetRows

Extract all ℓ per-coordinate nodeJets.length × J Taylor-jet tables (u = 0, …, ℓ - 1).

theorem Cslib.CommonCountingAccum.isTableShape_extractCoordNodeJets (J u : ℕ) (nodeJets : List JetRows) : IsTableShape nodeJets.length J (extractCoordNodeJets J u nodeJets)

@[simp]

theorem Cslib.CommonCountingAccum.length_extractAllCoordNodeJets (J ℓ : ℕ) (nodeJets : List JetRows) : (extractAllCoordNodeJets J ℓ nodeJets).length = ℓ

theorem Cslib.CommonCountingAccum.rowEntry_extractCoordNodeJets_of_lt (J u : ℕ) (nodeJets : List JetRows) {i j : ℕ} (hi : i < nodeJets.length) (hj : j < J) : rowEntry (extractCoordNodeJets J u nodeJets) i j = rowEntry nodeJets[i] j u

theorem Cslib.CommonCountingAccum.rowEntry_extractCoordNodeJets_eq_taylor {J ℓ : ℕ} {K : Type u_1} [CommRing K] (Ω : ℤ) (nodes : List ℤ) (nodeJets : List JetRows) (hlen : nodeJets.length = nodes.length) (P : Polynomial (Polynomial K)) (hclear : ∀ (i : Fin nodes.length), Ω • (taylorOuterVJet J ℓ ↑nodes[i]) P = (JetTable.castRingHom K) (toJetTable J ℓ nodeJets[↑i])) (u : Fin ℓ) (i : Fin nodes.length) (j : Fin J) : ↑(rowEntry (extractCoordNodeJets J (↑u) nodeJets) ↑i ↑j) = ↑Ω * ((Polynomial.taylor ↑nodes[i]) (P.coeff ↑u)).coeff ↑j

Under hlen and hclear, extractCoordNodeJets gives the Ω-scaled (i, j) Taylor coefficients of P.coeff u (unconditional in K).

theorem Cslib.CommonCountingAccum.computableInPolyTime_extractCoordNodeJets {α : Type} {encIn : α ↪ List Bool} {J u : α → ℕ} {nodeJets : α → List JetRows} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hu : Turing.MultiTapeTM.ComputableInPolyTime u encIn Turing.MultiTapeTM.encUnary) (hnodeJets : Turing.MultiTapeTM.ComputableInPolyTime nodeJets encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => extractCoordNodeJets (J x) (u x) (nodeJets x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

theorem Cslib.CommonCountingAccum.computableInPolyTime_extractAllCoordNodeJets {α : Type} {encIn : α ↪ List Bool} {J ℓ : α → ℕ} {nodeJets : α → List JetRows} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hnodeJets : Turing.MultiTapeTM.ComputableInPolyTime nodeJets encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => extractAllCoordNodeJets (J x) (ℓ x) (nodeJets x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))

def Cslib.CommonCountingAccum.prodJet (J ℓ : ℕ) (factors : List JetRows) : JetRows

Truncated r-fold product in ℤ[V]/(V^ℓ)[z]/(z^J) from constJet J ℓ 1 (OpenAI, The Exponential Time Hypothesis is False, eq. (3.11) and Appendix B.2, p. 49; returns constJet J ℓ 1 on []).

@[simp]

theorem Cslib.CommonCountingAccum.prodJet_nil (J ℓ : ℕ) : prodJet J ℓ [] = constJet J ℓ 1

theorem Cslib.CommonCountingAccum.isTableShape_prodJet (J ℓ : ℕ) (factors : List JetRows) : IsTableShape J ℓ (prodJet J ℓ factors)

@[simp]

theorem Cslib.CommonCountingAccum.toJetTable_prodJet (J ℓ : ℕ) (factors : List JetRows) : toJetTable J ℓ (prodJet J ℓ factors) = (List.map (toJetTable J ℓ) factors).prod

theorem Cslib.CommonCountingAccum.jetL1Norm_prodJet_le (J ℓ : ℕ) (factors : List JetRows) : jetL1Norm (prodJet J ℓ factors) ≤ (List.map jetL1Norm factors).prod

theorem Cslib.CommonCountingAccum.cast_prodJet_ofFn_cleared {J ℓ r m_test : ℕ} {K : Type u_1} [CommRing K] (Γ : ℤ) (m_group : Fin r → ℕ) (hm : ∑ g : Fin r, m_group g = m_test) (S_rat : Fin r → JetTable J ℓ K) (S_int : Fin r → JetRows) (hS : ∀ (g : Fin r), Γ ^ m_group g • S_rat g = (JetTable.castRingHom K) (toJetTable J ℓ (S_int g))) : Γ ^ m_test • ∏ g : Fin r, S_rat g = (JetTable.castRingHom K) (toJetTable J ℓ (prodJet J ℓ (List.ofFn S_int)))

Product denominator clearing (prodJet over Fin r) under ∑ g, m_group g = m_test (eq. (3.11) and Appendix B.2, p. 49; unconditional in K).

theorem Cslib.CommonCountingAccum.size_natAbs_rowEntry_prodJet_le {J ℓ b : ℕ} {factors : List JetRows} (hf : ∀ F ∈ factors, ∀ row ∈ F, ∀ z ∈ row, z.natAbs.size ≤ b) (j u : ℕ) : (rowEntry (prodJet J ℓ factors) j u).natAbs.size ≤ 1 + factors.length * (b + (J * ℓ).size)

theorem Cslib.CommonCountingAccum.computableInPolyTime_prodJet {α : Type} {encIn : α ↪ List Bool} {J ℓ : α → ℕ} {factors : α → List JetRows} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hfactors : Turing.MultiTapeTM.ComputableInPolyTime factors encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => prodJet (J x) (ℓ x) (factors x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

def Cslib.CommonCountingAccum.weightedProdJet (J ℓ : ℕ) (w : ℤ) (groups : List JetRows) : JetRows

Multiply groups modulo (z^J, V^ℓ) and scale by w : ℤ (zeroJet J ℓ when w = 0; OpenAI, The Exponential Time Hypothesis is False, eq. (3.13)).

theorem Cslib.CommonCountingAccum.isTableShape_weightedProdJet (J ℓ : ℕ) (w : ℤ) (groups : List JetRows) : IsTableShape J ℓ (weightedProdJet J ℓ w groups)

@[simp]

theorem Cslib.CommonCountingAccum.toJetTable_weightedProdJet (J ℓ : ℕ) (w : ℤ) (groups : List JetRows) : toJetTable J ℓ (weightedProdJet J ℓ w groups) = w • (List.map (toJetTable J ℓ) groups).prod

theorem Cslib.CommonCountingAccum.jetL1Norm_weightedProdJet_le (J ℓ : ℕ) (w : ℤ) (groups : List JetRows) : jetL1Norm (weightedProdJet J ℓ w groups) ≤ w.natAbs * (List.map jetL1Norm groups).prod

theorem Cslib.CommonCountingAccum.computableInPolyTime_weightedProdJet {α : Type} {encIn : α ↪ List Bool} {J ℓ : α → ℕ} {w : α → ℤ} {groups : α → List JetRows} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hw : Turing.MultiTapeTM.ComputableInPolyTime w encIn Turing.MultiTapeTM.encIntBin) (hgroups : Turing.MultiTapeTM.ComputableInPolyTime groups encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => weightedProdJet (J x) (ℓ x) (w x) (groups x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Shared additive-fold and IndexFold certificate helpers

theorem Cslib.CommonCountingAccum.foldl_keep_fst {ι : Type u_1} {π : Type u_2} {α : Type u_3} (step : π → α → ι → α) (par : π) (xs : List ι) (init : α) : List.foldl (fun (pa : π × α) (i : ι) => (pa.1, step pa.1 pa.2 i)) (par, init) xs = (par, List.foldl (step par) init xs)

def Cslib.CommonCountingAccum.HasPolySpace {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool} {f : α → β} (c : GenericRAM.NativeCertificate f ei eo) : Prop

A native certificate c has polynomially bounded workspace in the encoded input length.

theorem Cslib.CommonCountingAccum.polyBounded_length_of_hasPolySpace {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool} {f : α → β} {c : GenericRAM.NativeCertificate f ei eo} (hc : HasPolySpace c) : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (ei a).length) fun (a : α) => (eo (f a)).length

theorem Cslib.CommonCountingAccum.hasPolySpace_comp {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β} {g : β → γ} {d : GenericRAM.NativeCertificate g em eo} {c : GenericRAM.NativeCertificate f ei em} (hd : HasPolySpace d) (hc : HasPolySpace c) : HasPolySpace (d.comp c)

theorem Cslib.CommonCountingAccum.hasPolySpace_prod {α β γ : Type} {ei : α ↪ List Bool} {em : β ↪ List Bool} {eo : γ ↪ List Bool} {f : α → β} {g : α → γ} {c : GenericRAM.NativeCertificate f ei em} {d : GenericRAM.NativeCertificate g ei eo} (hc : HasPolySpace c) (hd : HasPolySpace d) : HasPolySpace (c.prod d)

theorem Cslib.CommonCountingAccum.exists_natAbs_rowEntry_le_two_pow {ι γ : Type} {sz : ι → ℕ} {encΓ : γ ↪ List Bool} {f : γ → JetRows} {L : ι → ℕ} (hf : Turing.MultiTapeTM.PolyBounded (fun (y : γ) => (encΓ y).length) fun (y : γ) => ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (f y)).length) (hL : Turing.MultiTapeTM.PolyBounded sz L) : ∃ (M : ι → ℕ), Turing.MultiTapeTM.PolyBounded sz M ∧ ∀ (x : ι) (y : γ), (encΓ y).length ≤ L x → ∀ (j u : ℕ), (rowEntry (f y) j u).natAbs ≤ 2 ^ M x

theorem Cslib.CommonCountingAccum.computableInO_snd_indexFold {ι β : Type} {encIn : ι ↪ List Bool} {encB : β ↪ List Bool} {count : ι → ℕ} {initial : ι → β} {body : ℕ × β → β} (cn : GenericRAM.NativeCertificate count encIn Turing.MultiTapeTM.encNat) (ci : GenericRAM.NativeCertificate initial encIn encB) (cb : GenericRAM.NativeCertificate body (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encB) encB) (hcn : cn.IsPolynomial) (hci : ci.IsPolynomial) (hcb : HasPolySpace cb) {B : ι → ℕ} (hB_pb : Turing.MultiTapeTM.PolyBounded (fun (x : ι) => (encIn x).length) B) (hB : ∀ (x : ι), ∀ j ≤ count x, (encB (GenericRAM.IndexFold.run body j (initial x)).2).length ≤ B x) (R P_cb : ι → ℕ) (hP_cb : Turing.MultiTapeTM.PolyBounded (fun (x : ι) => (encIn x).length) P_cb) (hR : ∀ (x : ι), ∀ j ≤ count x, ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encB) (GenericRAM.IndexFold.run body j (initial x))).length ≤ 2 * (Turing.MultiTapeTM.encNat (count x)).length + 1 + B x → cb.time (GenericRAM.IndexFold.run body j (initial x)) ≤ R x + P_cb x) : ∃ (P : ι → ℕ), Turing.MultiTapeTM.PolyBounded (fun (x : ι) => (encIn x).length) P ∧ Turing.MultiTapeTM.ComputableInO (fun (x : ι) => (GenericRAM.IndexFold.run body (count x) (initial x)).2) encIn encB (fun (x : ι) => (count x + 1) * (R x + P x)) P

noncomputable def Cslib.CommonCountingAccum.initJetStateCertificate {ι α : Type} {encIn : ι ↪ List Bool} {encCtx : α ↪ List Bool} {J ℓ : ι → ℕ} {ctx : ι → α} (cJ : GenericRAM.NativeCertificate J encIn Turing.MultiTapeTM.encUnary) (cℓ : GenericRAM.NativeCertificate ℓ encIn Turing.MultiTapeTM.encUnary) (cctx : GenericRAM.NativeCertificate ctx encIn encCtx) : GenericRAM.NativeCertificate (fun (x : ι) => (((J x, ℓ x), ctx x), zeroJet (J x) (ℓ x))) encIn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) encCtx) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))

Initial loop-state certificate pairing ((J, ℓ), ctx) with zeroJet J ℓ.

theorem Cslib.CommonCountingAccum.prepareAccumEval_polyTime {α ω : Type} {encCtx : α ↪ List Bool} {encΩ : ω ↪ List Bool} : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ω × ((ℕ × ℕ) × α) × JetRows) => (p.2.1.2, p.1)) (Turing.MultiTapeTM.encPair encΩ (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) encCtx) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) (Turing.MultiTapeTM.encPair encCtx encΩ)

@[reducible, inline]

abbrev Cslib.CommonCountingAccum.CombPoly {ρ : Type} (combine : ℕ × ℕ → JetRows → ρ → JetRows) (encΡ : ρ ↪ List Bool) : Prop

Polynomial-time combinator predicate for encoded accumulator updates.

theorem Cslib.CommonCountingAccum.applyAccumCombine_polyTime {α ω ρ : Type} {encCtx : α ↪ List Bool} {encΩ : ω ↪ List Bool} {encΡ : ρ ↪ List Bool} (combine : ℕ × ℕ → JetRows → ρ → JetRows) (hcomb : CombPoly combine encΡ) : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : (ω × ((ℕ × ℕ) × α) × JetRows) × ρ) => combine q.1.2.1.1 q.1.2.2 q.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encΩ (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) encCtx) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) encΡ) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

noncomputable def Cslib.CommonCountingAccum.accumStepBodyCertificate {α ω ρ : Type} {encCtx : α ↪ List Bool} {encΩ : ω ↪ List Bool} {encΡ : ρ ↪ List Bool} (combine : ℕ × ℕ → JetRows → ρ → JetRows) (hcomb : CombPoly combine encΡ) {cb_eval : α × ω → ρ} (ceval : GenericRAM.NativeCertificate cb_eval (Turing.MultiTapeTM.encPair encCtx encΩ) encΡ) : GenericRAM.NativeCertificate (fun (p : ω × ((ℕ × ℕ) × α) × JetRows) => (p.2.1, combine p.2.1.1 p.2.2 (cb_eval (p.2.1.2, p.1)))) (Turing.MultiTapeTM.encPair encΩ (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) encCtx) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) encCtx) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))

Generic single-step NativeCertificate updating the JetRows accumulator component.

2. Streaming local-Boolean group sum (streamGroupJetSum)

def Cslib.CommonCountingAccum.groupSumBody {α : Type} (evalGroupProd : α × ℕ × List Bool → JetRows) (p : (ℕ × List Bool) × ((ℕ × ℕ) × α) × JetRows) : ((ℕ × ℕ) × α) × JetRows

Single-assignment body for streamGroupJetSum: retains ((J, ℓ), ctx) and adds evalGroupProd (ctx, wd) via addJet.

def Cslib.CommonCountingAccum.streamGroupJetSumPrefix {α : Type} (evalGroupProd : α × ℕ × List Bool → JetRows) (J ℓ d j : ℕ) (ctx : α) : JetRows

Live (J × ℓ) jet accumulator after visiting the first j local-Boolean assignments.

def Cslib.CommonCountingAccum.streamGroupJetSum {α : Type} (evalGroupProd : α × ℕ × List Bool → JetRows) (J ℓ d : ℕ) (ctx : α) : JetRows

Streaming local-Boolean group sum over all 2 ^ d assignments of unary dimension d via BooleanFold.run (OpenAI, The Exponential Time Hypothesis is False, Lemma 3.2, Proposition 3.4, and Appendix B.2, p. 49).

theorem Cslib.CommonCountingAccum.streamGroupJetSumPrefix_eq_foldl {α : Type} (evalGroupProd : α × ℕ × List Bool → JetRows) (J ℓ d j : ℕ) (ctx : α) : streamGroupJetSumPrefix evalGroupProd J ℓ d j ctx = List.foldl (fun (acc : List (List ℤ)) (i : ℕ) => addJet J ℓ acc (evalGroupProd (ctx, d, BitString.lowBits d i))) (zeroJet J ℓ) (List.range j)

theorem Cslib.CommonCountingAccum.toJetTable_streamGroupJetSum_eq_sum {α : Type} (evalGroupProd : α × ℕ × List Bool → JetRows) (J ℓ d : ℕ) (ctx : α) : toJetTable J ℓ (streamGroupJetSum evalGroupProd J ℓ d ctx) = ∑ x : BitString d, toJetTable J ℓ (evalGroupProd (ctx, d, List.ofFn x))

theorem Cslib.CommonCountingAccum.isTableShape_streamGroupJetSumPrefix {α : Type} (evalGroupProd : α × ℕ × List Bool → JetRows) (J ℓ d j : ℕ) (ctx : α) : IsTableShape J ℓ (streamGroupJetSumPrefix evalGroupProd J ℓ d j ctx)

theorem Cslib.CommonCountingAccum.isTableShape_streamGroupJetSum {α : Type} (evalGroupProd : α × ℕ × List Bool → JetRows) (J ℓ d : ℕ) (ctx : α) : IsTableShape J ℓ (streamGroupJetSum evalGroupProd J ℓ d ctx)

theorem Cslib.CommonCountingAccum.length_encJetRows_streamGroupJetSumPrefix_le {α : Type} (evalGroupProd : α × ℕ × List Bool → JetRows) {J ℓ d j M_group : ℕ} (ctx : α) (hj : j ≤ 2 ^ d) (hM : ∀ (word : List Bool), word.length = d → ∀ j' < J, ∀ u' < ℓ, (rowEntry (evalGroupProd (ctx, d, word)) j' u').natAbs ≤ M_group) : ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (streamGroupJetSumPrefix evalGroupProd J ℓ d j ctx)).length ≤ J * (2 * (ℓ * (2 * (d + 1 + M_group.size) + 3)) + 1)

All-prefix encoded bit-length bound for streamGroupJetSumPrefix (Appendix B.2, p. 49).

theorem Cslib.CommonCountingAccum.cast_streamGroupJetSum_cleared {α : Type} {J ℓ d m_g : ℕ} {K : Type u_1} [CommRing K] (Γ : ℤ) (evalGroupProd : α × ℕ × List Bool → JetRows) (ctx : α) (A_rat : BitString d → JetTable J ℓ K) (hA : ∀ (x : BitString d), Γ ^ m_g • A_rat x = (JetTable.castRingHom K) (toJetTable J ℓ (evalGroupProd (ctx, d, List.ofFn x)))) : Γ ^ m_g • ∑ x : BitString d, A_rat x = (JetTable.castRingHom K) (toJetTable J ℓ (streamGroupJetSum evalGroupProd J ℓ d ctx))

Fixed-denominator clearing for streamGroupJetSum (Appendix B.2, p. 49, in CommRing K).

theorem Cslib.CommonCountingAccum.toJetTable_prodJet_streamGroupJetSum {α : Type} {J ℓ r : ℕ} (d : Fin r → ℕ) (evalGroup : Fin r → α × ℕ × List Bool → JetRows) (ctx : α) : toJetTable J ℓ (prodJet J ℓ (List.ofFn fun (g : Fin r) => streamGroupJetSum (evalGroup g) J ℓ (d g) ctx)) = ∑ x : (g : Fin r) → BitString (d g), ∏ g : Fin r, toJetTable J ℓ (evalGroup g (ctx, d g, List.ofFn (x g)))

Lemma 3.2 cross-group distributive factorization (OpenAI, The Exponential Time Hypothesis is False, §3.3, pp. 22–23).

theorem Cslib.CommonCountingAccum.combineGroupAdd_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (r : ((ℕ × ℕ) × JetRows) × JetRows) => addJet r.1.1.1 r.1.1.2 r.1.2 r.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

@[reducible, inline]

noncomputable abbrev Cslib.CommonCountingAccum.groupSumBodyCertificate {α : Type} {encCtx : α ↪ List Bool} {evalGroupProd : α × ℕ × List Bool → JetRows} (cprod : GenericRAM.NativeCertificate evalGroupProd (Turing.MultiTapeTM.encPair encCtx (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : GenericRAM.NativeCertificate (groupSumBody evalGroupProd) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) encCtx) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) encCtx) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))

Single-step BooleanFold body certificate for streamGroupJetSum.

noncomputable def Cslib.CommonCountingAccum.groupJetSumCertificate {ι α : Type} {encIn : ι ↪ List Bool} {encCtx : α ↪ List Bool} {J ℓ d : ι → ℕ} {ctx : ι → α} {evalGroupProd : α × ℕ × List Bool → JetRows} (cJ : GenericRAM.NativeCertificate J encIn Turing.MultiTapeTM.encUnary) (cℓ : GenericRAM.NativeCertificate ℓ encIn Turing.MultiTapeTM.encUnary) (cd : GenericRAM.NativeCertificate d encIn Turing.MultiTapeTM.encUnary) (cctx : GenericRAM.NativeCertificate ctx encIn encCtx) (cprod : GenericRAM.NativeCertificate evalGroupProd (Turing.MultiTapeTM.encPair encCtx (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : GenericRAM.NativeCertificate (fun (x : ι) => streamGroupJetSum evalGroupProd (J x) (ℓ x) (d x) (ctx x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Uniform NativeCertificate for streamGroupJetSum, built via BooleanFold.certificate.

theorem Cslib.CommonCountingAccum.computableInO_streamGroupJetSum {ι α : Type} {encIn : ι ↪ List Bool} {encCtx : α ↪ List Bool} {J ℓ d : ι → ℕ} {ctx : ι → α} {evalGroupProd : α × ℕ × List Bool → JetRows} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn Turing.MultiTapeTM.encUnary) (hctx : Turing.MultiTapeTM.ComputableInPolyTime ctx encIn encCtx) (hprod : Turing.MultiTapeTM.ComputableInPolyTime evalGroupProd (Turing.MultiTapeTM.encPair encCtx (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : ∃ (P : ι → ℕ), Turing.MultiTapeTM.PolyBounded (fun (x : ι) => (encIn x).length) P ∧ Turing.MultiTapeTM.ComputableInO (fun (x : ι) => streamGroupJetSum evalGroupProd (J x) (ℓ x) (d x) (ctx x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (fun (x : ι) => (2 ^ d x + 1) * P x) P

Explicit ComputableInO time O((2 ^ d + 1) * P) and space O(P) bound for streamGroupJetSum.

theorem Cslib.CommonCountingAccum.computableInPolySpace_streamGroupJetSum {ι α : Type} {encIn : ι ↪ List Bool} {encCtx : α ↪ List Bool} {J ℓ d : ι → ℕ} {ctx : ι → α} {evalGroupProd : α × ℕ × List Bool → JetRows} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn Turing.MultiTapeTM.encUnary) (hctx : Turing.MultiTapeTM.ComputableInPolyTime ctx encIn encCtx) (hprod : Turing.MultiTapeTM.ComputableInPolySpace evalGroupProd (Turing.MultiTapeTM.encPair encCtx (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : Turing.MultiTapeTM.ComputableInPolySpace (fun (x : ι) => streamGroupJetSum evalGroupProd (J x) (ℓ x) (d x) (ctx x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Plain ComputableInPolySpace guarantee for streamGroupJetSum.

3. Cross-group r-fold product and outer round accumulator (streamOuterJetAccum)

def Cslib.CommonCountingAccum.combineOuterRound (J ℓ : ℕ) (acc : JetRows) (wy : ℤ × List JetRows) : JetRows

Add weightedProdJet J ℓ wy.1 wy.2 into acc (ℤ × List JetRows round payload combiner).

def Cslib.CommonCountingAccum.outerAccumBody {α : Type} (evalRound : α × ℕ → ℤ × List JetRows) (p : ℕ × ((ℕ × ℕ) × α) × JetRows) : ((ℕ × ℕ) × α) × JetRows

Single-round body for streamOuterJetAccum (eq. (3.13) and Appendix B.2, p. 49).

def Cslib.CommonCountingAccum.streamOuterJetAccumPrefix {α : Type} (evalRound : α × ℕ → ℤ × List JetRows) (J ℓ j : ℕ) (ctx : α) : JetRows

Live (J × ℓ) jet accumulator after the first j outer rounds (T_j(z, V)).

def Cslib.CommonCountingAccum.streamOuterJetAccum {α : Type} (evalRound : α × ℕ → ℤ × List JetRows) (J ℓ T_rounds : ℕ) (ctx : α) : JetRows

Streaming outer round accumulator over T_rounds binary-indexed steps via IndexFold.run (OpenAI, The Exponential Time Hypothesis is False, Proposition 3.4 eq. (3.13) and Appendix B.2, pp. 49–50).

theorem Cslib.CommonCountingAccum.streamOuterJetAccumPrefix_eq_foldl {α : Type} (evalRound : α × ℕ → ℤ × List JetRows) (J ℓ j : ℕ) (ctx : α) : streamOuterJetAccumPrefix evalRound J ℓ j ctx = List.foldl (fun (acc : List (List ℤ)) (idx : ℕ) => addJet J ℓ acc (weightedProdJet J ℓ (evalRound (ctx, idx)).1 (evalRound (ctx, idx)).2)) (zeroJet J ℓ) (List.range j)

@[simp]

theorem Cslib.CommonCountingAccum.streamOuterJetAccum_zero {α : Type} (evalRound : α × ℕ → ℤ × List JetRows) (J ℓ : ℕ) (ctx : α) : streamOuterJetAccum evalRound J ℓ 0 ctx = zeroJet J ℓ

theorem Cslib.CommonCountingAccum.toJetTable_streamOuterJetAccumPrefix {α : Type} (evalRound : α × ℕ → ℤ × List JetRows) (J ℓ j : ℕ) (ctx : α) : toJetTable J ℓ (streamOuterJetAccumPrefix evalRound J ℓ j ctx) = ∑ idx ∈ Finset.range j, (evalRound (ctx, idx)).1 • (List.map (toJetTable J ℓ) (evalRound (ctx, idx)).2).prod

theorem Cslib.CommonCountingAccum.toJetTable_streamOuterJetAccum {α : Type} (evalRound : α × ℕ → ℤ × List JetRows) (J ℓ T_rounds : ℕ) (ctx : α) : toJetTable J ℓ (streamOuterJetAccum evalRound J ℓ T_rounds ctx) = ∑ idx ∈ Finset.range T_rounds, (evalRound (ctx, idx)).1 • (List.map (toJetTable J ℓ) (evalRound (ctx, idx)).2).prod

theorem Cslib.CommonCountingAccum.isTableShape_streamOuterJetAccumPrefix {α : Type} (evalRound : α × ℕ → ℤ × List JetRows) (J ℓ j : ℕ) (ctx : α) : IsTableShape J ℓ (streamOuterJetAccumPrefix evalRound J ℓ j ctx)

theorem Cslib.CommonCountingAccum.isTableShape_streamOuterJetAccum {α : Type} (evalRound : α × ℕ → ℤ × List JetRows) (J ℓ T_rounds : ℕ) (ctx : α) : IsTableShape J ℓ (streamOuterJetAccum evalRound J ℓ T_rounds ctx)

theorem Cslib.CommonCountingAccum.length_encJetRows_streamOuterJetAccumPrefix_le {α : Type} (evalRound : α × ℕ → ℤ × List JetRows) {J ℓ T_rounds j M_prod : ℕ} (ctx : α) (hj : j ≤ T_rounds) (hM : ∀ idx < T_rounds, ∀ j' < J, ∀ u' < ℓ, (rowEntry (weightedProdJet J ℓ (evalRound (ctx, idx)).1 (evalRound (ctx, idx)).2) j' u').natAbs ≤ M_prod) : ((Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (streamOuterJetAccumPrefix evalRound J ℓ j ctx)).length ≤ J * (2 * (ℓ * (2 * ((Turing.MultiTapeTM.encNat T_rounds).length + M_prod.size) + 3)) + 1)

All-prefix bit-length bound for streamOuterJetAccumPrefix (Appendix B.2, pp. 49–50).

theorem Cslib.CommonCountingAccum.cast_streamOuterJetAccum_cleared {α : Type} {J ℓ r m T_rounds : ℕ} {K : Type u_1} [CommRing K] (Γ : ℤ) (evalRound : α × ℕ → ℤ × List JetRows) (ctx : α) (w : ℕ → ℤ) (m_group : ℕ → Fin r → ℕ) (H_rat : ℕ → Fin r → JetTable J ℓ K) (H_int : ℕ → Fin r → JetRows) (hround : ∀ idx < T_rounds, evalRound (ctx, idx) = (w idx, List.ofFn (H_int idx))) (hm : ∀ idx < T_rounds, ∑ g : Fin r, m_group idx g = m) (hH : ∀ idx < T_rounds, ∀ (g : Fin r), Γ ^ m_group idx g • H_rat idx g = (JetTable.castRingHom K) (toJetTable J ℓ (H_int idx g))) : Γ ^ m • ∑ idx ∈ Finset.range T_rounds, w idx • ∏ g : Fin r, H_rat idx g = (JetTable.castRingHom K) (toJetTable J ℓ (streamOuterJetAccum evalRound J ℓ T_rounds ctx))

Fixed-denominator Ω = Γ ^ m clearing for streamOuterJetAccum (Appendix B.2, p. 49).

theorem Cslib.CommonCountingAccum.cast_streamOuterJetAccum_taylorOuterVJet {α : Type} {J ℓ r m T_rounds : ℕ} {K : Type u_1} [CommRing K] (Γ : ℤ) (t : K) (evalRound : α × ℕ → ℤ × List JetRows) (ctx : α) (w : ℕ → ℤ) (m_group : ℕ → Fin r → ℕ) (P_rat : ℕ → Fin r → Polynomial (Polynomial K)) (H_int : ℕ → Fin r → JetRows) (hround : ∀ idx < T_rounds, evalRound (ctx, idx) = (w idx, List.ofFn (H_int idx))) (hm : ∀ idx < T_rounds, ∑ g : Fin r, m_group idx g = m) (hP : ∀ idx < T_rounds, ∀ (g : Fin r), Γ ^ m_group idx g • (taylorOuterVJet J ℓ t) (P_rat idx g) = (JetTable.castRingHom K) (toJetTable J ℓ (H_int idx g))) : Γ ^ m • (taylorOuterVJet J ℓ t) (∑ idx ∈ Finset.range T_rounds, w idx • ∏ g : Fin r, P_rat idx g) = (JetTable.castRingHom K) (toJetTable J ℓ (streamOuterJetAccum evalRound J ℓ T_rounds ctx))

Direct taylorOuterVJet clearing for streamOuterJetAccum (unconditional in K).

theorem Cslib.CommonCountingAccum.combineOuterRound_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (r : ((ℕ × ℕ) × JetRows) × ℤ × List JetRows) => combineOuterRound r.1.1.1 r.1.1.2 r.1.2 r.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encIntBin (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

@[reducible, inline]

noncomputable abbrev Cslib.CommonCountingAccum.outerAccumBodyCertificate {α : Type} {encCtx : α ↪ List Bool} {evalRound : α × ℕ → ℤ × List JetRows} (cround : GenericRAM.NativeCertificate evalRound (Turing.MultiTapeTM.encPair encCtx Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encIntBin (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))))) : GenericRAM.NativeCertificate (outerAccumBody evalRound) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) encCtx) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) encCtx) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))

Single-step IndexFold body certificate for streamOuterJetAccum.

noncomputable def Cslib.CommonCountingAccum.outerJetAccumCertificate {ι α : Type} {encIn : ι ↪ List Bool} {encCtx : α ↪ List Bool} {J ℓ T_rounds : ι → ℕ} {ctx : ι → α} {evalRound : α × ℕ → ℤ × List JetRows} (cJ : GenericRAM.NativeCertificate J encIn Turing.MultiTapeTM.encUnary) (cℓ : GenericRAM.NativeCertificate ℓ encIn Turing.MultiTapeTM.encUnary) (cT : GenericRAM.NativeCertificate T_rounds encIn Turing.MultiTapeTM.encNat) (cctx : GenericRAM.NativeCertificate ctx encIn encCtx) (cround : GenericRAM.NativeCertificate evalRound (Turing.MultiTapeTM.encPair encCtx Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encIntBin (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))))) : GenericRAM.NativeCertificate (fun (x : ι) => streamOuterJetAccum evalRound (J x) (ℓ x) (T_rounds x) (ctx x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Uniform NativeCertificate for streamOuterJetAccum, built via IndexFold.certificate.

theorem Cslib.CommonCountingAccum.computableInO_outerJetAccumCertificate {ι α : Type} {encIn : ι ↪ List Bool} {encCtx : α ↪ List Bool} {J ℓ T_rounds : ι → ℕ} {ctx : ι → α} {evalRound : α × ℕ → ℤ × List JetRows} (cJ : GenericRAM.NativeCertificate J encIn Turing.MultiTapeTM.encUnary) (cℓ : GenericRAM.NativeCertificate ℓ encIn Turing.MultiTapeTM.encUnary) (cT : GenericRAM.NativeCertificate T_rounds encIn Turing.MultiTapeTM.encNat) (cctx : GenericRAM.NativeCertificate ctx encIn encCtx) (cround : GenericRAM.NativeCertificate evalRound (Turing.MultiTapeTM.encPair encCtx Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encIntBin (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))))) (hcJ : cJ.IsPolynomial) (hcℓ : cℓ.IsPolynomial) (hcT : cT.IsPolynomial) (hcctx : cctx.IsPolynomial) (hcround_space : Turing.MultiTapeTM.PolyBounded (fun (q : α × ℕ) => ((Turing.MultiTapeTM.encPair encCtx Turing.MultiTapeTM.encNat) q).length) cround.space) (R_round : ι → ℕ) (hR : ∀ (x : ι), ∀ idx ≤ T_rounds x, cround.time (ctx x, idx) ≤ R_round x) : ∃ (P : ι → ℕ), Turing.MultiTapeTM.PolyBounded (fun (x : ι) => (encIn x).length) P ∧ Turing.MultiTapeTM.ComputableInO (fun (x : ι) => streamOuterJetAccum evalRound (J x) (ℓ x) (T_rounds x) (ctx x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (fun (x : ι) => (T_rounds x + 1) * (R_round x + P x)) P

Explicit ComputableInO bound for streamOuterJetAccum from certificate components in time O((T_rounds + 1) * (R_round + P)) and space O(P).

theorem Cslib.CommonCountingAccum.computableInO_streamOuterJetAccum {ι α : Type} {encIn : ι ↪ List Bool} {encCtx : α ↪ List Bool} {J ℓ T_rounds : ι → ℕ} {ctx : ι → α} {evalRound : α × ℕ → ℤ × List JetRows} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hT : Turing.MultiTapeTM.ComputableInPolyTime T_rounds encIn Turing.MultiTapeTM.encNat) (hctx : Turing.MultiTapeTM.ComputableInPolyTime ctx encIn encCtx) (hround : Turing.MultiTapeTM.ComputableInPolyTime evalRound (Turing.MultiTapeTM.encPair encCtx Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encIntBin (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))))) : ∃ (P : ι → ℕ), Turing.MultiTapeTM.PolyBounded (fun (x : ι) => (encIn x).length) P ∧ Turing.MultiTapeTM.ComputableInO (fun (x : ι) => streamOuterJetAccum evalRound (J x) (ℓ x) (T_rounds x) (ctx x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (fun (x : ι) => (T_rounds x + 1) * P x) P

Explicit (T_rounds + 1) * P ComputableInO bound for streamOuterJetAccum when evalRound is computable in polynomial time.

theorem Cslib.CommonCountingAccum.computableInPolySpace_streamOuterJetAccum {ι α : Type} {encIn : ι ↪ List Bool} {encCtx : α ↪ List Bool} {J ℓ T_rounds : ι → ℕ} {ctx : ι → α} {evalRound : α × ℕ → ℤ × List JetRows} (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hT : Turing.MultiTapeTM.ComputableInPolyTime T_rounds encIn Turing.MultiTapeTM.encNat) (hctx : Turing.MultiTapeTM.ComputableInPolyTime ctx encIn encCtx) (hround : Turing.MultiTapeTM.ComputableInPolySpace evalRound (Turing.MultiTapeTM.encPair encCtx Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encIntBin (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))))) : Turing.MultiTapeTM.ComputableInPolySpace (fun (x : ι) => streamOuterJetAccum evalRound (J x) (ℓ x) (T_rounds x) (ctx x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Plain ComputableInPolySpace guarantee for streamOuterJetAccum when evalRound is computable in polynomial space.

4. Confluent Hermite Cramer recovery from per-node outer jets

def Cslib.CommonCountingAccum.recoverOuterJetSumModPowTwo (nodes : List ℤ) (J ℓ : ℕ) (Ω : ℤ) (nodeJets : List JetRows) : ℤ

Recover (∑_{u < ℓ} H_u(0)).modPowTwo ℓ from per-node J × ℓ Ω-scaled Taylor-jet arrays nodeJets at nodes via extractAllCoordNodeJets and Cslib.Circuits.Rational.hermiteRecoverZero (OpenAI, The Exponential Time Hypothesis is False, eq. (5.5) and Appendix B.3, p. 50; returns 0 when ℓ = 0, Ω = 0, or detRows (hermiteRows nodes J) = 0).

@[simp]

theorem Cslib.CommonCountingAccum.recoverOuterJetSumModPowTwo_zero_cols (nodes : List ℤ) (J : ℕ) (Ω : ℤ) (nodeJets : List JetRows) : recoverOuterJetSumModPowTwo nodes J 0 Ω nodeJets = 0

theorem Cslib.CommonCountingAccum.hermiteRecoverZero_extractCoordNodeJets_eq {J ℓ : ℕ} {Ω H_zero : ℤ} {nodes : List ℤ} (hnodup : nodes.Nodup) (hΩ : Ω ≠ 0) (nodeJets : List JetRows) (hlen : nodeJets.length = nodes.length) (P : Polynomial (Polynomial ℚ)) (hclear : ∀ (i : Fin nodes.length), Ω • (taylorOuterVJet J ℓ ↑nodes[i]) P = (JetTable.castRingHom ℚ) (toJetTable J ℓ nodeJets[↑i])) (u : Fin ℓ) (hdeg : (P.coeff ↑u).natDegree < nodes.length * J) (hH0 : Polynomial.eval 0 (P.coeff ↑u) = ↑H_zero) : Circuits.Rational.hermiteRecoverZero nodes J Ω (extractCoordNodeJets J (↑u) nodeJets) = H_zero

Single-coordinate confluent Hermite Cramer recovery of (P.coeff u).eval 0 = H_zero.

theorem Cslib.CommonCountingAccum.recoverOuterJetSumModPowTwo_eq {J ℓ : ℕ} {Ω count : ℤ} {nodes : List ℤ} (hnodup : nodes.Nodup) (hΩ : Ω ≠ 0) (nodeJets : List JetRows) (hlen : nodeJets.length = nodes.length) (P : Polynomial (Polynomial ℚ)) (H_zero : Fin ℓ → ℤ) (hclear : ∀ (i : Fin nodes.length), Ω • (taylorOuterVJet J ℓ ↑nodes[i]) P = (JetTable.castRingHom ℚ) (toJetTable J ℓ nodeJets[↑i])) (hdeg : ∀ (u : Fin ℓ), (P.coeff ↑u).natDegree < nodes.length * J) (hH0 : ∀ (u : Fin ℓ), Polynomial.eval 0 (P.coeff ↑u) = ↑(H_zero u)) (hcount₀ : 0 ≤ count) (hcount₁ : count < 2 ^ ℓ) (hdvd : 2 ^ ℓ ∣ ∑ u : Fin ℓ, H_zero u - count) : recoverOuterJetSumModPowTwo nodes J ℓ Ω nodeJets = count

Full multi-coordinate modular count recovery S_ℓ(H(0)) ≡ count (mod 2 ^ ℓ) from Ω-scaled per-node outer Taylor jets (OpenAI, The Exponential Time Hypothesis is False, eq. (5.5) and Appendix B.3, p. 50).

theorem Cslib.CommonCountingAccum.recoverOuterJetSumModPowTwo_streamOuterJetAccum_eq {α : Type} {J ℓ r m T_rounds : ℕ} {Γ count : ℤ} {nodes : List ℤ} (hnodup : nodes.Nodup) (hΓ : Γ ≠ 0) (evalRound : α × ℕ → ℤ × List JetRows) (nodeCtx : Fin nodes.length → α) (w : ℕ → ℤ) (m_group : ℕ → Fin r → ℕ) (P_rat : ℕ → Fin r → Polynomial (Polynomial ℚ)) (H_int : Fin nodes.length → ℕ → Fin r → JetRows) (H_zero : Fin ℓ → ℤ) (hround : ∀ (i : Fin nodes.length), ∀ idx < T_rounds, evalRound (nodeCtx i, idx) = (w idx, List.ofFn (H_int i idx))) (hm : ∀ idx < T_rounds, ∑ g : Fin r, m_group idx g = m) (hP : ∀ (i : Fin nodes.length), ∀ idx < T_rounds, ∀ (g : Fin r), Γ ^ m_group idx g • (taylorOuterVJet J ℓ ↑nodes[i]) (P_rat idx g) = (JetTable.castRingHom ℚ) (toJetTable J ℓ (H_int i idx g))) (hdeg : ∀ (u : Fin ℓ), ((∑ idx ∈ Finset.range T_rounds, w idx • ∏ g : Fin r, P_rat idx g).coeff ↑u).natDegree < nodes.length * J) (hH0 : ∀ (u : Fin ℓ), Polynomial.eval 0 ((∑ idx ∈ Finset.range T_rounds, w idx • ∏ g : Fin r, P_rat idx g).coeff ↑u) = ↑(H_zero u)) (hcount₀ : 0 ≤ count) (hcount₁ : count < 2 ^ ℓ) (hdvd : 2 ^ ℓ ∣ ∑ u : Fin ℓ, H_zero u - count) : recoverOuterJetSumModPowTwo nodes J ℓ (Γ ^ m) (List.ofFn fun (i : Fin nodes.length) => streamOuterJetAccum evalRound J ℓ T_rounds (nodeCtx i)) = count

Outer-round accumulation plus Cramer count recovery from supplied cleared group payloads across Q distinct nodes.

theorem Cslib.CommonCountingAccum.computableInPolyTime_recoverOuterJetSumModPowTwo {α : Type} {encIn : α ↪ List Bool} {nodes : α → List ℤ} {J ℓ : α → ℕ} {Ω : α → ℤ} {nodeJets : α → List JetRows} (hnodes : Turing.MultiTapeTM.ComputableInPolyTime nodes encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hΩ : Turing.MultiTapeTM.ComputableInPolyTime Ω encIn Turing.MultiTapeTM.encIntBin) (hnodeJets : Turing.MultiTapeTM.ComputableInPolyTime nodeJets encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => recoverOuterJetSumModPowTwo (nodes x) (J x) (ℓ x) (Ω x) (nodeJets x)) encIn Turing.MultiTapeTM.encIntBin