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

The paper's Step 5 bridge (references/ldt-paper/inductive_step.tex, lines 119--133): the algebraic expansion and reindexing from evaluated consistency to the full-polynomial consistency defect, the genuinely Schwartz--Zippel part being the tensor bound Preliminaries.polynomialCollisionMass_le_mdq. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Test/SchwartzZippelStep.lean in the port of planning/c6b-plan.md (milestone M4, section "Port conventions").

The declarations live in MIPRE.LIDT.Co.Test, with the symmetric model S : SymModel 𝔓 K an ordinary explicit argument in place of the vendored state ψ : QuantumState (ιA × ιB), as in Co/Preliminaries/PolynomialAgreement.lean; the bipartite quantities are the SymModel declarations of Co/Test/Defs.lean (S.qBipartiteMatchMass, S.qBipartiteConsDefect, S.bipartiteConsError, S.ConsRel). Both registers carry the local algebra 𝔓, so the vendored carriers ιA, ιB become 𝔓. The normalization hypothesis hnorm : ψ.IsNormalized of the two Step 5 theorems is dropped: it is a theorem of the model, and Preliminaries.polynomialCollisionMass_le_mdq does not take it.

mainFormalStep5_selfConsistency_ofExpansionBound_heterogeneous is therefore narrowed to one carrier, and has the type of mainFormalStep5_selfConsistency_ofExpansionBound. Its vendored caller, on the two-space ProjStrat of Test/MainTheorem/SourceRoleRegister/Core.lean, is left to M13 and M14 (planning/c6b-plan.md, "Same-space and bipartite quantities"), as for the heterogeneous triangle lemmas of Co/Preliminaries/Triangles.

Not ported

Every declaration of the vendored file has a counterpart here.

theorem MIPRE.LIDT.Co.Test.qBipartiteMatchMass_postprocess_eq_pair_sum {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (A B : SubMeas α 𝔓) (f : α → β) : S.qBipartiteMatchMass (postprocess A f) (postprocess B f) = ∑ aa : α × α, if f aa.1 = f aa.2 then S.ev (S.opTensor (A.outcome aa.1) (B.outcome aa.2)) else 0

The matching mass of two postprocessed submeasurements, expanded as a sum over pairs of original outcomes (a, a') whose readouts agree.

noncomputable def MIPRE.LIDT.Co.Test.localCollisionMass {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] (S : SymModel 𝔓 K) (A B : SubMeas α 𝔓) (f : α → β) : ℝ

The off-diagonal collision mass of A and B under the readout f: the pairs of distinct outcomes with the same readout, weighted by ⟨Ψ, (A_a ⊗ B_{a'}) Ψ⟩.

Equations

• MIPRE.LIDT.Co.Test.localCollisionMass S A B f = ∑ aa : α × α, (if aa.1 = aa.2 then 0 else if f aa.1 = f aa.2 then 1 else 0) * S.ev (S.opTensor (A.outcome aa.1) (B.outcome aa.2))

theorem MIPRE.LIDT.Co.Test.qBipartiteMatchMass_postprocess_eq_add_localCollision {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (A B : SubMeas α 𝔓) (f : α → β) : S.qBipartiteMatchMass (postprocess A f) (postprocess B f) = S.qBipartiteMatchMass A B + localCollisionMass S A B f

Postprocessing adds exactly the collision mass to the matching mass.

theorem MIPRE.LIDT.Co.Test.qBipartiteConsDefect_le_postprocess_add_localCollision {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (A B : SubMeas α 𝔓) (f : α → β) : S.qBipartiteConsDefect A B ≤ S.qBipartiteConsDefect (postprocess A f) (postprocess B f) + localCollisionMass S A B f

The consistency defect is at most that of the postprocessed pair plus the collision mass.

theorem MIPRE.LIDT.Co.Test.avg_localCollisionMass_eval_eq_polynomialCollisionMass {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (Left Right : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) fun (u : MIPStarRE.LDT.Point params) => localCollisionMass S Left Right fun (g : MIPStarRE.LDT.Polynomial params) => g.toFun u) = Preliminaries.polynomialCollisionMass params S Left Right

Averaging the collision mass of the point evaluations over a uniform point gives the polynomial collision mass.

def MIPRE.LIDT.Co.Test.MainFormalStep5ExpansionBound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (Left Right : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : 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 MIPRE.LIDT.Co.Test.mainFormalStep5_expansionBound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (Left Right : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : MainFormalStep5ExpansionBound params S 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 MIPRE.LIDT.Co.Test.mainFormalStep5_selfConsistency_ofExpansionBound_heterogeneous {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (Left Right : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (ζ : ℝ) (hevaluated : S.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params Left) (polynomialEvaluationFamily params Right) ζ) : S.ConsRel (MIPStarRE.LDT.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).

In the symmetric model both registers carry 𝔓, so this is mainFormalStep5_selfConsistency_ofExpansionBound; the vendored hypothesis hnorm : ψ.IsNormalized is a theorem of the model.

theorem MIPRE.LIDT.Co.Test.mainFormalStep5_selfConsistency_ofExpansionBound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (S : SymModel 𝔓 K) (Left Right : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (ζ : ℝ) (hevaluated : S.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params Left) (polynomialEvaluationFamily params Right) ζ) : S.ConsRel (MIPStarRE.LDT.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 (the vendored hypothesis hnorm : ψ.IsNormalized is a theorem of the model).