Off-diagonal residual estimates for the helper SSC argument #
This module names the off-diagonal scalar quantities appearing after the projector insertion in the helper strong-self-consistency proof, records their exact decompositions, and assembles the two variance-transport comparisons with the Schwartz--Zippel endpoint.
References #
references/ldt-paper/self_improvement.texlines 455--468blueprint/src/chapter/ch07_self_improvement.tex
Off-diagonal residual quantities for the helper SSC estimate #
The off-diagonal contribution after inserting the outer point projector
A^u_{h(u)} around the pointwise helper outcome H^u_{h'}.
This is the non-diagonal term added when the diagonal released expression is
enlarged to the full (h,h') sum in the proof of helper strong
self-consistency.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The same off-diagonal contribution after using eq:h-blt: the outer
projector has been removed from the operator and replaced by the polynomial
agreement indicator 1_{h(u)=h'(u)}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The intermediate off-diagonal expression after the first variance swap.
The left copy of the point projector has been evaluated at an independent point
v, while the right copy is still evaluated at the original point u. This is
the Lean scalar form of the expression in the paper immediately after
eq:swapped-u-for-v.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The post-variance-swap endpoint for the off-diagonal contribution.
Here both copies of the point projector have been evaluated at an independent
point v, while the agreement indicator has already been averaged over the
original point u. This is the scalar expression to which the
Schwartz--Zippel estimate is applied.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The full enlarged expression after inserting the outer point projector.
This includes both the diagonal and off-diagonal pairs (h,h'), and is the
right-hand side of eq:threw-in-h-prime before applying eq:h-blt.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The full inserted expression splits into its released diagonal part and its off-diagonal remainder.
This is the finite-sum identity underlying the passage from
eq:release-the-kraken to eq:threw-in-h-prime: for each fixed polynomial
h, the sum over all h' is the diagonal term h' = h plus the sum over
h' ≠ h.
The full enlarged expression after deleting the left copy of the point projector.
This is the paper's eq:delete-an-A scalar quantity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Formal version of the paper's eq:delete-an-A identity.
The delete-an-A expression after replacing the remaining point projector
by an independent point.
This is the scalar quantity on the right-hand side of the paper's
eq:swap-u-for-v-attack-of-the-clones.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The expression obtained after moving the remaining point projector to the right tensor factor.
This is the scalar quantity on the right-hand side of the paper's
eq:move-over-v.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Assemble the post-delete-an-A transport estimates.
The first hypothesis is the variance replacement
A^u_{h(u)} → A^v_{h(v)} in eq:swap-u-for-v-attack-of-the-clones. The second
hypothesis is the self-consistency move eq:move-over-v, which moves the
remaining point projector from Alice's tensor factor to Bob's tensor factor.
This lemma only performs the scalar triangle-inequality assembly; the analytic
proofs of the two displayed hypotheses remain separate.
The reverse scalar direction of the post-delete-an-A transport estimates.
This is the direction used when the final move-over-v expression is known to
be large and one transfers that lower bound back to the delete-an-A expression.
It is again only the triangle-inequality assembly of the two analytic transport
estimates.
Named form of the identity eq:h-blt for the off-diagonal helper SSC
quantity.
Named Schwartz--Zippel endpoint for the helper SSC off-diagonal term.
Assemble the two one-projector variance transports for the off-diagonal helper residual.
The first hypothesis is the estimate for replacing the left copy of
A^u_{h(u)} by A^v_{h(v)}. The second hypothesis is the estimate for
replacing the remaining right copy by the same independent point v. Together
they give the transport inequality used before the Schwartz--Zippel endpoint in
the proof of helper strong self-consistency.
Assemble the off-diagonal projector-insertion bound from the two variance swaps and the Schwartz--Zippel endpoint.
The hypothesis htransport is precisely the analytic content of the two
Cauchy--Schwarz variance moves in the proof of
item:self-improvement-self: it transports the indicator form of the
off-diagonal term to the endpoint with both point projectors evaluated at the
independent point v. The conclusion is the corresponding paper estimate
before substituting the concrete value of the transport error.
Paper-shaped form of the off-diagonal projector-insertion estimate.
Once the two variance swaps have supplied transport error
2√ζ_variance, the inserted off-diagonal contribution is bounded by
2√ζ_variance + md/q.
Paper-shaped off-diagonal bound from the two explicit variance transports.
This version exposes the two Cauchy--Schwarz/global-variance moves separately: first from the indicator form to the one-sided swapped expression, and then from the one-sided swapped expression to the Schwartz--Zippel endpoint.