Source-Boundary Role-Register Handoff: Core Reductions #
This module contains the main-induction handoff, unsymmetrization, and the first
two-space projectivization outputs for the source route toward thm:main-formal.
Apply the source-shaped main-induction theorem to the heterogeneous role-register symmetrization of a two-space strategy.
Paper origin: references/ldt-paper/inductive_step.tex:26-83, where the
general projective strategy of thm:main-formal is symmetrized by adding role
registers and thm:main-induction is applied to the resulting symmetric
strategy.
This theorem is not a proof of thm:main-formal: it stops at the polynomial
measurement produced by corrected large-k main induction on the role-register
space. It does, however, discharge the Step 1 handoff for the two-space
strategy container under the confirmed 400md correction. The downstream
unsymmetrization and two-sided projective-submeasurement construction are
formalized later in this file; completion, line-169 transport, and scalar
absorption remain separate.
Unsymmetrize the two point-consistency estimates obtained from a role-register source-induction measurement.
Paper origin: references/ldt-paper/inductive_step.tex:84-109.
This theorem is the quantitative part of the heterogeneous role-register
reduction before the later projectivization and completion steps. It starts
from the consistency estimate produced on the role-register symmetrized
strategy and extracts the two occupied principal blocks of the polynomial
measurement. The factor 2 is exactly the factor coming from the two role
sectors in the symmetrized state.
This statement is source-boundary infrastructure, not a replacement for
thm:main-formal: the extracted measurements are complete measurements, not
yet projective measurements, and the error has not yet been absorbed into
mainFormalError.
Passing the two-space low individual degree test bounds the point-agreement
branch by 3ε.
It follows because the point-agreement branch is one of the three nonnegative
terms averaged in ProjStrat.lowIndividualDegreeFailureProbability.
The two-space Step 5 self-consistency calculation before projectivization.
Paper origin: references/ldt-paper/inductive_step.tex:111-133.
Starting from the two unsymmetrized estimates
G^A_[g(u)=a] \otimes I \simeq_\sigma I \otimes A^{B,u}_a and
A^{A,u}_a \otimes I \simeq_\sigma I \otimes G^B_[g(u)=a],
the original point-agreement branch of the test gives the evaluated polynomial
consistency at error σ + 2 sqrt(3ε + σ). The heterogeneous
Schwartz--Zippel Step 5 lemma then gives full-polynomial consistency with the
additional md/q loss.
The two unsymmetrized polynomial measurements obtained from the source-shaped role-register main-induction call.
Paper origin: references/ldt-paper/inductive_step.tex:68-109.
This theorem packages the first two quantitative conclusions of the
role-register reduction in the proof of thm:main-formal: after applying
source main induction to the heterogeneous role-register symmetrization, the
occupied principal blocks of the resulting polynomial measurement are
consistent with the original two-space point measurements, with the expected
factor-two loss.
It is not the final theorem. The outputs here are complete polynomial
measurements, not projective measurements, and no self-consistency conclusion is
claimed. Those are the later projectivization, completion, and scalar
absorption steps in references/ldt-paper/inductive_step.tex:111-185.
It uses the corrected large-k main-induction handoff; no additional bridge,
package, residual, repair, producer, input, or generic hypothesis is introduced
at the theorem boundary.
Complete polynomial measurements obtained from the two-space source role-register route, including full-polynomial self-consistency.
Paper origin: references/ldt-paper/inductive_step.tex:68-133.
This is the source-boundary route through the end of the paper's Schwartz--Zippel Step 5 calculation. It applies source main induction to the heterogeneous role-register symmetrization, extracts the occupied principal blocks, proves the two factor-two point-consistency estimates, and then applies the heterogeneous triangle and Schwartz--Zippel calculation to obtain full-polynomial consistency.
It is still not thm:main-formal: the measurements are complete POVMs, not
projective measurements, and the scalar cascade has not yet been absorbed into
mainFormalError.
It uses the corrected large-k role-register handoff and remains an
intermediate construction, not the final theorem.
Alice-side projective submeasurement obtained from a two-space complete-measurement Step 5 output.
Paper origin: references/ldt-paper/inductive_step.tex:135-143, applying
lem:orthonormalization-main-lemma to the complete polynomial measurements
whose full-polynomial consistency has just been proved.
This is a genuine two-space consequence of the source-facing orthonormalization
lemma. It constructs the Alice-side projective submeasurement from the
complete measurement G_A and the cross-consistency relation with G_B, without
assuming permutation-invariance or identifying the two local Hilbert spaces.
Bob-side projective submeasurement obtained from a two-space complete-measurement Step 5 output.
Paper origin: references/ldt-paper/inductive_step.tex:135-143, applying
lem:orthonormalization-main-lemma to the complete polynomial measurements
whose full-polynomial consistency has just been proved.
This is the right-register counterpart of
sourceRoleRegisterLeftProjectiveSubmeasurement_ofFullConsistency. It
constructs the Bob-side projective submeasurement from the complete measurement
G_B and the cross-consistency relation with G_A, without assuming
permutation-invariance or identifying the two local Hilbert spaces.