Main-formal soundness theorem #
This module contains the corrected two-space final theorem for
thm:main-formal. The theorem starts from a general projective strategy
ProjStrat params ιA ιB, applies the heterogeneous role-register route, and
absorbs the explicit intermediate errors into the final parameter
mainFormalError.
The public theorem uses the confirmed large-k correction k ≥ 400 m d and
the nonzero sampling condition 0 < k. These are documented in
docs/paper-gaps/issue-906-main-formal-k-bound.tex and
docs/paper-gaps/issue-422-main-formal-zero-k-boundary.tex.
References #
- Paper:
references/ldt-paper/test_definition.tex,thm:main-formalat line 180; its proof is inreferences/ldt-paper/inductive_step.tex(lines 26–236). - Blueprint:
blueprint/src/chapter/ch02_test.tex,\label{thm:main-formal}.
Two-space source route #
Trivial saturated-error branch for the printed two-space theorem
thm:main-formal.
Paper origin: references/ldt-paper/test_definition.tex:180-202.
Source: This is a source-faithful saturated-error branch: when the printed
target error is at least 1, the consistency conclusion follows from the
normalization bound for bipartite consistency defects, without adding any
construction hypothesis to the source theorem.
Whenever mainFormalError params k eps ≥ 1, the three consistency conclusions
hold for arbitrary projective polynomial measurements, since each underlying
consistency defect is bounded by 1 for a normalized bipartite state and a
uniform question distribution. The argument does not use the low individual
degree test hypothesis.
Source role-register conclusion after the scalar branch has supplied
0 < k.
This theorem is not an additional hypothesis of thm:main-formal; it isolates
the checked two-space role-register construction from the scalar absorption at
the corrected nonzero sampling boundary. The proof uses
ProjStrat.sourceRoleRegisterFinalPointConsistency and then weakens the three
explicit pre-absorption errors to mainFormalError by the existing Step 8
scalar cascade.
Small-error branch for the corrected two-space theorem
thm:main-formal.
Paper origin: references/ldt-paper/test_definition.tex:180-202.
This theorem records the small-error branch of the corrected source theorem.
It is not an additional hypothesis of thm:main-formal; the source-boundary
reduction below calls it only after the saturated-error branch has been
discharged by mainFormal_trivial_witness.
The heterogeneous role-register symmetrization, factor-two
unsymmetrization, point-agreement branch, heterogeneous triangle step,
Schwartz--Zippel Step 5 calculation, the step making measurements projective,
completion, line-169 transport, final point-evaluation triangle, and scalar absorption into
mainFormalError are checked in the two-space route once the nonzero
scalar-cascade boundary 0 < k is supplied. This nonzero boundary is the
correction recorded in
docs/paper-gaps/issue-422-main-formal-zero-k-boundary.tex.
Source-boundary reduction for the corrected two-space theorem
thm:main-formal.
Paper origin: references/ldt-paper/test_definition.tex:180-202.
This theorem closes the saturated-error branch of the source-boundary
argument. If mainFormalError params k eps ≥ 1, the conclusion follows from
mainFormal_trivial_witness; otherwise the proof is exactly the named
small-error branch mainFormal_smallErrorConclusion. This reduction
is not an additional hypothesis of thm:main-formal.
Corrected source statement of thm:main-formal.
Paper origin: references/ldt-paper/test_definition.tex:180-202.
This theorem records the two-space source theorem with the confirmed large-k
correction k ≥ 400 m d. The paper prints the weaker hypothesis k ≥ m d;
the missing factor 400 is documented in
docs/paper-gaps/issue-906-main-formal-k-bound.tex. The additional condition
0 < k corrects the zero-sampling boundary where the printed error collapses
to zero; this boundary is documented in
docs/paper-gaps/issue-422-main-formal-zero-k-boundary.tex.