Measurement-fiber Taylor-jet identities and Hermite–Cramer zero-counting recovery #
This module completes two mathematical bridges in the polynomial-interpolation and parity-counting pipeline of OpenAI, The Exponential Time Hypothesis is False (Sections 3.4, 5.3–5.5, and Appendix B.2–B.3, printed pp. 24–25, 37–39, 48–50):
§3.4 Affine-Taylor to measurement-fiber jet bridge (
Cslib.ReplacementCounting, equations (3.9)–(3.13) and Proposition 3.4, pp. 24–25): ConnectingCslib.AffineTaylor(replacedSum,affineInput,affineFactor,factorProduct,coeff_taylor_replacedSum_eq_restricted_subsets) withCslib.ReplacementCounting.Design(targetPoly,shiftedFactorEval,sum_restricted_shiftedFactor_eq_sum_measurement_fibers):targetPolynomial_eq_replacedSumandDesign.targetPoly_eq_replacedSumidentifytargetPolynomialwithAffineTaylor.replacedSum.Design.map_eval_affineInput_indicator,Design.map_eval_affineFactor_indicator, andDesign.eval_coeff_factorProduct_indicatorshow that evaluating the formal Boolean variablesXofAffineTaylor.affineFactorandAffineTaylor.factorProductat the subset indicator ofU ⊆ ιproducesM.shiftedFactorEval Φ t U.Design.coeff_taylor_targetPoly_eq_sum_measurement_fibersandDesign.coeff_taylor_targetPoly_eq_measurementFiberJetprove equation (3.13): for every jet orderj ≤ qat evaluation nodet : Fin Q,[z ^ j] H(t + z)equals the signed Möbius sum over subset pairs#E ≤ q,U ⊆ Eof the measurement-fiber sums overM.measurementBox t.Design.targetSum_eq_of_measurementFiberJetandDesign.targetSum_eq_of_measurementFiberJet_jetOrdercombine equation (3.13) with confluent Hermite interpolation (Design.targetSum_eq_of_taylorJet_jetOrder) to recovertargetSum s scope Φdirectly fromM.measurementFiberJet.
§5.4 & Appendix B.2–B.3 Taylor-shift commutation,
JetTablebridge, and unconditional Hermite–Cramer recovery (Cslib.BitString, pp. 37–39, 48–50):- Taylor-shift commutation:
Polynomial.taylor tcommutes withclearedMonomialPoly,clearedMonomialSumPoly,parityBaseDigitCleared,hPolyCleared,parityFactorCleared,univariateClearedParityCoord, andunivariateClearedParityTruncatedSumby shifting each variable numerator polynomialθ x i v(taylor_univariateClearedParityCoord,taylor_univariateClearedParityTruncatedSum). - Staged
JetTablebridge (Appendix B.2):JetTable.ofPolyVPolyZ J ℓextracts the(J × ℓ)coefficient table(j, u) ↦ [z ^ j] ([V ^ u] Q)as a ring homomorphismPolynomial (Polynomial R) →+* JetTable J ℓ R. UnderofPolyVPolyZ J ℓ, the Stage-1 and Stage-2 table operationsJetTable.clearedMonomialJet,JetTable.clearedMonomialSumJet, andJetTable.clearedParityFactorJetfromStagedJetArithmeticcompute the exact Taylor-jet coefficients ofclearedMonomialSumPoly,parityFactorCleared, andunivariateClearedParityCoord(clearedParityJetTable_apply). - Unconditional Hermite–Cramer determinant recovery (Appendix B.3, eq. B.1):
instantiating
Polynomial.hermiteMatrixandCslib.hermiteCramerNumeratorat distinct integer nodesnodes : Fin Q → ℤ(and atnodeInt : Fin Q → ℤwith canonical jet ordersparseParityJetOrder k R Q #I ℓfor anyD : ReplacementDesign scope Q r A₀ R τ) discharges the abstractD_H ≠ 0andhcramerpremises ofemod_sum_cramer_ediv_eq_commonZeroCountandemod_sum_cramer_ediv_design_eq_commonZeroCountunconditionally (emod_sum_hermiteCramerNumerator_ediv_eq_commonZeroCount,emod_sum_hermiteCramerNumerator_design_eq_commonZeroCount,emod_hermiteCramerNumerator_truncatedSum_design_eq_commonZeroCount, and branch-summedcommonZeroCount_eq_sum_branch_hermiteCramerNumerator_design).
- Taylor-shift commutation:
Main definitions #
Cslib.ReplacementCounting.Design.measurementFiberJet: the equation (3.13) Möbius-summed measurement-fiber Taylor-jet coefficient at nodetand orderj.Cslib.BitString.clearedParityJetTable:(J × ℓ)integer jet table at evaluation pointt : ℤbuilt fromJetTable.clearedParityFactorJetandJetTable.clearedMonomialSumJet.Cslib.BitString.sparseParityJetOrder: canonical confluent jet orderReplacementCounting.jetOrder ((k * (R - 1)) * (m_eq + 2 * (ℓ - 1))) Q.
Main results #
Cslib.ReplacementCounting.targetPolynomial_eq_replacedSum,Cslib.ReplacementCounting.Design.map_eval_affineFactor_indicator,Cslib.ReplacementCounting.Design.coeff_taylor_targetPoly_eq_sum_measurement_fibers,Cslib.ReplacementCounting.Design.targetSum_eq_of_measurementFiberJet_jetOrder: §3.4 equation (3.13) and Proposition 3.4 measurement-fiber Taylor-jet recovery.Cslib.BitString.taylor_univariateClearedParityCoord,Cslib.BitString.taylor_univariateClearedParityTruncatedSum,Cslib.BitString.clearedParityJetTable_apply: Taylor-shift commutation and exactJetTablecorrespondence for cleared parity polynomials.Cslib.BitString.hermiteCramerNumerator_intPoly_eq_mul,Cslib.BitString.emod_sum_hermiteCramerNumerator_ediv_eq_commonZeroCount,Cslib.BitString.emod_sum_hermiteCramerNumerator_design_eq_commonZeroCount,Cslib.BitString.emod_hermiteCramerNumerator_truncatedSum_design_eq_commonZeroCount,Cslib.BitString.commonZeroCount_eq_sum_branch_hermiteCramerNumerator_design: unconditional Hermite–Cramer determinant recovery ofcommonZeroCount.
References #
- OpenAI, The Exponential Time Hypothesis is False, §3.4, §§5.3–5.5, and Appendix B.2–B.3, pp. 24–25, 37–39, 48–50.
1. §3.4 Affine-Taylor to measurement-fiber jet bridge (equations (3.9)–(3.13)) #
ReplacementCounting.targetPolynomial coincides with AffineTaylor.replacedSum
([OAI26c], equation (3.3), pp. 21, 24).
M.targetPoly Φ coincides with AffineTaylor.replacedSum s Φ (M.rowIn A).
Evaluating the formal variables X of AffineTaylor.affineInput (M.rowIn A f v) at the
indicator of U ⊆ ι yields the scalar baseline algebraMap ℚ A (M.evalRow t f v x) plus the sum
of Taylor corrections over i ∈ U ([OAI26c], equations (3.7)–(3.8), p. 24).
Evaluating the formal variables X of AffineTaylor.affineFactor at the indicator of U ⊆ ι
produces M.shiftedFactorEval Φ t U f (fun v => M.evalRow t f v x) ([OAI26c],
equations (3.8) and (3.11), pp. 24–25).
Evaluating the j-th Taylor coefficient of AffineTaylor.factorProduct at the indicator of
U ⊆ ι equals the j-th coefficient of the product of M.shiftedFactorEval over f ∈ s.
Classical fiber-representative selector for M.localMeasure t, choosing a local Boolean
assignment u : M.LocalCube t g with M.localMeasure t g u = y g whenever all fibers y g are
nonempty.
Instances For
M.classicalRepresentative t satisfies the representative validity condition for
SharedSummaries.fiberContribution.
Equation (3.13) measurement-fiber Taylor-jet coefficient ([OAI26c], §3.4, p. 25):
the signed Möbius sum over subset pairs E ⊆ ι (#E ≤ q) and U ⊆ E of the j-th coefficient of
the measurement-fiber sum at node t : Fin Q.
Instances For
Equation (3.13) Taylor-jet measurement-fiber identity ([OAI26c], §3.4, pp. 24–25):
for every Taylor order j ≤ q and node t : Fin Q, [z ^ j] H(nodes t + z) equals the signed
Möbius sum over #E ≤ q and U ⊆ E of the j-th coefficient of the measurement-fiber sums over
M.measurementBox t.
Packaging coeff_taylor_targetPoly_eq_sum_measurement_fibers in terms of
M.measurementFiberJet.
When J ≤ q + 1, the order-J Taylor jet Polynomial.taylorJet of M.targetPoly Φ at
M.nodes agrees entrywise with M.measurementFiberJet Φ q.
Proposition 3.4 complete algebraic recovery of targetSum from measurement-fiber Taylor
jets ([OAI26c], §§3.4–3.5, pp. 24–25): whenever
(liftedFactorProduct s Φ).totalDegree ≤ d, 0 < J, d * R < Q * J, and J ≤ q + 1,
targetSum s scope Φ equals the Hermite determinant formed from M.measurementFiberJet Φ q.
Specialization of targetSum_eq_of_measurementFiberJet to the canonical truncation order
q = (d * R) / Q and jet order J = jetOrder (d * R) Q = (d * R) / Q + 1
([OAI26c], equation (3.5) and Proposition 3.4, pp. 24–25).
2. §5.4 & Appendix B.2–B.3 Taylor-shift commutation, JetTable bridge, and unconditional #
Hermite–Cramer recovery
3.1 Taylor-shift commutation with cleared parity polynomials #
Polynomial.taylor t commutes with clearedMonomialPoly by Taylor-shifting each factor
θ v.
Polynomial.taylor t commutes with clearedMonomialSumPoly by Taylor-shifting each factor
θ v.
Mapping parityFactorCleared ℓ (Polynomial.C Δ) A_i by (Polynomial.taylorAlgHom t).toRingHom
shifts A_i by Polynomial.taylor t.
Polynomial.taylor t commutes with univariateClearedParityCoord by Taylor-shifting each
numerator polynomial θ x i v.
Polynomial.taylor t commutes with univariateClearedParityTruncatedSum by Taylor-shifting
each numerator polynomial θ x i v.
3.2 Exact correspondence with JetTable staged operations (Appendix B.2) #
JetTable.ofPolyZ J ℓ maps clearedMonomialPoly d_den k θ M to
JetTable.clearedMonomialJet d_den k (fun v => JetTable.ofPolyZ J ℓ (θ v)) M.
JetTable.ofPolyZ J ℓ maps clearedMonomialSumPoly d_den k θ 𝓜 to
JetTable.clearedMonomialSumJet d_den k (fun v => JetTable.ofPolyZ J ℓ (θ v)) 𝓜 id.
JetTable.ofPolyVPolyZ J ℓ maps parityFactorCleared ℓ (Polynomial.C Δ) A_i to
JetTable.clearedParityFactorJet Δ (JetTable.ofPolyZ J ℓ A_i) with coefficients from
Polynomial.parityBaseDigit ℓ.
The (J × ℓ) integer Taylor-jet table at evaluation point t : ℤ constructed from the Stage-1
and Stage-2 JetTable operations (JetTable.clearedMonomialSumJet and
JetTable.clearedParityFactorJet) of StagedJetArithmetic ([OAI26c], Appendix B.2,
pp. 48–49).
Instances For
Appendix B.2 JetTable Taylor-jet identity: at every jet order j : Fin J and V-degree
s : Fin ℓ, clearedParityJetTable I P d_den k ℓ J θ t j s equals the j-th Taylor coefficient of
univariateClearedParityCoord I P d_den k ℓ θ s at t.
3.3 Unconditional Hermite–Cramer determinant recovery (Appendix B.3, eq. B.1) #
Integer Cramer factorization for ℤ[X] (Appendix B.3, eq. B.1, p. 50): for any integer
polynomial p : Polynomial ℤ with p.natDegree < Q * J, replacing column (0, 0) of
Polynomial.hermiteMatrix nodes J with the order-J Taylor jet of p at nodes yields a
determinant equal to (Polynomial.hermiteMatrix nodes J).det * p.eval 0.
Exact integer Cramer quotient for ℤ[X]: at distinct integer nodes nodes : Fin Q → ℤ,
dividing hermiteCramerNumerator of p's order-J Taylor jet by
(Polynomial.hermiteMatrix nodes J).det recovers p.eval 0.
Cramer numerator factorization for univariateClearedParityCoord (Appendix B.3, eq. B.1):
when (k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J, the Cramer determinant of the order-J Taylor jet
of univariateClearedParityCoord I P d_den k ℓ θ s (s < ℓ) at nodes equals
(Polynomial.hermiteMatrix nodes J).det * (univariateClearedParityCoord I P d_den k ℓ θ s).eval 0.
Cramer numerator factorization for univariateClearedParityTruncatedSum (Appendix B.3,
eq. B.1): under the same degree bound, the Cramer determinant of the order-J Taylor jet of
univariateClearedParityTruncatedSum I P d_den k ℓ θ at nodes equals
(Polynomial.hermiteMatrix nodes J).det * (univariateClearedParityTruncatedSum I P d_den k ℓ θ).eval 0.
Unconditional Hermite–Cramer coordinate recovery of commonZeroCount (Appendix B.3,
eq. B.1, p. 50): at distinct integer nodes nodes : Fin Q → ℤ with (k * R_deg) * (#I + 2 * (ℓ - 1)) < Q * J, d_den ≠ 0, and Fintype.card ι < ℓ, summing the exact integer Cramer
quotients over s ∈ range ℓ and reducing modulo 2 ^ ℓ recovers commonZeroCount I P without
auxiliary D_H or hcramer hypotheses.
Unconditional Hermite–Cramer truncated-sum recovery of commonZeroCount (Appendix B.3,
eq. B.1, p. 50): under the same hypotheses, dividing the single Cramer determinant of
univariateClearedParityTruncatedSum I P d_den k ℓ θ by
clearedProductDenom d_den k ℓ #I * (Polynomial.hermiteMatrix nodes J).det and reducing modulo
2 ^ ℓ recovers commonZeroCount I P.
3.4 Canonical jet order and concrete ReplacementDesign Hermite–Cramer recovery #
Canonical confluent Taylor jet order
J = ⌊(k * (R - 1)) * (m_eq + 2 * (ℓ - 1)) / Q⌋ + 1 for a degree-≤ k sparse parity system of
m_eq equations at precision ℓ under a Section 4 ReplacementDesign with degree bound R - 1
and Q evaluation nodes ([OAI26c], equations (3.5) and (5.5), pp. 24, 37).
Instances For
sparseParityJetOrder is always positive.
When 0 < Q, Q * sparseParityJetOrder k R Q m_eq ℓ strictly exceeds the equation (5.5)
degree bound (k * (R - 1)) * (m_eq + 2 * (ℓ - 1)).
Concrete ReplacementDesign Hermite–Cramer coordinate recovery of commonZeroCount
(§5.4 & Appendix B.3, eq. B.1): for any D : ReplacementDesign scope Q r A₀ R τ with 0 < Q,
n < ℓ, ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k, and (k * (R - 1)) * (#I + 2 * (ℓ - 1)) < Q * J (in
particular for J = sparseParityJetOrder k R Q #I ℓ), summing the concrete hermiteCramerNumerator
quotients at nodeInt over s ∈ range ℓ and reducing modulo 2 ^ ℓ recovers commonZeroCount I P
(discharging D_H ≠ 0 and hcramer of emod_sum_cramer_ediv_design_eq_commonZeroCount
unconditionally).
Concrete ReplacementDesign Hermite–Cramer truncated-sum recovery of commonZeroCount
(§5.4 & Appendix B.3, eq. B.1): under the same hypotheses, dividing the single Cramer determinant
of univariateClearedParityTruncatedSum at nodeInt by
clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I * (Polynomial.hermiteMatrix nodeInt J).det and
reducing modulo 2 ^ ℓ recovers commonZeroCount I P.
§5.5 & Appendix B.3 branch-summed concrete Hermite–Cramer recovery of commonZeroCount at
shared precision $\ell = n + 1$ and canonical jet order sparseParityJetOrder: given a
heavy-variable subset S : Finset (Fin n), a free-variable relabeling e : ↥(univ \ S) ≃ Fin n',
and a per-branch ReplacementDesign family D b (0 < Q), summing the branch modular residues of
the concrete hermiteCramerNumerator quotients at nodeInt and jet order
J = sparseParityJetOrder k R Q #I (branchPrecision n) across b ∈ branchAssignments S recovers
commonZeroCount I P.