Section 9 self-improvement statements

The SDP, addInU and orthonormalization interfaces of the self-improvement theorem: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/SelfImprovement/Theorems/Statements.lean in the port of planning/c6b-plan.md (milestone M10, section "Port conventions").

A strategy is a SymStrat params 𝔓 K. The SDP witnesses T : SubMeas (Polynomial params) 𝔓 and Z : 𝔓 are local, and every structure keeps the vendored fields verbatim. The addInU and helper-agreement operators are joint operators K →L[ℂ] K, built with strategy.state.opTensor, so the strategy argument of addInULeftOperatorAtPoint, unused in the vendored file (_strategy), is used here. The two operators that place without a strategy, helperUpperOperator and projectiveResidualOperator, take the model (S : SymModel 𝔓 K) as an explicit first argument, as M6's and M7's placement helpers do; helperBoundednessOperator, helperBoundednessGap and projectiveBoundednessGap pass strategy.state. The vendored placements leftPlacedSubMeas (ιB := ι) and rightPlacedSubMeas (ιA := ι) are strategy.state.leftPlacedSubMeas and strategy.state.rightPlacedSubMeas.

The summed semidefinite form

The vendored SdpStatementWithSlackness is supplied by the matrix SDP bridge (SelfImprovement/Theorems/Results/SdpMatrixBridge.lean, through the canonical block SDP of SelfImprovement/MatrixRealization), which the port does not have: there is no dimension. It is replaced by the summed form of M9, MIPRE.SummedSdp.IsSummedSdp, whose fields are those of SdpOptimalPairWithSlackness. SdpStatementWithSlackness.of_isSummedSdp is the interface half of that adapter: a summed form for the averaged point operators A_g = averagedPointOperator gives the SDP statement. SdpOptimalPairWithSlackness.isSummedSdp is its converse, with the self-adjointness of Z from dual_positive. The other half, the existence of a summed form in a finite pair, is sdp_statement_with_slackness in the ported HelperCompleteness/Bracketed.lean.

Not ported

Every declaration of the vendored file has a counterpart here.

New here

• SdpStatementWithSlackness.of_isSummedSdp: the summed form of M9 gives the SDP statement.
• SdpOptimalPairWithSlackness.isSummedSdp: its converse.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• blueprint/src/chapter/ch07_self_improvement.tex
• references/ldt-paper/self_improvement.tex

Operators and conclusions

structure MIPRE.LIDT.Co.SelfImprovement.SdpOptimalPair {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) : Prop

Lean-only reduced SDP data for the currently formalized fragment of the self-improvement argument.

Paper-gap note (upstream): docs/paper-gaps/issue-1230-self-improvement-sdp-usage.tex.

The paper's lem:sdp eventually supplies strong duality, complementary slackness, and an optimal witness. The 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.

• primalTotalOperator : T.total = 1

  The primal witness is complete.

• dualFeasible (g : MIPStarRE.LDT.Polynomial params) : 0 ≤ sdpDualSlackOperator params strategy Z g

  The dual witness dominates every averaged point operator.

