Section 11 commutativity: symmetry transport #
Symmetry transport between coded F_q points and the underlying scalar model.
The lemmas below put the point-consistency relation into the orientations used
by the Section 11 commutativity argument.
References #
references/ldt-paper/commutativity-points.texreferences/ldt-paper/commutativity-G.texblueprint/src/chapter/ch08_commutativity.tex
theorem
MIPStarRE.LDT.Commutativity.evaluatedPointFamily_pointConsistency
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
(zeta : Error)
(hcons : family.ConsistentWithPoints strategy zeta)
:
ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas
(evaluatedPointFamily params family) zeta
The point-consistency relation written in local evaluated-point-family notation.
theorem
MIPStarRE.LDT.Commutativity.evaluatedPointFamily_pointConsistency_swapped
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
(params : Parameters)
[FieldModel params.q]
(strategy : SymStrat params.next ι)
(family : IdxPolyFamily params ι)
(zeta : Error)
(hcons : family.ConsistentWithPoints strategy zeta)
:
ConsRel strategy.state (uniformDistribution (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.