Section 10 commutativity points: shared-line helpers

Compatibility lemmas between sampled point pairs and shared-diagonal line questions, used by both the lift and drop comparisons: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/CommutativityPoints/SharedHelpers/SharedLine.lean in the port of planning/c6b-plan.md (milestone M1, section "Port conventions"). The outcome formulas of the bridge families of Co/CommutativityPoints/Defs.lean and the transport of the point/diagonal-line approximation to the shared-line distribution are stated for a symmetric strategy strategy : SymStrat params 𝔓 K, with the point answers placed by strategy.state.L and the line answers by strategy.state.R.

The classical half of the vendored file (the two decompositions of a shared-line question, the equivalences that forget one of its two parameters, and the averaging identities over the shared-line distribution) is not ported: this file imports the vendored file and names those declarations through an explicit open MIPStarRE.LDT.CommutativityPoints (…) list.

Not ported

• sharedDiagonalLineQuestionOfPointPair_sampledPointPair: classical, imported.
• sharedDiagonalLineQuestionOfPointPair_of_line: classical, imported.
• pointPairSharedDiagonalLine_ignore_first_equiv: classical, imported.
• pointPairSharedDiagonalLine_ignore_second_equiv: classical, imported.
• avgOver_pointPairSharedDiagonalLine_ignore_first: classical, imported.
• avgOver_pointPairSharedDiagonalLine_ignore_second: classical, imported.
• avgOver_pointPairSharedDiagonalLine_sampled_pair: classical, imported.

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.pointMeasurementProductAlongSharedLine_outcome {𝔓 : 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) (q : MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (a b : MIPStarRE.LDT.Fq params) : (pointMeasurementProductAlongSharedLine params strategy q).outcome (a, b) = strategy.state.L ((strategy.pointMeasurement (q.1.pointAt q.2.1)).outcome a * (strategy.pointMeasurement (q.1.pointAt q.2.2)).outcome b)

Outcome (a, b) of the shared-line point product, at a question (ℓ, (t_u, t_v)) with u = ℓ(t_u) and v = ℓ(t_v): it is (A^u_a A^v_b) ⊗ I, strategy.state.L of the product.

theorem MIPRE.LIDT.Co.CommutativityPoints.pointMeasurementProductAlongSharedLineReversed_outcome {𝔓 : 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) (q : MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (a b : MIPStarRE.LDT.Fq params) : (pointMeasurementProductAlongSharedLineReversed params strategy q).outcome (a, b) = strategy.state.L ((strategy.pointMeasurement (q.1.pointAt q.2.2)).outcome b * (strategy.pointMeasurement (q.1.pointAt q.2.1)).outcome a)

Outcome (a, b) of the reversed shared-line point product: it is (A^v_b A^u_a) ⊗ I, strategy.state.L of the product in the opposite order.

theorem MIPRE.LIDT.Co.CommutativityPoints.pointDiagonalLineMixedProductLeft_outcome {𝔓 : 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) (q : MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (a b : MIPStarRE.LDT.Fq params) : ((pointDiagonalLineMixedProductLeft params strategy).toIdxOpFamily q).outcome (a, b) = strategy.state.opTensor ((strategy.pointMeasurement (q.1.pointAt q.2.1)).outcome a) ((sampledDiagonalLineEvaluation params strategy (q.1, q.2.2)).outcome b)

Outcome (a, b) of the left mixed bridge: it is A^u_a ⊗ L^ℓ_[f(v)=b], the point measurement at u and the diagonal-line evaluation at t_v, placed by strategy.state.opTensor.

theorem MIPRE.LIDT.Co.CommutativityPoints.pointDiagonalLineMixedProductRight_outcome {𝔓 : 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) (q : MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (a b : MIPStarRE.LDT.Fq params) : ((pointDiagonalLineMixedProductRight params strategy).toIdxOpFamily q).outcome (a, b) = strategy.state.opTensor ((strategy.pointMeasurement (q.1.pointAt q.2.2)).outcome b) ((sampledDiagonalLineEvaluation params strategy (q.1, q.2.1)).outcome a)

Outcome (a, b) of the right mixed bridge: it is A^v_b ⊗ L^ℓ_[f(u)=a], the point measurement at v and the diagonal-line evaluation at t_u, placed by strategy.state.opTensor, the post-processing having swapped the outcome pair back.

theorem MIPRE.LIDT.Co.CommutativityPoints.diagonalLineProductOrdered_outcome {𝔓 : 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) (q : MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (a b : MIPStarRE.LDT.Fq params) : (diagonalLineProductOrdered params strategy q).outcome (a, b) = strategy.state.R ((sampledDiagonalLineEvaluation params strategy (q.1, q.2.2)).outcome b * (sampledDiagonalLineEvaluation params strategy (q.1, q.2.1)).outcome a)

Outcome (a, b) of the ordered diagonal-line product: it is I ⊗ (L^ℓ_[f(v)=b] · L^ℓ_[f(u)=a]), strategy.state.R of the product.

theorem MIPRE.LIDT.Co.CommutativityPoints.diagonalLineProductReversed_outcome {𝔓 : 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) (q : MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (a b : MIPStarRE.LDT.Fq params) : (diagonalLineProductReversed params strategy q).outcome (a, b) = strategy.state.R ((sampledDiagonalLineEvaluation params strategy (q.1, q.2.1)).outcome a * (sampledDiagonalLineEvaluation params strategy (q.1, q.2.2)).outcome b)

Outcome (a, b) of the reversed diagonal-line product: it is I ⊗ (L^ℓ_[f(u)=a] · L^ℓ_[f(v)=b]), strategy.state.R of the product.

theorem MIPRE.LIDT.Co.CommutativityPoints.sampledDiagonalLineApproximation_ignore_first {𝔓 : 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) (fun (q : MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) => OpFamily.leftPlacedOpFamily strategy.state (strategy.pointMeasurement (q.1.pointAt q.2.2)).toOpFamily) (fun (q : MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) => OpFamily.rightPlacedOpFamily strategy.state (sampledDiagonalLineEvaluation params strategy (q.1, q.2.2)).toOpFamily) (MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineApproxError params gamma)

For a good strategy, over the shared-diagonal-line distribution, the point measurement at the second point v, placed left, and the diagonal-line evaluation at t_v, placed right, are pointDiagonalLineApproxError params gamma-close (SDDOpRel): the first point is ignored, (ℓ, t_v) having the law of pointWithDiagonalLineDistribution.

theorem MIPRE.LIDT.Co.CommutativityPoints.sampledDiagonalLineApproximation_ignore_second {𝔓 : 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) (fun (q : MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) => OpFamily.leftPlacedOpFamily strategy.state (strategy.pointMeasurement (q.1.pointAt q.2.1)).toOpFamily) (fun (q : MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) => OpFamily.rightPlacedOpFamily strategy.state (sampledDiagonalLineEvaluation params strategy (q.1, q.2.1)).toOpFamily) (MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineApproxError params gamma)

For a good strategy, over the shared-diagonal-line distribution, the point measurement at the first point u, placed left, and the diagonal-line evaluation at t_u, placed right, are pointDiagonalLineApproxError params gamma-close (SDDOpRel): the second point is ignored, (ℓ, t_u) having the law of pointWithDiagonalLineDistribution.