theorem MIPRE.LIDT.Co.SelfImprovement.SdpOptimalPair.dualPositive {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params 𝔓 K} {T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (h : SdpOptimalPair params strategy T Z) : 0 ≤ Z

The dual operator in an SDP witness is positive.

structure MIPRE.LIDT.Co.SelfImprovement.SdpOptimalPairWithSlackness {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) : Prop

SDP optimal-pair data strengthened by complementary slackness.

Paper origin: references/ldt-paper/self_improvement.tex:82-181 (\label{lem:sdp}); paper-gap note (upstream): docs/paper-gaps/issue-1230-self-improvement-sdp-usage.tex.

The reduced SdpOptimalPair interface above contains only the feasibility and normalization facts. The paper's strong-duality argument also gives complementary slackness, which this successor interface records.

• toSdpOptimalPair : SdpOptimalPair params strategy T Z

  The reduced SDP data.

• complementarySlackness (g : MIPStarRE.LDT.Polynomial params) : sdpComplementarySlacknessEquation params strategy T Z g

  Complementary slackness, T_g Z = T_g A_g for every g.

structure MIPRE.LIDT.Co.SelfImprovement.SdpStatementWithSlackness {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) : Prop

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.

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. In the port it comes from the summed form of M9 (SdpStatementWithSlackness.of_isSummedSdp).

• witness : ∃ (T : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓), SdpOptimalPairWithSlackness params strategy T.toSubMeas Z

  A complete primal measurement and a dual witness with slackness.

theorem MIPRE.LIDT.Co.SelfImprovement.SdpOptimalPairWithSlackness.primal_total_operator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params 𝔓 K} {T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (h : SdpOptimalPairWithSlackness params strategy T Z) : T.total = 1

The primal total of a slackness-carrying SDP pair is the identity.

theorem MIPRE.LIDT.Co.SelfImprovement.SdpOptimalPairWithSlackness.dual_positive {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params 𝔓 K} {T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (h : SdpOptimalPairWithSlackness params strategy T Z) : 0 ≤ Z

The dual operator in a slackness-carrying SDP pair is positive.

theorem MIPRE.LIDT.Co.SelfImprovement.SdpOptimalPairWithSlackness.dual_feasible {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params 𝔓 K} {T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (h : SdpOptimalPairWithSlackness params strategy T Z) (g : MIPStarRE.LDT.Polynomial params) : 0 ≤ sdpDualSlackOperator params strategy Z g

The dual slack operators in a slackness-carrying SDP pair are positive.

def MIPRE.LIDT.Co.SelfImprovement.SdpOptimalPairWithSlackness.primalMeasurement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params 𝔓 K} {T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (h : SdpOptimalPairWithSlackness params strategy T Z) : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓

The primal submeasurement in a slackness-carrying SDP pair is a measurement.

Equations

• h.primalMeasurement = { toSubMeas := T, total_eq_one := ⋯ }

@[simp]

theorem MIPRE.LIDT.Co.SelfImprovement.SdpOptimalPairWithSlackness.primalMeasurement_toSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params 𝔓 K} {T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (h : SdpOptimalPairWithSlackness params strategy T Z) : h.primalMeasurement.toSubMeas = T

The primal measurement of a slackness-carrying SDP pair has the pair's submeasurement.

theorem MIPRE.LIDT.Co.SelfImprovement.SdpOptimalPairWithSlackness.isSummedSdp {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params 𝔓 K} {T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (h : SdpOptimalPairWithSlackness params strategy T Z) : SummedSdp.IsSummedSdp (averagedPointOperator params strategy) T.outcome Z

New here. A slackness-carrying SDP pair is the summed form of M9 (MIPRE.SummedSdp.IsSummedSdp) for the averaged point operators, the self-adjointness of Z coming from its positivity.

theorem MIPRE.LIDT.Co.SelfImprovement.SdpStatementWithSlackness.exists_measurement_witness {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params 𝔓 K} (h : SdpStatementWithSlackness params strategy) : ∃ (T : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓), 0 ≤ Z ∧ (∀ (g : MIPStarRE.LDT.Polynomial params), 0 ≤ sdpDualSlackOperator params strategy Z g) ∧ ∀ (g : MIPStarRE.LDT.Polynomial params), sdpComplementarySlacknessEquation params strategy T.toSubMeas Z g

A slackness-carrying SDP statement gives the displayed paper-form measurement and dual witness: a complete primal measurement, a positive dual operator dominating every averaged point operator, and the complementary-slackness equations.

theorem MIPRE.LIDT.Co.SelfImprovement.SdpStatementWithSlackness.of_isSummedSdp {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {params : MIPStarRE.LDT.Parameters} [MIPStarRE.LDT.FieldModel params.q] {strategy : SymStrat params 𝔓 K} {T : MIPStarRE.LDT.Polynomial params → 𝔓} {Z : 𝔓} (h : SummedSdp.IsSummedSdp (averagedPointOperator params strategy) T Z) : SdpStatementWithSlackness params strategy

New here. The interface half of the adapter from M9's summed semidefinite form: a summed form IsSummedSdp A T Z for the averaged point operators A_g = averagedPointOperator gives the SDP statement, with the measurement T and the dual witness Z.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.addInULeftOperatorAtPoint {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (M : IdxSubMeas (MIPStarRE.LDT.Point params) Outcome 𝔓) (H : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (S : MIPStarRE.LDT.SelfImprovement.AddInUSelection params Outcome) (u : MIPStarRE.LDT.Point params) : K →L[ℂ] K

The operator inside the left-hand side of lem:add-in-u at a fixed point u: the joint operator Σ_{(o, h) ∈ S u} (M u)_o ⊗ H_h.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.addInURightOperatorAtPoint {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (M : IdxSubMeas (MIPStarRE.LDT.Point params) Outcome 𝔓) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (S : MIPStarRE.LDT.SelfImprovement.AddInUSelection params Outcome) (u : MIPStarRE.LDT.Point params) : K →L[ℂ] K

The operator inside the right-hand side of lem:add-in-u at a fixed point u: the joint operator Σ_{(o, h) ∈ S u} (A^u_{h(u)} (M u)_o A^u_{h(u)}) ⊗ T_h.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.addInUPointAverage {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (f : MIPStarRE.LDT.Point params → K →L[ℂ] K) : ℝ

The uniform point average E_u ⟨ψ, f(u) ψ⟩ of a point-indexed joint operator.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.addInULeftQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (M : IdxSubMeas (MIPStarRE.LDT.Point params) Outcome 𝔓) (H : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (S : MIPStarRE.LDT.SelfImprovement.AddInUSelection params Outcome) : ℝ

The left-hand expectation in lem:add-in-u.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.addInURightQuantity {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (M : IdxSubMeas (MIPStarRE.LDT.Point params) Outcome 𝔓) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (S : MIPStarRE.LDT.SelfImprovement.AddInUSelection params Outcome) : ℝ

The right-hand expectation in lem:add-in-u.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperAgreementOperatorAtPoint {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (H : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (u : MIPStarRE.LDT.Point params) : K →L[ℂ] K

The pointwise matched operator Σ_a A^u_a ⊗ H_[h(u)=a], a joint operator.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperAgreementAverageOperator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (H : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : K →L[ℂ] K

The average operator E_u Σ_a A^u_a ⊗ H_[h(u)=a], a joint operator.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperUpperOperator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (_params : MIPStarRE.LDT.Parameters) (Z : 𝔓) : K →L[ℂ] K

The helper-stage upper operator Z ⊗ I, the left placement of Z in the model S.

Equations

• MIPRE.LIDT.Co.SelfImprovement.helperUpperOperator S _params Z = S.L Z

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperBoundednessOperator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (H : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) : K →L[ℂ] K

The operator measuring the helper-stage boundedness defect, a joint operator.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperBoundednessGap {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (H : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) : ℝ

The helper-stage boundedness defect.

Equations

• MIPRE.LIDT.Co.SelfImprovement.helperBoundednessGap params strategy H Z = strategy.state.ev (MIPRE.LIDT.Co.SelfImprovement.helperBoundednessOperator params strategy H Z)

noncomputable def MIPRE.LIDT.Co.SelfImprovement.projectiveResidualOperator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) : K →L[ℂ] K

The projective-stage residual operator Z ⊗ (I - H), placed in the model S.

Equations

• MIPRE.LIDT.Co.SelfImprovement.projectiveResidualOperator S params H Z = S.L Z * S.R (1 - H.total)

noncomputable def MIPRE.LIDT.Co.SelfImprovement.projectiveBoundednessGap {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) : ℝ

The projective-stage boundedness defect.

Equations

• MIPRE.LIDT.Co.SelfImprovement.projectiveBoundednessGap params strategy H Z = strategy.state.ev (MIPRE.LIDT.Co.SelfImprovement.projectiveResidualOperator strategy.state params H Z)

structure MIPRE.LIDT.Co.SelfImprovement.AddInUStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓) (eps delta : ℝ) : Prop

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 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 ≤ MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError params eps delta

  The point-conditioned global variance of T is small.

structure MIPRE.LIDT.Co.SelfImprovement.SelfImprovementHelperConclusion {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓) (H : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) (eps delta : ℝ) : Prop

Paper origin: references/ldt-paper/self_improvement.tex:24-60 (\label{lem:self-improvement-helper}); upstream 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: 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). They are not fields here; they are proved as separate estimates that consume this SDP-witness conclusion together with the paper hypotheses.

• sdpWitness : SdpOptimalPair params strategy T.toSubMeas Z

  The SDP witness.

• averagedConstruction : H = averagedSandwichedPolynomialSubMeas params strategy T.toSubMeas

  H is the averaged sandwiched submeasurement of T.

• addInUVarianceBound : AddInUStatement params strategy T eps delta

  The reduced addInU variance bound.

structure MIPRE.LIDT.Co.SelfImprovement.SelfImprovementHelperStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (H : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) (eps delta nu : ℝ) : Prop

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 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 : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state H) (1 - nu - MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta)

  H is almost complete.

• pointConsistency : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta)

  H is consistent with the point measurement.

• strongSelfConsistency : strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily H) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta)

  H is strongly self-consistent.

• positiveSemidefiniteWitness : 0 ≤ Z

  The dual witness is positive.

• dualDominatesAveragedPoint (g : MIPStarRE.LDT.Polynomial params) : 0 ≤ sdpDualSlackOperator params strategy Z g

  The dual witness dominates every averaged point operator.

• boundednessGap : helperBoundednessGap params strategy H Z ≤ MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta

  The helper-stage boundedness defect is small.

structure MIPRE.LIDT.Co.SelfImprovement.SelfImprovementHelperConclusionWithSlackness {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (T : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓) (H : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) (eps delta : ℝ) : Prop

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}); upstream 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 the slackness. 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

  The reduced helper conclusion.

• complementarySlackness (g : MIPStarRE.LDT.Polynomial params) : sdpComplementarySlacknessEquation params strategy T.toSubMeas Z g

  Complementary slackness, T_g Z = T_g A_g for every g.

structure MIPRE.LIDT.Co.SelfImprovement.SelfImprovementConclusion {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (G : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓) (H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) (eps delta gamma nu : ℝ) : Prop

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 : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state H.toSubMeas) (1 - nu - MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta)

  H is almost complete.

• pointConsistency : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta)

  H is consistent with the point measurement.

• selfCloseness : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (strategy.state.leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (strategy.state.rightPlacedSubMeas H.toSubMeas)) (MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta)

  The left and right placements of H are close.

• positiveSemidefiniteWitness : 0 ≤ Z

  The dual witness is positive.

• dualDominatesAveragedPoint (g : MIPStarRE.LDT.Polynomial params) : 0 ≤ sdpDualSlackOperator params strategy Z g

  The dual witness dominates every averaged point operator.

• projectiveResidualBound : projectiveBoundednessGap params strategy H Z ≤ MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta

  The projective residual ⟨ψ, Z ⊗ (I - H)⟩ is small.

structure MIPRE.LIDT.Co.SelfImprovement.SelfImprovementFinalFields {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) (eps delta nu : ℝ) : Prop

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: completeness, point consistency, self-closeness, and the projective-residual estimate, the paper-facing boundedness quantity carried into SelfImprovementConclusion.

• completeness : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state H.toSubMeas) (1 - nu - MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta)

  H is almost complete.

• pointConsistency : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta)

  H is consistent with the point measurement.

• selfCloseness : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (strategy.state.leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (strategy.state.rightPlacedSubMeas H.toSubMeas)) (MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta)

  The left and right placements of H are close.

• projectiveResidualBound : projectiveBoundednessGap params strategy H Z ≤ MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta

  The projective residual ⟨ψ, Z ⊗ (I - H)⟩ is small.