Section 5 — Rounding to projectors, core #
The consistency-to-almost-projective step of the rounding-to-projectors chain, with its
Cauchy–Schwarz helpers, and the zero projective submeasurement used in trivial large-error
branches: the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/MakingMeasurementsProjective/Projectivization.lean in the
port of planning/c6b-plan.md (milestone M8, section "Port conventions").
One carrier. The vendored bipartite lemmas take a state ψ on ιA × ιB, a measurement on
each factor and named carrier arguments (ι₂ := ιB), (ι₁ := ιA). Here they are narrowed to a
symmetric model S : SymModel 𝔓 K, with both measurements local in 𝔓, as milestone M3 did for
triangleSub_heterogeneous ("Departures in M3 and M5"): leftTensor is S.L, rightTensor
is S.R, leftPlacedSubMeas is S.leftPlacedSubMeas and leftLiftedMeasurement is
S.leftLiftedMeasurement. Each takes the model as an explicit first argument, in the namespace
MakingMeasurementsProjective. The two-space use is served separately, by the heterogeneous
lemmas of Co/MakingMeasurementsProjective/Orthonormalization.lean
(one_sub_two_mul_le_sum_norm_sq_πA/_πB,
orthonormalizationMeasurement_{,right_}of_consistency_from_projectivizationRepair_heterogeneous),
for milestone M13.
sourceAlmostProjective_of_ssc and sourceAlmostProjective_nonneg are about a state on one
space and take a vector state V : VecState K with a joint measurement in K →L[ℂ] K.
zeroProjSubMeas mentions no state and is generic over an ordered ⋆-ring, so that it serves
the local algebra 𝔓 and the joint operators alike. The vendored hypotheses hψ : ψ.IsNormalized
of the two qSDD_*Placed_zeroProjSubMeas_le_one lemmas are dropped (S.ev 1 = 1 is a theorem),
and their entrywise matrix step is map_zero. The unused vendored instance arguments
[DecidableEq Outcome] of consistencyToAlmostProjective and its right form are dropped.
The pure real inequality totalMass_sub_two_defect_le_diagA and the error function
consistencyToAlmostProjectiveError are classical; they are imported from the vendored
Projectivization.lean and Defs.lean and named through an explicit open list.
Not ported #
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/orthonormalization.texblueprint/src/chapter/ch04_projective.tex
Lower bound for the diagA sum in terms of the overlap and the bipartite consistency defect,
obtained from the Cauchy–Schwarz squared bound. Upstream keeps it private since its
Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy.
Orthonormalization helper lemmas #
S.L (A_a) * star (S.L (A_a)) = S.L (A_a * A_a) for the self-adjoint outcomes of a
submeasurement.
The right-placement analogue of leftTensor_outcome_mul_conjTranspose_eq:
star (S.R (B_a)) * S.R (B_a) = S.R (B_a * B_a).
Cauchy–Schwarz bound for the overlap ∑ₐ ⟨Ψ, (A_a ⊗ B_a) Ψ⟩, in terms of the left and right
diagonal masses.
The left diagonal mass ∑ₐ ⟨Ψ, S.L (A_a²) Ψ⟩ is nonnegative.
The right diagonal mass ∑ₐ ⟨Ψ, S.R (B_a²) Ψ⟩ is nonnegative.
The overlap ∑ₐ ⟨Ψ, (A_a ⊗ B_a) Ψ⟩ of two measurements is at most the total mass
⟨Ψ, Ψ⟩, since B_a ≤ 1 and A is complete.
The consistency defect of (A, B) controls the strong self-consistency defect of the
left-placed A: qSSCDefect (S.leftPlacedSubMeas A) ≤ 2 · qBipartiteConsDefect A B.
The consistency defect of (A, B) controls the strong self-consistency defect of the
right-placed B: the right-register counterpart of
qSSCDefect_leftPlacedMeasurement_le_two_qBipartiteConsDefect, by the same Cauchy–Schwarz
calculation with the two diagonal masses interchanged.
Almost projectivity from strong self-consistency #
A measurement whose strong self-consistency defect is at most η has idempotence defect
∑ₐ ⟨Ψ, (A_a − A_a²) Ψ⟩ at most η.
The source idempotence defect ∑ₐ ⟨Ψ, (A_a − A_a²) Ψ⟩ of a measurement is nonnegative.
Consistency implies almost projectivity #
Consistency implies almost projective: if A is ζ-consistent with B, then the
left-lifted A is 2ζ-almost-projective.
Right-register form of consistencyToAlmostProjective: if A and B are ζ-consistent,
then the right-lifted B is 2ζ-almost-projective.
The zero projective submeasurement #
The zero family is a projective submeasurement. This supplies trivial large-error branches
where the target error bound is already at least the universal qSDD ≤ 1 estimate.
Equations
- MIPRE.LIDT.Co.MakingMeasurementsProjective.zeroProjSubMeas = { outcome_pos := ⋯, sum_eq_total := ⋯, total_le_one := ⋯, proj := ⋯ }
Instances For
The zero projective submeasurement, placed on the first factor, is within unit qSDD of any
left-placed submeasurement.
The zero projective submeasurement, placed on the second factor, is within unit qSDD of
any right-placed submeasurement.