Phase-five endpoint for the evaluated-slice paper chain

This file isolates the paper line-87 removal endpoint and the finite reindexing to the raw scalar G-commutativity stability defect.

Paper-faithful phase-five removal after the right-register swap

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSlicePhaseFivePaperRemoved {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : EvaluatedSliceQuestion params) : Error

Paper line-87 endpoint after removing the trailing G^x.total.

At question q = ((u,x),(v,y)) and outcome (a,b), this is G^{u,x}_a G^{v,y}_b ⊗ A^{u,x}_a A^{v,y}_b.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSlicePhaseSixFirstReverse {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : EvaluatedSliceQuestion params) : Error

Paper line 101 endpoint after reversing the first eq:add-an-a insertion.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSlicePhaseSixFirstRemoved {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : EvaluatedSliceQuestion params) : Error

Paper line 102 endpoint after simplifying the first-coordinate projector.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSlicePhaseSevenGonnaCite {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : EvaluatedSliceQuestion params) : Error

Paper line 104 endpoint eq:gonna-cite-this-in-just-a-bit.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSlicePhaseEightTailRight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : EvaluatedSliceQuestion params) : Error

Paper line 118 endpoint after moving the second factor to the right register.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSlicePhaseFivePaperOrderedDefect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (q : EvaluatedSliceQuestion params) : Error

Ordered missing-mass defect for the paper phase-five removal.

This is the defect before swapping the two right-register point measurements: G^{u,x}_a G^{v,y}_b (1-G^x) ⊗ A^{u,x}_a A^{v,y}_b.

Equations

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

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSlicePhaseFivePaperSwappedDefect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (q : EvaluatedSliceQuestion params) : Error

Swapped missing-mass defect for the paper phase-five removal.

After the right-register point swap, this reindexes to gCommStabilityTwoRawScalarDefect: the right register is A^{v,y}_b A^{u,x}_a.

Equations

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

theorem MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseFivePaper_avg_diff_eq_neg_orderedDefect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) : have 𝒟 := uniformDistribution (EvaluatedSliceQuestion params); have inserted := fun (q : EvaluatedSliceQuestion params) => ∑ a : Fq params, ∑ b : Fq params, ev strategy.state (leftTensor ((evaluatedSliceFirstFactor params family q).outcome a * (evaluatedSliceSecondFactor params family q).outcome b * (evaluatedSliceFirstFactor params family q).total) * rightTensor ((evaluatedSlicePointMeas params strategy q.1).outcome a * (evaluatedSlicePointMeas params strategy q.2).outcome b)); have removed := evaluatedSlicePhaseFivePaperRemoved params strategy family; avgOver 𝒟 inserted - avgOver 𝒟 removed = -avgOver 𝒟 (evaluatedSlicePhaseFivePaperOrderedDefect params strategy family G)

Average the paper phase-five algebra over evaluated-slice questions.

theorem MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseFivePaper_reindex_to_raw_defect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) : avgOver (uniformDistribution (EvaluatedSliceQuestion params)) (evaluatedSlicePhaseFivePaperSwappedDefect params strategy family G) = avgOver (uniformDistribution (Fq params)) (gCommStabilityTwoRawScalarDefect params strategy family G)

Exact reindexing of the swapped paper defect to the raw scalar stability defect.

This is the phase-five coordinate audit point from issue #628. The proof intentionally decomposes the first evaluated-slice coordinate q.1 = appendPoint params u x, because the defect reads pointHeight params q.1 and the first-coordinate point outcome evaluatedSlicePointMeas params strategy q.1. There is no gamma parameter in this reindexing lemma: the only gamma loss in phase five is the separate right-register point-measurement swap paid by hphase5paper in ProcessedG.lean.