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, and the theorem itself, commutativityPoints (thm:commutativity-points): the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/CommutativityPoints/BridgeTheorems/DropBridges.lean in the port of planning/c6b-plan.md (milestone M1, section "Port conventions"). The strategy is a symmetric one, strategy : SymStrat params 𝔓 K, with the point answers placed by strategy.state.L and the line answers by strategy.state.R; the conclusion is the vendored one, an SDDOpRel of the vector state of strategy.state between the two orders of a product of point measurements. The flip of the model is not used.

As in BridgeTheorems/LiftBridges.lean, the hypothesis of Preliminaries.cabApproxDelta_raw on a lifted submeasurement is liftLeft_sum_adjoint_mul_le_one / liftRight_sum_adjoint_mul_le_one.

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
• blueprint/src/chapter/ch08_commutativity.tex

In this repository: lem:co-commutativity-points in blueprint/src/content/08_downstream.tex.

theorem MIPRE.LIDT.Co.CommutativityPoints.reversedDropFromLineComparison {𝔓 : 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 𝔓 K) (eps delta gamma : ℝ) (hgood : strategy.IsGood eps delta gamma) : strategy.state.SDDOpRel (MIPStarRE.LDT.CommutativityPoints.pointPairSharedDiagonalLineDistribution params) (diagonalLineProductReversed params strategy) (pointDiagonalLineMixedProductRight params strategy).toIdxOpFamily (MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineApproxError params gamma)

Third replacement step: for a good strategy, over the shared-diagonal-line distribution, the reversed line product I ⊗ (L^ℓ_[f(u)=a] · L^ℓ_[f(v)=b]) and the right mixed bridge A^v_b ⊗ L^ℓ_[f(u)=a] are pointDiagonalLineApproxError params gamma-close (SDDOpRel).

theorem MIPRE.LIDT.Co.CommutativityPoints.orderedDropFromLineComparison {𝔓 : 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 𝔓 K) (eps delta gamma : ℝ) (hgood : strategy.IsGood eps delta gamma) : strategy.state.SDDOpRel (MIPStarRE.LDT.CommutativityPoints.pointPairSharedDiagonalLineDistribution params) (diagonalLineProductOrdered params strategy) (pointDiagonalLineMixedProductRight params strategy).toIdxOpFamily (MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineApproxError params gamma)

The third replacement step for the ordered line product: the ordered line product I ⊗ (L^ℓ_[f(v)=b] · L^ℓ_[f(u)=a]) and the right mixed bridge A^v_b ⊗ L^ℓ_[f(u)=a] are pointDiagonalLineApproxError params gamma-close (SDDOpRel), the two line evaluations commuting as postprocessings of one diagonal-line measurement.

theorem MIPRE.LIDT.Co.CommutativityPoints.reversedDropToPointsComparison {𝔓 : 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 𝔓 K) (eps delta gamma : ℝ) (hgood : strategy.IsGood eps delta gamma) : strategy.state.SDDOpRel (MIPStarRE.LDT.CommutativityPoints.pointPairSharedDiagonalLineDistribution params) (pointDiagonalLineMixedProductRight params strategy).toIdxOpFamily (pointMeasurementProductAlongSharedLineReversed params strategy) (MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineApproxError params gamma)

Final replacement step: for a good strategy, over the shared-diagonal-line distribution, the right mixed bridge A^v_b ⊗ L^ℓ_[f(u)=a] and the reversed point product (A^v_b A^u_a) ⊗ I are pointDiagonalLineApproxError params gamma-close (SDDOpRel).

theorem MIPRE.LIDT.Co.CommutativityPoints.commutativityPoints {𝔓 : 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 𝔓 K) (eps delta gamma : ℝ) (hgood : strategy.IsGood eps delta gamma) : strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.GlobalVariance.PointPairQuestion params)) (pointMeasurementProductLeft params strategy) (pointMeasurementProductRight params strategy) (MIPStarRE.LDT.CommutativityPoints.commutativityPointsError params gamma)

thm:commutativity-points.