Section 10 commutativity points: answer-valued diagonal measurements

This file proves the commutativity-at-points theorem using the answer-valued diagonal-line verifier relation: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/CommutativityPoints/AnswerTheorems.lean in the port of planning/c6b-plan.md (milestone M1, section "Port conventions"). The conclusion concerns only the point measurements, hence it can later be transferred to the ordinary carrier used by self-improvement, but the proof does not use the carrier's inert diagonal measurement.

The strategy is an answer-valued symmetric strategy strategy : AnswerSymStrat params 𝔓 K: the point answers are placed by strategy.state.L, the line answers by strategy.state.R, and the joint operators are K →L[ℂ] K. The answer-valued route is ported as the vendored file has it, parallel to the bridge theorems for SymStrat and not unified with them. The vendored file has no classical content, so it is not imported; the classical names it uses come from the vendored Defs, Approximation and SharedHelpers/SharedLine through the imports of Co/CommutativityPoints/SharedHelpers/SharedLine.lean, named by an explicit open MIPStarRE.LDT.CommutativityPoints (…) list.

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.

def MIPRE.LIDT.Co.CommutativityPoints.answerSampledPointMeasurement {𝔓 : 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 : AnswerSymStrat params 𝔓 K) : IdxSubMeas (MIPStarRE.LDT.CommutativityPoints.PointDiagonalLineQuestion params) (MIPStarRE.LDT.Fq params) 𝔓

The point measurement, reindexed by a sampled diagonal line and a parameter on it, for an answer-valued strategy.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.answerSampledDiagonalLineEvaluation {𝔓 : 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 : AnswerSymStrat params 𝔓 K) : IdxSubMeas (MIPStarRE.LDT.CommutativityPoints.PointDiagonalLineQuestion params) (MIPStarRE.LDT.Fq params) 𝔓

