Section 12 pasting: final pasting theorems #
Final completeness and pasting theorems.
Internal form of cor:ld-pasting-N-completeness from the two preceding
mass-comparison inputs.
This theorem isolates the scalar assembly after lem:over-all-outcomes,
lem:from-H-to-G, and the Bernoulli-tail lower bound have already been
established.
cor:ld-pasting-N-completeness once the Bernoulli-tail lower bound is
supplied explicitly.
This records the downstream scalar algebra after lem:over-all-outcomes and
lem:from-H-to-G. The hypothesis htail is exactly the θ = 1 / (200m)
specialization of lem:chernoff-bernoulli-matrix for the averaged complete
operator G = \mathbb E_x \sum_g G^x_g, expressed as the concrete
fromHToGBernoulliTailMass lower bound with error
κ · (1 + 1/(100m)) + exp(-k / (80000 m²)).
cor:ld-pasting-N-completeness.
Internal form of cor:ld-pasting-N-completeness from the Section 11
commutativity conclusion.
lem:ld-pasting-sub-measurement.
Restricted nontrivial-regime Lean form of thm:ld-pasting.
The source theorem is references/ldt-paper/ld-pasting.tex, lines 12--50.
Lines 52--55 explain that the proof may assume the nontrivial regime
eps, delta, gamma, zeta, d / q ≤ 1, since the complementary cases are
trivial. This declaration states the restricted assumptions
gamma ≤ 1, zeta ≤ 1, params.d ≤ params.q, 0 < params.d, and 1 ≤ k.
The unrestricted statement aligned with the paper is ldPasting; the
degree-zero complementary branch is handled separately by
ldPastingDegreeZeroBranch.
Trivial consistency conclusion when the target pasting error is at least 1.
The consistency defect of two submeasurements against a normalized bipartite
state is always at most 1; hence a scalar lower bound
1 ≤ ldPastingInInductionError ... is enough to produce the final conclusion
with a distinguished trivial measurement.
Trivial consistency conclusion from the complementary scalar branches.
If k is positive, it suffices to show that the ν term in the pasting error
is at least 1; if k = 0, the exponential term already gives the trivial
bound.
Complementary branch for thm:ld-pasting when gamma > 1.
Paper origin: references/ldt-paper/ld-pasting.tex:52-55, where this is one
of the large-error cases in which the final consistency bound is trivial.
This is one of the proved complementary cases for thm:ld-pasting.
Complementary branch for thm:ld-pasting when zeta > 1.
Paper origin: references/ldt-paper/ld-pasting.tex:52-55, where this is one
of the large-error cases in which the final consistency bound is trivial.
This is one of the proved complementary cases for thm:ld-pasting.
Complementary branch for thm:ld-pasting when d > q.
Paper origin: references/ldt-paper/ld-pasting.tex:52-55, where this is the
large-error case (d/q) ≥ 1. This is one of the proved complementary cases
for thm:ld-pasting.
Complementary branch for thm:ld-pasting when k = 0.
This branch is a boundary case for the reduction to the nontrivial theorem,
whose proof assumes 1 ≤ k. The scalar calculation showing that the
exponential term gives the trivial bound is proved in ScalarBounds.lean.
Degree-zero complementary branch for the unrestricted source theorem.
Paper origin: references/ldt-paper/ld-pasting.tex:12-55. The paper's
large-error reduction names the cases
eps, delta, gamma, zeta, d/q ≥ 1; it does not explicitly add 0 < d as a
hypothesis of thm:ld-pasting. Thus the Lean theorem should not add 0 < d
as an assumption of that cited theorem.
Issue #1622 recorded the need for a direct proof of this degree-zero branch; see
docs/paper-gaps/issue-1622-ld-pasting-degree-zero.tex. The existing
nontrivial argument cannot simply be reused: its hBConsistency aggregation
passes from distinct sampled heights to independent sampled heights and absorbs
the resulting k^2/q loss through the displayed (d/q)^(1/32) term. When
d = 0, that term is zero, so the branch requires a separate argument rather
than an additional hypothesis on ldPasting.
Projection from the restricted nontrivial construction.
The restricted construction theorem ldPastingNontrivial proves the nontrivial
analytic regime for the canonical pasted measurement. This auxiliary statement
records the projection from the restricted construction theorem to the conclusion
needed by the unrestricted theorem, without changing the statement of
thm:ld-pasting.
Paper-aligned form of thm:ld-pasting.
Paper origin: references/ldt-paper/ld-pasting.tex, lines 12--50. The
following lines 52--55 explain that the proof may restrict to the regime
eps, delta, gamma, zeta, d / q ≤ 1, because the complementary cases are
trivial. The restricted theorem ldPastingNontrivial proves the nontrivial
regime, and the large-gamma, large-zeta, large-d / q, and k = 0
complementary branches are proved above, including the degree-zero case, so
this declaration keeps the unrestricted paper statement visible without adding
the non-paper assumptions from the restricted theorem. The former obstruction is documented in
docs/paper-gaps/issue-1622-ld-pasting-degree-zero.tex.