Section 9 self-improvement statements #
This file records the SDP, addInU, and orthonormalization interfaces used in
the current formalization of the self-improvement theorem.
References #
blueprint/src/chapter/ch07_self_improvement.texreferences/ldt-paper/self_improvement.tex
Operators and conclusions #
Lean-only reduced SDP data for the currently formalized fragment of the self-improvement argument.
Paper-gap note: docs/paper-gaps/issue-1230-self-improvement-sdp-usage.tex.
The paper's lem:sdp eventually supplies strong duality, complementary
slackness, and a concrete matrix-level optimal witness. The current Lean
development only consumes the weaker facts recorded here: the primal witness is
a full measurement (T.total = 1), and the dual witness dominates every
averaged point operator. Positivity of the dual witness is derivable from dual
feasibility and positivity of the averaged point operators. Despite the
historical name, this reduced record does not assert SDP optimality.
Instances For
The dual operator in an SDP witness is positive semidefinite.
SDP optimal-pair data strengthened by complementary slackness.
Paper origin: references/ldt-paper/self_improvement.tex:82-181
(\label{lem:sdp}); paper-gap note:
docs/paper-gaps/issue-1230-self-improvement-sdp-usage.tex.
The reduced SdpOptimalPair interface above contains only the feasibility and
normalization facts already produced by the current Lean theorem for lem:sdp.
The paper's strong-duality argument also gives complementary slackness. This
successor interface records that additional conclusion without claiming that
the reduced theorem has already proved it.
- toSdpOptimalPair : SdpOptimalPair params strategy T Z
- complementarySlackness (g : Polynomial params) : sdpComplementarySlacknessEquation params strategy T Z g
Instances For
Paper origin: references/ldt-paper/self_improvement.tex:82-181
(\label{lem:sdp}); the complementary-slackness equation T_g · Z = T_g · A_g
is eq:complementary-slackness at line 179.
SDP conclusion strengthened by complementary slackness.
Paper origin: references/ldt-paper/self_improvement.tex lines 62--88
introduce the Section 9 primal/dual SDP pair and state \label{lem:sdp}:
there is an optimal pair {T_g}, Z with ∑ g, T_g = I and
T_g Z = T_g A_g for every polynomial g. Lines 168--190 then invoke
Slater's condition, strong duality, and complementary slackness to derive these
same measurement-total and slackness conclusions from the canonical SDP.
This is the statement shape expected from that paper argument: it records the complete primal measurement, the dual-feasible operator, and the complementary-slackness equations.
- witness : ∃ (T : Measurement (Polynomial params) ι) (Z : Quantum.Op ι), SdpOptimalPairWithSlackness params strategy T.toSubMeas Z
Instances For
The primal total of a slackness-carrying SDP pair is the identity.
The dual operator in a slackness-carrying SDP pair is positive semidefinite.
The dual slack operators in a slackness-carrying SDP pair are positive semidefinite.
The primal submeasurement in a slackness-carrying SDP pair is a measurement.
Equations
- h.primalMeasurement = { toSubMeas := T, total_eq_one := ⋯ }
Instances For
A slackness-carrying SDP statement gives the displayed paper-form measurement and dual witness.
This is the abstract analogue of the matrix-level witness extractors: the existential SDP statement contains a complete primal measurement, a positive dual operator dominating every averaged point operator, and the complementary-slackness equations.
The operator inside the left-hand side of lem:add-in-u at a fixed point u.
Returns a bipartite operator (M u).outcome o ⊗ H.outcome h.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The operator inside the right-hand side of lem:add-in-u at a fixed point u.
Returns a bipartite operator (Au * (M u).outcome o * Au) ⊗ T.outcome h.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The left-hand expectation in lem:add-in-u.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The right-hand expectation in lem:add-in-u.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The pointwise matched operator Σ_a A^u_a ⊗ H_[h(u)=a]
on the bipartite space ι × ι.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The average operator E_u Σ_a A^u_a ⊗ H_[h(u)=a]
on the bipartite space ι × ι.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The helper-stage upper operator Z ⊗ I
on the bipartite space ι × ι.
Equations
Instances For
The operator measuring the helper-stage boundedness defect
on the bipartite space ι × ι.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The helper-stage boundedness defect.
Equations
- MIPStarRE.LDT.SelfImprovement.helperBoundednessGap params strategy H Z = MIPStarRE.LDT.ev strategy.state (MIPStarRE.LDT.SelfImprovement.helperBoundednessOperator params strategy H Z)
Instances For
The projective-stage residual operator Z ⊗ (I - H)
on the bipartite space ι × ι.
Equations
Instances For
The projective-stage boundedness defect.
Equations
- MIPStarRE.LDT.SelfImprovement.projectiveBoundednessGap params strategy H Z = MIPStarRE.LDT.ev strategy.state (MIPStarRE.LDT.SelfImprovement.projectiveResidualOperator params H Z)
Instances For
Paper origin: references/ldt-paper/self_improvement.tex:238-455
(\label{lem:add-in-u}).
Reduced conclusion for the currently formalized fragment of lem:add-in-u.
The paper statement quantifies over an auxiliary submeasurement M, the
averaged family H, and a selection rule S, and proves a transfer inequality
between two expectations. The current Lean development only uses the downstream
global-variance corollary, which depends only on the SDP measurement T and
the error parameters, so those unused inputs are omitted here.
- varianceBound : GlobalVariance.pointConditionedGlobalVariance params strategy T.toSubMeas ≤ selfImprovementVarianceError params eps delta
Instances For
Paper origin: references/ldt-paper/self_improvement.tex:24-60
(\label{lem:self-improvement-helper});
docs/paper-gaps/issue-1230-self-improvement-sdp-usage.tex (SDP gap).
Reduced conclusion for the SDP and addInU stage of
lem:self-improvement-helper.
This structure intentionally records only the guarantees produced directly by
the current slackness-carrying SDP route and the addInU argument: the SDP
witness, the averaged construction of H, and the reduced addInU variance
bound. Positivity and pointwise dual feasibility of Z are read from the
bundled SDP witness rather than repeated as helper fields.
The paper and blueprint state four additional helper-lemma guarantees
(completeness, pointConsistency, strong self-consistency, and boundedness).
Those do not yet come from these arguments alone, so they are not fields here;
they should be proved as separate estimates that consume this SDP-witness
conclusion together with the paper hypotheses.
- sdpWitness : SdpOptimalPair params strategy T.toSubMeas Z
- addInUVarianceBound : AddInUStatement params strategy T eps delta
Instances For
Paper origin: references/ldt-paper/self_improvement.tex:24-60
(\label{lem:self-improvement-helper}).
Output of the self-improvement helper lemma before rounding to projectors. The
submeasurement H satisfies the four conclusions stated in the paper:
completeness, consistency with the point measurement, strong self-consistency,
and boundedness by a positive semidefinite dual witness Z. The boundedness
conclusion is represented by the positivity of Z, the pointwise domination
inequality Z ≥ E_u A^u_{g(u)}, and the corresponding state-dependent gap
estimate.
- completeness : CompletenessAtLeast strategy.state H.liftLeft (1 - nu - selfImprovementHelperError params eps delta)
- pointConsistency : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H) (selfImprovementHelperError params eps delta)
- strongSelfConsistency : BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily H) (selfImprovementHelperError params eps delta)
- boundednessGap : helperBoundednessGap params strategy H Z ≤ selfImprovementHelperError params eps delta
Instances For
Internal helper conclusion strengthened by the SDP complementary-slackness equation.
Paper origin: references/ldt-paper/self_improvement.tex:82-181
(\label{lem:sdp}) and references/ldt-paper/self_improvement.tex:635-671
(\label{thm:self-improvement}); paper-gap note:
docs/paper-gaps/issue-1230-self-improvement-sdp-usage.tex.
This is not an additional source-theorem hypothesis. It is the internal
helper-output record produced after the SDP theorem
sdp_statement_with_slackness supplies strong duality. It keeps all fields of
the reduced helper conclusion and additionally records the consequence
T_g Z = T_g A_g.
- toHelperConclusion : SelfImprovementHelperConclusion params strategy T H Z eps delta
- complementarySlackness (g : Polynomial params) : sdpComplementarySlacknessEquation params strategy T.toSubMeas Z g
Instances For
Paper origin: references/ldt-paper/self_improvement.tex:635-671
(\label{thm:self-improvement}).
Conclusion of thm:self-improvement.
The paper's boundedness output is the projective residual estimate
⟨ψ, Z ⊗ (I - H)⟩ ≤ ζ, recorded here as projectiveResidualBound. This
structure is the conjunction of the paper's displayed conclusions for the
already-quantified witnesses H and Z; it does not store an internal helper
form or an SDP connection input.
- completeness : CompletenessAtLeast strategy.state H.liftLeft (1 - nu - selfImprovementError params eps delta)
- pointConsistency : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (selfImprovementError params eps delta)
- selfCloseness : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas H.toSubMeas)) (selfImprovementError params eps delta)
- projectiveResidualBound : projectiveBoundednessGap params strategy H Z ≤ selfImprovementError params eps delta
Instances For
Final fields for the Section 9 transport stage.
The final fields are the Section 9 outputs that remain after combining:
SelfImprovementHelper, orthonormalization, data-processing, and the
monotone-total transport used in the projective-output step.
This record contains completeness, point-consistency, self-closeness, and the
projective-residual estimate. This projective residual is already the
paper-facing boundedness quantity carried into SelfImprovementConclusion.
- completeness : CompletenessAtLeast strategy.state H.liftLeft (1 - nu - selfImprovementError params eps delta)
- pointConsistency : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (selfImprovementError params eps delta)
- selfCloseness : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas H.toSubMeas)) (selfImprovementError params eps delta)
- projectiveResidualBound : projectiveBoundednessGap params strategy H Z ≤ selfImprovementError params eps delta