Evaluate an answer-valued diagonal-line measurement at the sampled parameter.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.answerPointMeasurementProductLeft {𝔓 : 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 : AnswerSymStrat params 𝔓 K) : IdxOpFamily (MIPStarRE.LDT.GlobalVariance.PointPairQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The ordered point product (A^u_a A^v_b) ⊗ I for an answer-valued strategy, placed by strategy.state.L.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.answerPointMeasurementProductRight {𝔓 : 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 : AnswerSymStrat params 𝔓 K) : IdxOpFamily (MIPStarRE.LDT.GlobalVariance.PointPairQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The reversed point product (A^v_b A^u_a) ⊗ I for an answer-valued strategy, placed by strategy.state.L.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.answerPointMeasurementProductAlongSharedLine {𝔓 : 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 : AnswerSymStrat params 𝔓 K) : IdxOpFamily (MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The ordered point product, indexed by a shared sampled line.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.answerPointMeasurementProductAlongSharedLineReversed {𝔓 : 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 : AnswerSymStrat params 𝔓 K) : IdxOpFamily (MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The reversed point product, indexed by a shared sampled line.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.answerPointDiagonalLineMixedProductLeft {𝔓 : 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 : AnswerSymStrat params 𝔓 K) : IdxSubMeas (MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The mixed bridge A^u_a ⊗ L^ℓ_[f(v)=b], placed by strategy.state.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.answerDiagonalLineProductOrdered {𝔓 : 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 : AnswerSymStrat params 𝔓 K) : IdxOpFamily (MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The bridge I ⊗ (L^ℓ_[f(v)=b] · L^ℓ_[f(u)=a]), placed by strategy.state.R.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.answerDiagonalLineProductReversed {𝔓 : 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 : AnswerSymStrat params 𝔓 K) : IdxOpFamily (MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The swapped bridge I ⊗ (L^ℓ_[f(u)=a] · L^ℓ_[f(v)=b]), placed by strategy.state.R.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.CommutativityPoints.answerPointDiagonalLineMixedProductRight {𝔓 : 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 : AnswerSymStrat params 𝔓 K) : IdxSubMeas (MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (MIPStarRE.LDT.CommutativityPoints.PointPairOutcome params) (K →L[ℂ] K)

The mixed bridge A^v_b ⊗ L^ℓ_[f(u)=a], placed by strategy.state, with outcome (a, b): a indexes the line evaluation and b the point measurement.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.LIDT.Co.CommutativityPoints.answerPointDiagonalLineMixedProductLeft_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 : AnswerSymStrat params 𝔓 K) (q : MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (a b : MIPStarRE.LDT.Fq params) : ((answerPointDiagonalLineMixedProductLeft params strategy).toIdxOpFamily q).outcome (a, b) = strategy.state.opTensor ((strategy.pointMeasurement (q.1.pointAt q.2.1)).outcome a) ((answerSampledDiagonalLineEvaluation 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 answer-valued diagonal-line evaluation at t_v, placed by strategy.state.opTensor.

theorem MIPRE.LIDT.Co.CommutativityPoints.answerPointDiagonalLineMixedProductRight_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 : AnswerSymStrat params 𝔓 K) (q : MIPStarRE.LDT.CommutativityPoints.PointPairDiagonalLineQuestion params) (a b : MIPStarRE.LDT.Fq params) : ((answerPointDiagonalLineMixedProductRight params strategy).toIdxOpFamily q).outcome (a, b) = strategy.state.opTensor ((strategy.pointMeasurement (q.1.pointAt q.2.2)).outcome b) ((answerSampledDiagonalLineEvaluation 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 answer-valued 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.answerSampledDiagonalLineApproximation_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 : AnswerSymStrat 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 (answerSampledDiagonalLineEvaluation params strategy (q.1, q.2.2)).toOpFamily) (MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineApproxError params gamma)

For a good answer-valued strategy, over the shared-diagonal-line distribution, the point measurement at the second point v, placed left, and the answer-valued 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.answerSampledDiagonalLineApproximation_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 : AnswerSymStrat 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 (answerSampledDiagonalLineEvaluation params strategy (q.1, q.2.1)).toOpFamily) (MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineApproxError params gamma)

For a good answer-valued strategy, over the shared-diagonal-line distribution, the point measurement at the first point u, placed left, and the answer-valued 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.

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

Lean-only: A local tensor-placement comparison in the answer-valued point-commutativity chain.

Paper origin: upstream references/ldt-paper/commutativity_points.tex; this is one of the formal transport steps used to realize the mixed point/diagonal comparison appearing in the paper. It is internal to the answer-valued implementation tracked in upstream issue #1507 and is not a source theorem. Discharge: proved here from the already formalized point-to-diagonal-line approximation and tensor-ordering identities.

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

Lean-only: A local tensor-placement comparison from the mixed product to the ordered diagonal-line product.

Paper origin: upstream references/ldt-paper/commutativity_points.tex; this is an internal reindexing and tensor-ordering step in the answer-valued point-commutativity route tracked in upstream issue #1507. Discharge: proved here by transporting the point-to-line comparison through the explicit ordered product identities.

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

Lean-only: A local tensor-placement comparison from the ordered diagonal-line product to the reversed mixed product.

Paper origin: upstream references/ldt-paper/commutativity_points.tex; this is an internal answer-valued implementation step for the point-commutativity argument tracked in upstream issue #1507. Discharge: proved here from the reversed point-to-line comparison and the explicit ordered/reversed product equality.

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

Lean-only: A local tensor-placement comparison from the reversed mixed product back to the reversed point product.

Paper origin: upstream references/ldt-paper/commutativity_points.tex; this is the last internal answer-valued transport step in the point-commutativity chain tracked in upstream issue #1507. Discharge: proved here from the line-to-point comparison and the explicit tensor-placement identities.

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

Answer-valued form of thm:commutativity-points.

The proof is the paper's diagonal-line bridge argument, but the diagonal-line measurement is the answer-valued measurement of strategy.