mainFormal Step 5 — Schwartz--Zippel self-consistency handoff

This file isolates the paper's Step 5 bridge in references/ldt-paper/inductive_step.tex, lines 119--133. The algebraic expansion/reindexing from evaluated consistency to the full-polynomial consistency defect is proved here, and the genuinely Schwartz--Zippel part is provided by the shared tensor bound Preliminaries.polynomialCollisionMass_le_mdq.

def MIPStarRE.LDT.Test.MainFormalStep5ExpansionBound {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (params : Parameters) [FieldModel params.q] (ψ : QuantumState (ιA × ιB)) (Left : SubMeas (Polynomial params) ιA) (Right : SubMeas (Polynomial params) ιB) : Prop

The exact algebraic expansion/reindexing statement used in mainFormal Step 5.

Paper origin: references/ldt-paper/inductive_step.tex:119-130 (\label{eq:G-self-consistency}), with the collision estimate supplied by the Schwartz--Zippel lemma.

Paper lines 119--128 compare the evaluated consistency defect

E_u ∑_{a ≠ b} ⟨ψ| G^A_[g(u)=a] ⊗ G^B_[h(u)=b] |ψ⟩

with the full-polynomial consistency defect

∑_{g ≠ h} ⟨ψ| G^A_g ⊗ G^B_h |ψ⟩.

The paper reuses g as the bound name in the Alice and Bob sums; Lean writes these independently-bound polynomial outcomes as g and h to make the independence explicit.

After expanding the postprocessed outcomes and separating the colliding pairs g(u)=h(u), the only extra term is the collision mass bounded by Schwartz--Zippel in Preliminaries.polynomialCollisionMass_le_mdq. This predicate records precisely that expansion step, without bundling the Schwartz--Zippel estimate itself into an unproved hypothesis.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Test.mainFormalStep5_expansionBound {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (params : Parameters) [FieldModel params.q] (ψ : QuantumState (ιA × ιB)) (Left : SubMeas (Polynomial params) ιA) (Right : SubMeas (Polynomial params) ιB) : MainFormalStep5ExpansionBound params ψ Left Right

The algebraic Step 5 expansion bound: the full-polynomial consistency error is bounded by the evaluated consistency error plus the collision mass.

theorem MIPStarRE.LDT.Test.mainFormalStep5_selfConsistency_ofExpansionBound_heterogeneous {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (params : Parameters) [FieldModel params.q] (ψ : QuantumState (ιA × ιB)) (hnorm : ψ.IsNormalized) (Left : SubMeas (Polynomial params) ιA) (Right : SubMeas (Polynomial params) ιB) (ζ : Error) (hevaluated : ConsRel ψ (uniformDistribution (Point params)) (polynomialEvaluationFamily params Left) (polynomialEvaluationFamily params Right) ζ) : ConsRel ψ (uniformDistribution Unit) (constSubMeasFamily Left) (constSubMeasFamily Right) (ζ + ↑params.m * ↑params.d / ↑params.q)

Heterogeneous Step 5 packaging for mainFormal using the proved algebraic expansion bound.

Given evaluated consistency at error ζ (paper line 116) and the exact line-122--125 expansion recorded by MainFormalStep5ExpansionBound, the proved tensor Schwartz--Zippel bound contributes the paper's md/q loss and returns full-polynomial consistency at error ζ + md/q (paper lines 126--133).

theorem MIPStarRE.LDT.Test.mainFormalStep5_selfConsistency_ofExpansionBound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (ψ : QuantumState (ι × ι)) (hnorm : ψ.IsNormalized) (Left Right : SubMeas (Polynomial params) ι) (ζ : Error) (hevaluated : ConsRel ψ (uniformDistribution (Point params)) (polynomialEvaluationFamily params Left) (polynomialEvaluationFamily params Right) ζ) : ConsRel ψ (uniformDistribution Unit) (constSubMeasFamily Left) (constSubMeasFamily Right) (ζ + ↑params.m * ↑params.d / ↑params.q)

Step 5 packaging for mainFormal using the proved algebraic expansion bound.

Given evaluated consistency at error ζ (paper line 116) and the exact line-122--125 expansion recorded by MainFormalStep5ExpansionBound, the proved tensor Schwartz--Zippel bound contributes the paper's md/q loss and returns full-polynomial consistency at error ζ + md/q (paper lines 126--133).

This is the source-labelled same-space statement.