Section 5 — Orthonormalization #
The orthonormalization theorem and scalar bookkeeping lemmas from Section 5.
lem:orthonormalization-main-lemma.
Paper origin: references/ldt-paper/orthonormalization.tex:282-310
(\label{lem:orthonormalization-main-lemma}).
This is the source-facing orthogonalization lemma for complete measurements. The theorem statement deliberately contains no spectral-truncation or repair input: those are steps in the proof of the paper lemma, not hypotheses of the lemma. The proof uses the locality-preserving projectivization repair in its heterogeneous left-register form.
Measurement-level orthonormalization from a cross-consistency hypothesis.
This is the measurement analogue of
orthonormalizationMainLemma, with the paper's
84·ζ^{1/4} bound weakened to the public 100·ζ^{1/4} envelope.
Measurement-level orthonormalization for a complete measurement.
This is the measurement-level corollary of lem:orthonormalization-main-lemma;
it does not assume the proof-stage spectral-truncation or repair data.
Measurement-level orthonormalization from cross consistency, using the locality-preserving Section 5 repair construction directly.
This is the source-faithful form needed by the final Step 6 construction: a cross-consistency estimate for the two unsymmetrized role measurements gives the projective submeasurement without an additional spectral-truncation or repair-input hypothesis.
Heterogeneous measurement-level orthonormalization from cross consistency.
This is the two-space form of lem:orthonormalization-main-lemma needed in the
source proof of thm:main-formal: if complete measurements A and B on
possibly different local spaces are consistent on a bipartite state, then A
has a projective submeasurement close on Alice's tensor factor. No
permutation-invariance or same-space identification is used.
Faithful encoding: Paper origin:
references/ldt-paper/test_definition.tex:180-202 and
references/ldt-paper/projectivization.tex; the heterogeneous form is the
two-space tensor-factor version needed by the source proof.
Heterogeneous measurement-level orthonormalization on Bob's tensor factor.
This is the right-register counterpart of
orthonormalizationMeasurement_of_consistency_from_projectivizationRepair_heterogeneous.
If complete measurements A and B are consistent on a bipartite state, then
B has a projective submeasurement close on Bob's tensor factor. No
same-space identification or permutation-invariance hypothesis is used.
Faithful encoding: Paper origin:
references/ldt-paper/test_definition.tex:180-202 and
references/ldt-paper/projectivization.tex; the heterogeneous form is the
two-space tensor-factor version needed by the source proof.
Completion-route orthonormalization with the documented weakened constant.
This theorem preserves the proved construction obtained by completing the
submeasurement first and then applying the concrete Q/X/XHat/P repair route to
the option-completed measurement. The conversion introduces the
orthonormalizationCompletionRouteError ζ = 120 * ζ^(1/4) envelope.
This is not the source theorem thm:orthonormalization; the source theorem has
the sharper orthonormalizationError ζ = 100 * ζ^(1/4) bound and is stated below
as a separate proved theorem.
thm:orthonormalization.
A strongly self-consistent submeasurement on a permutation-invariant normalized
state admits a close projective submeasurement with the paper's
100 * ζ^(1/4) error envelope.
Paper origin: references/ldt-paper/orthonormalization.tex:67-76
(\label{thm:orthonormalization}). The earlier proved completion-route
construction remains available as orthonormalizationCompletionRoute, but its
120 * ζ^(1/4) conclusion is weaker than this source theorem. The proof below
follows the paper's completion-to-measurement reduction and then feeds the
completed measurement's 2ζ self-consistency estimate into the sharp
locality-preserving Section 5 repair route, recovering the paper's scalar
constant.