Section 5 — Locality-preserving projectivization repair #
The repair step of the proof of thm:orthonormalization: a measurement of the local algebra whose
left placement is almost projective at the 2ζ scale is close, with the paper's 84 ζ^{1/4}
envelope, to a projective submeasurement of the same local algebra. This is the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/MakingMeasurementsProjective/LocalityPreservingRepair.lean
in the port of planning/c6b-plan.md (milestone M8, section "Port conventions"), and the first
site at which the port calls the orthonormalization tier T1.
A different proof. The vendored proof passes to the reduced (marginal) density matrix of the
left factor and runs the finite-dimensional Q/X/X̂/P route there (spectral truncation, rank
reduction, a positive Gram completion), then transports the estimate back to left placements.
A vector state has no reduced density, and the route is legal only on finite spectrum, so here
the four repair theorems are proved from T1 instead
(MIPRE.Orthonormalization.povm_orthogonalization_finitePair), as Theorem G is
(SymModel.orthonormalization_of_isFinitePair_sddRel, Co/Doubling/Orthonormalization.lean):
∑ₐ ‖L(Aₐ) Ψ‖² = 1 − ∑ₐ ⟨Ψ, L(Aₐ − Aₐ²) Ψ⟩ ≥ 1 − 2ζ, hence > 1 − 3 min(ζ, 1)
(Doubling.one_sub_three_mul_min_lt), so T1 gives a projective measurement Q of the local
algebra with ∑ₐ ‖L(Aₐ − Qₐ) Ψ‖² < 27 min(ζ, 1) ≤ 84 ζ^{1/4}
(twentySeven_mul_min_le_orthonormalizationMainLemmaError).
Shape changes, in each of the four repair theorems:
- the state
ψ : QuantumState (ιA × ιB)(orι × ι) is a symmetric modelS : SymModel 𝔓 K, with both measurements local in𝔓(the vendored left/right lemmas allow two carriers; here they are narrowed to one, as milestone M3 did fortriangleSub_heterogeneous); hψ : ψ.IsNormalizedis dropped (S.ev 1 = 1is a theorem);hS : S.toBipartite.IsFinitePairandhA : NoAbelianProj S.toBipartite.opsA, the hypotheses of Theorem G and of T1, are added afterS;hζ : 0 ≤ ζbecomeshζ : 0 < ζ, the strictness of T1's hypothesis;leftLiftedProjectivizationRepairhad nohζand gains(hζ : 0 < ζ)afterζ. The caseζ = 0does not follow from the strict tier and is not needed (planning/c6b-plan.md, §5).
The right-register form keeps the hypothesis on the first player's operators and is deduced from
the left one by the swap symmetry (S.ev_L_eq_ev_R,
Preliminaries.qSDDCore_rightTensor_eq_leftTensor_of_permInv). The bridges
sddRel_of_leftPlaced_sddOpRel and sddRel_of_rightPlaced_sddOpRel mention no marginal and are
ported; the vendored ψ is implicit in them, as is S here.
New here #
twentySeven_mul_min_le_orthonormalizationMainLemmaError:27 min(ζ, 1) ≤ 84 ζ^{1/4}forζ ≥ 0, the arithmetic of T1's error against the vendored envelope.
Not ported #
diagBlock: a diagonal block of a matrix; the model has no reduced density matrix.leftMarginalDensity: the reduced density matrix of the first factor; no counterpart.leftMarginalDensity_nonneg: positivity of a reduced density matrix; no counterpart.leftMarginalState: the reduced state of the first factor; no counterpart.leftTensor_eq_blockDiagonal_const: a Kronecker identity of matrices; no counterpart.trace_blockDiagonal_const_mul_eq_sum_trace_diagBlock: a matrix trace identity; no counterpart.normalizedTrace_leftMarginalDensity_mul_eq: the trace of a reduced density matrix; no counterpart.leftMarginalState_isNormalized: normalization of a reduced state; no counterpart.leftMarginal_ev_eq: expectations in a reduced state; no counterpart.rightDiagBlock: asdiagBlock, for the second factor.rightMarginalDensity: asleftMarginalDensity, for the second factor.rightMarginalDensity_nonneg: asleftMarginalDensity_nonneg, for the second factor.rightMarginalState: asleftMarginalState, for the second factor.trace_mul_rightTensor_eq_sum_trace_rightDiagBlock: a matrix trace identity; no counterpart.normalizedTrace_rightMarginalDensity_mul_eq: as its left counterpart, for the second factor.rightMarginalState_isNormalized: as its left counterpart, for the second factor.rightMarginal_ev_eq: as its left counterpart, for the second factor.matrix_eq_zero_of_rank_eq_zero: matrix rank; only the dropped route used it.sddOpRel_rightPlaced_of_ev_eq: transport from a reduced state on one factor; only the dropped route used it.projectivizationRepair_small_error_bound: classical, imported.roundingToProjectiveError_le_orthonormalizationMainLemmaError: classical, imported.one_le_orthonormalizationMainLemmaError_of_quarter_lt: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/orthonormalization.tex, lines 534–1194
27 min(ζ, 1) ≤ 84 ζ^{1/4} for ζ ≥ 0: T1's error 9 · 3 min(ζ, 1) lies under the
vendored repair envelope.
A distance bound on left-placed raw families, whose second family has the outcomes of a
projective submeasurement P, is a distance bound on the left-placed submeasurements.
The right-placement counterpart of sddRel_of_leftPlaced_sddOpRel.
Locality-preserving repair at the 2ζ scale: in a symmetric model whose bipartite reading
is a finite pair without abelian projections in its first player's operators, a measurement A
of the local algebra whose left placement has source idempotence defect at most 2ζ, ζ > 0, is
within orthonormalizationMainLemmaError ζ = 84 ζ^{1/4} of a projective submeasurement of the
local algebra, in the left placements.
Proved from the orthonormalization tier T1 (povm_orthogonalization_finitePair) rather than the
vendored Q/X/X̂/P route; hS, hA are new and hζ is strict (module docstring).
Right-register locality-preserving repair at the 2ζ scale: the counterpart of
leftPlacedProjectivizationRepair_of_sourceAlmostProjective_two_mul for the right placement,
under the same hypotheses on the first player's operators, deduced from it by the swap symmetry
of the model.
Locality-preserving repair, in the rounded-statement form: the conclusion of
leftPlacedProjectivizationRepair_of_sourceAlmostProjective_two_mul as a
RoundedProjMeasStatement for the left-lifted measurement and the left lift of P.
Locality-preserving projectivization repair (lem:locality-preserving-projectivization):
from a source idempotence defect at most ζ > 0 for the left-lifted measurement, a projective
submeasurement of the local algebra whose left lift is within 84 ζ^{1/4}.