Section 5 — basic projectivization data

The right-register transport of the state-dependent distance and the residual hypotheses passed to the self-consistency handoff of the orthonormalization projectivization chain: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/MakingMeasurementsProjective/ProjectivizationChain/Basic.lean in the port of planning/c6b-plan.md (milestone M8, section "Port conventions").

The mathematical source is the orthonormalization-and-completion argument of inductive_step.tex, lines 130–149. The vendored file also records the scalar of that argument, ζ₂ = 2 · (100·ζ^{1/4}) + 4 · √(100·ζ^{1/4}) + 2·ζ, and its absorbed form 200·ζ^{1/4} + 42·ζ^{1/8}. Those three declarations are classical; they are imported from the vendored file, not ported, and consumers name them through an explicit open MIPStarRE.LDT.MakingMeasurementsProjective (orthonormalizeAndCompleteError …) list. Inside MIPRE.LIDT.Co, a dotted MakingMeasurementsProjective.X resolves to the namespace of the port and does not find them.

The vendored transport lemmas ask for a permutation-invariant state, which determined the state implicitly. Here swap symmetry is a theorem of the model (S.ev_L_eq_ev_R, through Preliminaries.qSDDCore_rightTensor_eq_leftTensor_of_permInv), so hperm is dropped and the model S : SymModel 𝔓 K is explicit. The vendored lifts A.liftLeft, A.liftRight are A.map S.L, A.map S.R on submeasurements and IdxSubMeas.liftLeft S, IdxSubMeas.liftRight S on indexed families. ProjectivizationSelfConsistencyHandoff is a SymModel structure, with its fields verbatim.

Not ported

• orthonormalizeAndCompleteError: classical, imported.
• sqrt_orthonormalizationError_eq: classical, imported.
• orthonormalizeAndCompleteError_le_absorbedZeta2: classical, imported.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/inductive_step.tex lines 130–149
• references/ldt-paper/orthonormalization.tex lines 67–77 (thm:orthonormalization)
• references/ldt-paper/preliminaries.tex lines 1101–1170 (prop:completing-to-measurement)

Right-register transport

theorem MIPRE.LIDT.Co.MakingMeasurementsProjective.qSDD_liftRight_eq_liftLeft_of_permInv {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A B : SubMeas Outcome 𝔓) : S.qSDD (SubMeas.map S.R A) (SubMeas.map S.R B) = S.qSDD (SubMeas.map S.L A) (SubMeas.map S.L B)

The state-dependent distance between right placements of two local submeasurements equals the distance between their left placements.

This is the bookkeeping for the Bob-side completion estimate of inductive_step.tex, lines 140–147: the orthonormalize-and-complete step returns a left-register bound, and the paper also uses the right-register bound. It is the submeasurement case of Preliminaries.qSDDCore_rightTensor_eq_leftTensor_of_permInv.

theorem MIPRE.LIDT.Co.MakingMeasurementsProjective.sddRel_liftRight_of_liftLeft_permInv {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A B : IdxSubMeas Question Outcome 𝔓) (δ : ℝ) : S.SDDRel 𝒟 (IdxSubMeas.liftLeft S A) (IdxSubMeas.liftLeft S B) δ → S.SDDRel 𝒟 (IdxSubMeas.liftRight S A) (IdxSubMeas.liftRight S B) δ

Transport an SDDRel bound from left lifts to right lifts.

Projective self-consistency handoff

structure MIPRE.LIDT.Co.MakingMeasurementsProjective.ProjectivizationSelfConsistencyHandoff {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (G_A G_B : Measurement Outcome 𝔓) (Q_A Q_B : ProjMeas Outcome 𝔓) (ζ₁ ζ₂ : ℝ) : Prop

Handoff data for the projective-measurement part of the orthonormalization proof.

The three fields record the paper's pre-projective consistency and the two completion-closeness estimates of inductive_step.tex, lines 130–149: the hypotheses needed once the orthonormalization and completion constructions have produced projective measurements Q_A, Q_B close to the pre-projective measurements G_A, G_B.

• preProjectiveConsistency : S.ConsRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ζ₁

  Paper line 131, obtained before the projective measurements are produced.

• leftCompletionCloseness : S.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (SubMeas.map S.L G_A.toSubMeas)) (constSubMeasFamily (SubMeas.map S.L Q_A.toSubMeas)) ζ₂

  Left-register completion closeness, paper line 146 (eq:G-with-Q-A).

• rightCompletionCloseness : S.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (SubMeas.map S.R G_B.toSubMeas)) (constSubMeasFamily (SubMeas.map S.R Q_B.toSubMeas)) ζ₂

  Right-register completion closeness, paper line 147.