Section 11 commutativity: the phase-five endpoint of the evaluated-slice paper chain

The paper line-87 removal endpoint and the finite reindexing to the raw scalar G-commutativity stability defect: the counterpart of Commutativity/ScalarApproximation/PaperChainPhaseFive.lean under MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The endpoints and defects are real expectations strategy.state.ev (strategy.state.L … * strategy.state.R …) on the symmetric model of the strategy, with the vendored arguments unchanged. phaseFivePaper_fiber_sum_ev takes the symmetric model S where the vendored lemma takes the state ψ, in the same position.

The vendored proof of evaluatedSlice_phaseFivePaper_term_diff computes with Kronecker products and Matrix.smul_kronecker; here it is mul_sub, the keystone's leftTensor_sub and ev_sub, and ring on the scalars. The fiber collapse is Finset.sum_fiberwise after expanding the fiber sum into the left placement, and the last step of the reindexing holds by definitional equality, evaluatedSlicePointMeas being the strategy's point measurement.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

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

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSlicePhaseFivePaperRemoved {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) : ℝ

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 MIPRE.LIDT.Co.Commutativity.evaluatedSlicePhaseSixFirstReverse {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) : ℝ

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 MIPRE.LIDT.Co.Commutativity.evaluatedSlicePhaseSixFirstRemoved {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) : ℝ

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 MIPRE.LIDT.Co.Commutativity.evaluatedSlicePhaseSevenGonnaCite {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) : ℝ

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 MIPRE.LIDT.Co.Commutativity.evaluatedSlicePhaseEightTailRight {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) : ℝ

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 MIPRE.LIDT.Co.Commutativity.evaluatedSlicePhaseFivePaperOrderedDefect {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) : ℝ

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 MIPRE.LIDT.Co.Commutativity.evaluatedSlicePhaseFivePaperSwappedDefect {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) : ℝ

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 MIPRE.LIDT.Co.Commutativity.evaluatedSlice_phaseFivePaper_term_diff {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hG : ∀ (x : MIPStarRE.LDT.Fq params), G x = (family.meas x).toSubMeas) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (a b : MIPStarRE.LDT.Fq params) : strategy.state.ev (strategy.state.L ((evaluatedSliceFirstFactor params family q).outcome a * (evaluatedSliceSecondFactor params family q).outcome b * (evaluatedSliceFirstFactor params family q).total) * strategy.state.R ((evaluatedSlicePointMeas params strategy q.1).outcome a * (evaluatedSlicePointMeas params strategy q.2).outcome b)) - strategy.state.ev (strategy.state.L ((evaluatedSliceFirstFactor params family q).outcome a * (evaluatedSliceSecondFactor params family q).outcome b) * strategy.state.R ((evaluatedSlicePointMeas params strategy q.1).outcome a * (evaluatedSlicePointMeas params strategy q.2).outcome b)) = -strategy.state.ev (strategy.state.L ((evaluatedSliceFirstFactor params family q).outcome a * (evaluatedSliceSecondFactor params family q).outcome b * (1 - (G (MIPStarRE.LDT.pointHeight params q.1)).total)) * strategy.state.R ((evaluatedSlicePointMeas params strategy q.1).outcome a * (evaluatedSlicePointMeas params strategy q.2).outcome b))

Pointwise algebra for the paper phase-five removal.

The swapped phase-four endpoint contains the left factor A_a B_b G^x.total; subtracting the line-87 removed endpoint gives the negative of the ordered defect A_a B_b (1-G^x.total).

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSlice_phaseFivePaper_avg_diff_eq_neg_orderedDefect {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hG : ∀ (x : MIPStarRE.LDT.Fq params), G x = (family.meas x).toSubMeas) : have 𝒟 := MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params); have inserted := fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => ∑ a : MIPStarRE.LDT.Fq params, ∑ b : MIPStarRE.LDT.Fq params, strategy.state.ev (strategy.state.L ((evaluatedSliceFirstFactor params family q).outcome a * (evaluatedSliceSecondFactor params family q).outcome b * (evaluatedSliceFirstFactor params family q).total) * strategy.state.R ((evaluatedSlicePointMeas params strategy q.1).outcome a * (evaluatedSlicePointMeas params strategy q.2).outcome b)); have removed := evaluatedSlicePhaseFivePaperRemoved params strategy family; MIPStarRE.LDT.avgOver 𝒟 inserted - MIPStarRE.LDT.avgOver 𝒟 removed = -MIPStarRE.LDT.avgOver 𝒟 (evaluatedSlicePhaseFivePaperOrderedDefect params strategy family G)

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

theorem MIPRE.LIDT.Co.Commutativity.phaseFivePaper_fiber_sum_ev {𝔓 : 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) (u : MIPStarRE.LDT.Point params) (B T P₂ : 𝔓) (Gx : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (P₁ : MIPStarRE.LDT.Fq params → 𝔓) : ∑ a : MIPStarRE.LDT.Fq params, S.ev (S.L ((∑ g : MIPStarRE.LDT.Polynomial params with g.toFun u = a, Gx.outcome g) * B * T) * S.R (P₂ * P₁ a)) = ∑ g : MIPStarRE.LDT.Polynomial params, S.ev (S.L (Gx.outcome g * B * T) * S.R (P₂ * P₁ (g.toFun u)))

Collapse the first-coordinate postprocessing fiber in the raw paper defect.

For fixed (u,x) and right prefix P₂, summing over evaluated outcomes a expands G^{u,x}_a = ∑_{g : g(u)=a} G^x_g and collapses to a polynomial sum.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSlicePhaseFivePaperSwappedDefect_appendPoint_expansion {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hG : ∀ (x : MIPStarRE.LDT.Fq params), G x = (family.meas x).toSubMeas) (x : MIPStarRE.LDT.Fq params) (u : MIPStarRE.LDT.Point params) (vy : MIPStarRE.LDT.Point params.next) : evaluatedSlicePhaseFivePaperSwappedDefect params strategy family G (MIPStarRE.LDT.appendPoint params u x, vy) = ∑ g : MIPStarRE.LDT.Polynomial params, ∑ b : MIPStarRE.LDT.Fq params, strategy.state.ev (strategy.state.L ((G x).outcome g * (evaluatedPointFamily params family vy).outcome b * (1 - (G x).total)) * strategy.state.R ((evaluatedSlicePointMeas params strategy vy).outcome b * (evaluatedSlicePointMeas params strategy (MIPStarRE.LDT.appendPoint params u x)).outcome (g.toFun u)))

Pointwise expansion of the swapped paper defect after writing the first point as (u,x).

The statement keeps point measurements in the local evaluatedSlicePointMeas notation; the final reindexing lemma rewrites those to strategy.pointMeasurement when matching gCommStabilityTwoRawScalarDefect.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSlice_phaseFivePaper_reindex_to_raw_defect {𝔓 : 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] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hG : ∀ (x : MIPStarRE.LDT.Fq params), G x = (family.meas x).toSubMeas) : MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (evaluatedSlicePhaseFivePaperSwappedDefect params strategy family G) = MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) (gCommStabilityTwoRawScalarDefect params strategy family G)

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

The proof 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.