Section 10 commutativity points: drop comparisons

Comparison lemmas that drop structure from the mixed line family back to the ordered diagonal-line product, used in the drop direction of the Section 10 point-commutativity argument.

References

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

theorem MIPStarRE.LDT.CommutativityPoints.commutativityPoints {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) : SDDOpRel strategy.state (uniformDistribution (GlobalVariance.PointPairQuestion params)) (pointMeasurementProductLeft params strategy) (pointMeasurementProductRight params strategy) (commutativityPointsError params gamma)

thm:commutativity-points.