Section 5 — Orthonormalization #
The orthonormalization theorem thm:orthonormalization and the measurement-level lemma
lem:orthonormalization-main-lemma: the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/MakingMeasurementsProjective/Orthonormalization.lean in the
port of planning/c6b-plan.md (milestone M8, section "Port conventions"). It holds the second and
third sites at which the port calls the orthonormalization tier T1, and the top-level theorem.
Same-space theorems. The state ψ is a symmetric model S : SymModel 𝔓 K, with every
measurement local in 𝔓; hperm : PermInvState ψ and hψ : ψ.IsNormalized are dropped (the
swap symmetry and S.ev 1 = 1 are theorems). Every theorem that reaches T1 takes
hS : S.toBipartite.IsFinitePair and hA : NoAbelianProj S.toBipartite.opsA right after S,
and hζ : 0 < ζ in place of 0 ≤ ζ; orthonormalizationCompletionRoute and orthonormalization,
which had no hζ, gain (hζ : 0 < ζ) after ζ. The case ζ = 0 does not follow from the strict
tier and is not needed (planning/c6b-plan.md, §5). bipartiteSSCRel_self_of_measurement and
leftLiftedRoundedProjMeasStatement_to_local call no tier and take no new hypothesis.
orthonormalizationMainLemma is narrowed from two carriers ιA, ιB to one, as milestone M3
narrowed triangleSub_heterogeneous. The vendored A.liftLeft is A.map S.L, and the unused
vendored [DecidableEq Outcome] of leftLiftedRoundedProjMeasStatement_to_local is dropped.
orthonormalization is Theorem G (SymModel.orthonormalization_of_isFinitePair_sddRel,
Co/Doubling/Orthonormalization.lean) in one line: the vendored completion chain is not run again.
Its in-core call (the vendored SelfImprovementTop/Core.lean, line 433, milestone M10) must supply
0 < selfImprovementHelperError, which holds when 1 ≤ params.d, threaded from SoundIn by
milestone M14. orthonormalizationCompletionRoute keeps the vendored completion chain (the
completion optionCompletion, its 2ζ bound Completion.optionCompletion_bipartiteSSCRel, the
repair leftLiftedProjectivizationRepair and the restriction
Completion.qSDD_liftLeft_restrictSomeProjSubMeas_le), with the weaker 120 ζ^{1/4} envelope.
Two-space theorems. The two …_heterogeneous lemmas are stated over a dyadic pair
M : MIPRE.BipartiteModel 𝒞 𝒜 ℬ (BipartiteModel.IsDyadicPair), with A a measurement of the
first player's algebra and B of the second's, and call T5
(povm_orthogonalization_dyadicPair, povm_orthogonalization_dyadicPairB). Their vendored state
is on ιA × ιB and their only vendored callers are the two-space ProjStrat of
Test/MainTheorem/SourceRoleRegister/Core.lean (lines 507 and 547), which milestone M13 ports, so
a narrowing to one carrier would duplicate
orthonormalizationMeasurement_of_consistency_from_projectivizationRepair. This departs from the
narrowing rule, as the two-space defect of milestone M2 did (Co/Test/StrategyBiProj/Measurements.lean):
- the hypothesis is the two-space defect
bipartiteConsError M (uniformDistribution Unit) … ≤ ζ(the port has no two-spaceConsRel, "Same-space and bipartite quantities"); - the conclusion
∑ₐ ‖π(πA(Aₐ − Pₐ)) ψ‖² ≤ 100 ζ^{1/4}(or withℬ,πB,B) replaces the vendoredSDDRelof the left (right) placements, which mentions a state on the product space. The proof is the vendored Cauchy–Schwarz chain withbornProb(one_sub_two_mul_le_sum_norm_sq_πA), then the tier atε = 3 min(ζ, 1)(Doubling.one_sub_three_mul_min_lt) and27 min(ζ, 1) ≤ 100 ζ^{1/4}(Doubling.twentySeven_mul_min_le_orthonormalizationError). There is nohψ-free form: the two-space model carries no normalization, sohψ : ‖M.ψ‖ = 1stays.
The vendored files of MakingMeasurementsProjective that have no port, since the pairing
script checks only ported files:
Defs.lean(320 lines): its error functions (orthonormalizationError,orthonormalizationCompletionRouteError,orthonormalizationMainLemmaError,consistencyToAlmostProjectiveError,spectralTruncationError,roundingToProjectiveError) are classical and imported from the vendored file; the rest is matrix-only (FiniteHilbertSpace,MatrixOperator,PositiveMatrixState,MatrixSubmeasurement,MatrixMeasurement,matrixExpectation,naimarkAuxProjector,oneMeasLiftedDensity,OneMeasNaimarkData,NaimarkData), consumed only by the not-portedMatrixRealizationandSdpMatrixBridge(replaced by milestone M5's Gram positivity and M9's summed form) and by M5's vendored imports ofExpansionHypercubeGraph/{Defs/Core,Theorems/Foundations,Theorems/Matrix,Theorems/Results}, whose matrix content M5 replaced by Gram positivity.Orthonormalization/ErrorBounds.lean(142 lines): wholly classical scalar bookkeeping, imported by this file, as milestone M3 importsPolynomials.lean.NaimarkCore.lean(404 lines): the matrix Naimark dilation; nothing outsideMakingMeasurementsProjectivenames it, and the model route needs no dilation (T1 orthonormalizes inside the algebra).QXPLayer/{Core, QCompleteness, AlmostProjective, TruncationCombinatorics, RankReduction/LowRank, RankReduction/Sigma}.lean(2,478 lines): the finite-dimensionalQ/X/X̂/Proute (rank reduction, finite-spectrum functional calculus, cardinality counts), replaced by T1 (povm_orthogonalization_finitePairin the repair theorems ofCo/MakingMeasurementsProjective/LocalityPreservingRepair.lean, T5 in the heterogeneous lemmas here, Theorem G inorthonormalization); no declaration of it is used outsideMakingMeasurementsProjective.QXPLayerIdentities/{LayerAlgebra, ProjectorApprox, RectangularSvd, PositiveGram/Rows, PositiveGram/Completion, PositiveGram/Sigma}.lean(3,140 lines): matrix identities of the same route (rectangular SVD, coisometries, positive Gram completion), replaced by T1 as above. The vendoredProjectivizationChain/Basic.lean, imported for its classical names, keepsProjectorApproxin the import closure; no port file names it.SpectralTruncation/{Conversion, ProjectiveNonMeasurement}.lean(914 lines): a step-function calculus legal only on finite spectrum, replaced by T1; its conclusionSpectralTruncationStatementis listed as not ported inCo/MakingMeasurementsProjective/Statements.lean.
New here #
one_sub_two_mul_le_sum_norm_sq_πA: in a bipartite model with a unit state, a two-space consistency defect at mostζbetween measurementsAof𝒜andBofℬgives1 − 2ζ ≤ ∑ₐ ‖π(πA(Aₐ)) ψ‖².one_sub_two_mul_le_sum_norm_sq_πB: the same forB,1 − 2ζ ≤ ∑ₐ ‖π(πB(Bₐ)) ψ‖².
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/orthonormalization.tex, lines 67–76 and 282–310
Same-space orthonormalization #
lem:orthonormalization-main-lemma: 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 ζ-consistent with a measurement B, ζ > 0, is within
orthonormalizationMainLemmaError ζ = 84 ζ^{1/4} of a projective submeasurement, in the left
placements: consistency gives almost projectivity at 2ζ (consistencyToAlmostProjective), and
the locality-preserving repair at the 2ζ scale closes it.
Paper origin: references/ldt-paper/orthonormalization.tex:282-310.
For a complete measurement, bipartite strong self-consistency is bipartite consistency of A
with itself.
A rounded-projective witness for the left-lifted measurement, whose projective submeasurement is a left lift, is a distance bound on the left lifts.
Measurement-level orthonormalization from a cross-consistency hypothesis: the analogue of
orthonormalizationMainLemma for the left lifts, with the paper's 84 ζ^{1/4} weakened to the
public 100 ζ^{1/4} envelope.
Measurement-level orthonormalization for a complete measurement: the measurement-level
corollary of lem:orthonormalization-main-lemma, through the consistency of A with itself.
Measurement-level orthonormalization from cross consistency, through the locality-preserving
repair at the ζ scale applied to the 2ζ-almost-projective left lift
(leftLiftedProjectivizationRepair): 84 (2ζ)^{1/4} ≤ 100 ζ^{1/4}.
Completion-route orthonormalization, with the weaker orthonormalizationCompletionRouteError ζ = 120 ζ^{1/4} envelope: complete A by the outcome none
(Completion.optionCompletion_bipartiteSSCRel, at 2ζ), apply the repair to the completed
measurement at consistencyToAlmostProjectiveError (2ζ) = 4ζ, and drop the outcome none
(Completion.qSDD_liftLeft_restrictSomeProjSubMeas_le). The source theorem, with the sharper
100 ζ^{1/4}, is orthonormalization.
thm:orthonormalization: in a symmetric model whose bipartite reading is a finite pair
without abelian projections in its first player's operators, a submeasurement A of the local
algebra that is ζ-strongly self-consistent, ζ > 0, is within the paper's
orthonormalizationError ζ = 100 ζ^{1/4} of a projective submeasurement, in the left placements.
This is Theorem G (SymModel.orthonormalization_of_isFinitePair_sddRel). The in-core call of the
vendored SelfImprovementTop/Core.lean (line 433, milestone M10) must supply
0 < selfImprovementHelperError, which holds when 1 ≤ params.d, threaded from SoundIn by
milestone M14.
Paper origin: references/ldt-paper/orthonormalization.tex:67-76.
Two-space orthonormalization in a dyadic pair #
Consistency gives mass on the first player's side: in a bipartite model with a unit
state, if the two-space consistency defect of measurements A of 𝒜 and B of ℬ is at most
ζ, then 1 − 2ζ ≤ ∑ₐ ‖π(πA(Aₐ)) ψ‖².
Consistency gives mass on the second player's side: the counterpart of
one_sub_two_mul_le_sum_norm_sq_πA for B, 1 − 2ζ ≤ ∑ₐ ‖π(πB(Bₐ)) ψ‖².
Heterogeneous orthonormalization on the first player's side: in a dyadic pair with a unit
state, if measurements A of 𝒜 and B of ℬ have two-space consistency defect at most
ζ > 0, then A is within ∑ₐ ‖π(πA(Aₐ − Pₐ)) ψ‖² ≤ 100 ζ^{1/4} of a projective
submeasurement P of 𝒜.
The two-space form of lem:orthonormalization-main-lemma, consumed by milestone M13
(Test/MainTheorem/SourceRoleRegister); it departs from the narrowing rule as the two-space
defect of milestone M2 did (module docstring).
Heterogeneous orthonormalization on the second player's side: the counterpart of
orthonormalizationMeasurement_of_consistency_from_projectivizationRepair_heterogeneous for B,
∑ₐ ‖π(πB(Bₐ − Pₐ)) ψ‖² ≤ 100 ζ^{1/4} for a projective submeasurement P of ℬ, through the
second player's form of the tier (povm_orthogonalization_dyadicPairB).