Self-improvement theorem variants #
The main selfImprovementHelper and the selfImprovement theorem corresponding
to thm:self-improvement in the blueprint.
Contents #
- selfImprovementHelper —
lem:self-improvement-helper, with the paper's input consistency hypothesis and four helper conclusions. - self_improvement_helper_with_slackness — companion helper producing the slackness-carrying helper conclusion from the Section 9 SDP statement.
- selfImprovement — the statement corresponding to
thm:self-improvement.
References #
references/ldt-paper/self_improvement.texblueprint/src/chapter/ch07_self_improvement.tex
Conditional form of the helper lemma from a slackness-carrying SDP conclusion.
This is the companion to selfImprovementHelper when the Section 9
strong-duality conclusion has already been supplied as
SdpStatementWithSlackness. The helper output therefore carries the
complementary-slackness equations needed by the helper-completeness chain.
Helper lemma driven by the Section 9 SDP statement with complementary slackness.
This applies the Section 9 statement sdp_statement_with_slackness, which
records the strong-duality conclusion with complementary slackness.
Paper origin: references/ldt-paper/self_improvement.tex:24-60
(\label{lem:self-improvement-helper}).
Self-improvement helper lemma for a polynomial measurement G consistent with
the point measurement. It produces a polynomial submeasurement H and a
positive semidefinite witness Z satisfying the four conclusions of the paper:
completeness, consistency with A, strong self-consistency, and boundedness.
The boundedness conclusion is split into positivity of Z, pointwise domination
of the averaged point measurement, and the state-dependent gap estimate. The
strong-self-consistency branch is proved in this file and is not exposed as an
additional public hypothesis.
Internal large-error fallback for selfImprovement.
When the literal threshold selfImprovementError is at least 1, the paper
conclusion is trivial: take the zero projective submeasurement and the identity
dual witness.
Formal statement corresponding to the blueprint theorem thm:self-improvement,
with the input consistency hypothesis from the LDT paper.
The theorem assumes a measurement G whose polynomial evaluation family is
consistent with the point measurement at error nu. It must produce a
projective polynomial submeasurement satisfying the four self-improvement
conclusions. The paper and blueprint impose the (eps, delta, gamma)-good
strategy condition as a standing hypothesis for the self-improvement section
(blueprint/src/chapter/ch07_self_improvement.tex, line 4); Lean records it
here as the explicit hypothesis hgood. The source-facing theorem remains
visible with the paper statement; the intermediate estimates are assembled by
named internal construction lemmas rather than hidden in a conditional theorem
with extra hypotheses.
Self-improvement only uses the axis-parallel and point self-consistency parts of the good-strategy hypothesis.
Paper origin: references/ldt-paper/self_improvement.tex:24-60 and
references/ldt-paper/self_improvement.tex:631-811.
The displayed Section 9 construction is written in terms of the point
measurement (A^u), the input polynomial measurement (G), and the scalar
bounds eps and delta; the diagonal-line error parameter gamma is part of
the paper's standing good-strategy context but does not occur in
selfImprovementError or in SelfImprovementConclusion. This wrapper makes
that independence explicit: it supplies the diagonal component of IsGood by
taking the actual diagonal failure as the auxiliary parameter, applies the
source theorem, and then reindexes the conclusion at the caller's gamma.