Source-Boundary Role-Register Handoff: Final Point Consistency #
This module contains the final completed-measurement and point-consistency
statements used by the paper-facing thm:main-formal route.
Alice-side projective submeasurement from the source role-register route.
This theorem combines the source role-register Step 5 theorem with the
heterogeneous orthonormalization lemma. It is not the final theorem: it only
constructs the Alice-side projective submeasurement and its left-factor
state-dependent-distance estimate. The Bob-side construction, completion to
projective measurements, line-169 transport, scalar absorption, and source
boundary remain separate work. The role-register input uses the confirmed
large-k correction to thm:main-induction; this theorem itself adds no
bridge, package, residual, repair, producer, input, or generic hypothesis.
Two-sided projective submeasurements from the source role-register route.
This theorem combines the source role-register Step 5 theorem with the
heterogeneous orthonormalization lemmas on both tensor factors. It is still not
the final theorem: it constructs projective submeasurements and the two
state-dependent-distance estimates. Completion to projective measurements,
line-169 transport, and scalar absorption remain separate work. The
role-register input uses the confirmed large-k correction to
thm:main-induction; this theorem itself adds no bridge, package, residual,
repair, producer, input, or generic hypothesis.
Completed projective measurements from the source role-register route.
This theorem carries the heterogeneous role-register construction through the
completion step in references/ldt-paper/inductive_step.tex:143-149. Starting
from the paper hypotheses for the two-space strategy, it constructs the
complete polynomial measurements G_A,G_B, the projective submeasurements
P_A,P_B, and the completed projective measurements Q_A,Q_B, together with
the two tensor-factor state-dependent-distance estimates at the literal
orthonormalize-and-complete error.
It is still not thm:main-formal: the remaining source-route work is the
line-169 transport from the polynomial measurements to the point measurements,
and the scalar absorption into mainFormalError. The role-register input uses
the confirmed large-k correction to thm:main-induction; the completion
argument in this theorem itself adds no bridge, package, residual, repair,
producer, input, or generic hypothesis.
Final point-consistency estimates obtained from the source role-register route before scalar absorption.
Paper origin: references/ldt-paper/inductive_step.tex:158-185. This theorem
derives the point-evaluation triangle estimates from the completed projective
measurements. No point-consistency estimate is assumed: the two line-169
polynomial consistency relations are first postprocessed by evaluation, and the
Q_A,Q_B estimate is derived from the original G_A,G_B consistency together
with the two completion-distance estimates.
The displayed errors are the literal errors produced by the heterogeneous
triangle inequalities used here. Absorbing these scalar expressions into the
single mainFormalError bound is a separate final step.