Section 11 commutativity: symmetry transport

The point-consistency relation of a polynomial family, written in the evaluated-point-family notation and in both orientations used by the Section 11 commutativity argument: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Scaffold/Symmetry.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The relation is the bipartite strategy.state.ConsRel of the strategy's symmetric model. The swapped orientation is SymModel.consRel_symm_of_density_fixed, a theorem of the model, so the vendored strategy.densityFixed argument is gone.

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-points.tex
• references/ldt-paper/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

theorem MIPRE.LIDT.Co.Commutativity.evaluatedPointFamily_pointConsistency {𝔓 : 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 𝔓) (zeta : ℝ) (hcons : family.ConsistentWithPoints strategy zeta) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas (evaluatedPointFamily params family) zeta

The point-consistency relation written in local evaluated-point-family notation.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedPointFamily_pointConsistency_swapped {𝔓 : 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 𝔓) (zeta : ℝ) (hcons : family.ConsistentWithPoints strategy zeta) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (evaluatedPointFamily params family) strategy.pointMeasurement.toIdxSubMeas zeta

The evaluated-point consistency relation with the two families swapped. This is the orientation needed by Preliminaries.consSubMeas, whose submeasurement input comes first.