Helper completeness: the linearized SDP expression

The rewrite of the linearized helper-completeness expression as the dual mass, and the assembly of the Cauchy--Schwarz estimates with input consistency, the algebraic bridge from the two analytic moves to the Hhat-versus-Z lower bound: the counterpart of the vendored SelfImprovement/Theorems/Results/HelperCompleteness/Linearized.lean (under MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10, section "Port conventions").

A strategy is a SymStrat params 𝔓 K; T, Hhat and Z are local, in 𝔓, and the joint operators are strategy.state.L, strategy.state.R and strategy.state.opTensor in K →L[ℂ] K. The vendored Hhat.liftLeft is Hhat.liftLeft strategy.state, and subMeasMass/CompletenessAtLeast are those of the state.

• helper_first_move_abs_sub_bracketed_le_two_sqrt_delta passes hssc to M3's twoNotionsOfSelfConsistency, whose vendored hypothesis PermInvState ψ ∧ BipartiteSSCRel … is now BipartiteSSCRel alone, and calls closenessOfInnerProduct_right on strategy.state.toVecState without the vendored strategy.isNormalized. The vendored Matrix.PosSemidef self-adjointness of the fiber operator is IsSelfAdjoint.of_nonneg, and the adjoint computations are map_star strategy.state.L with the keystone's leftTensor_mul_leftTensor and rightTensor_mul_leftTensor_eq_opTensor.
• The averaging step of helper_linearized_completeness_eq_dual_mass_of_complementary_slackness is the keystone's ev_leftTensor_averageOperatorOverDistribution with Finset.mul_sum, in place of the vendored ev_opTensor_averageOperatorOverDistribution_left at B = 1 and Matrix.mul_sum.

The vendored file has no swap or density hypotheses.

Not ported

Every declaration of the vendored file has a counterpart here.

References

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

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

theorem MIPRE.LIDT.Co.SelfImprovement.helper_linearized_completeness_eq_dual_mass_of_complementary_slackness {𝔓 : 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 : 𝔓) (hTtotal : T.total = 1) (hslack : ∀ (h : MIPStarRE.LDT.Polynomial params), T.outcome h * averagedPointOperator params strategy h = T.outcome h * Z) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) fun (u : MIPStarRE.LDT.Point params) => ∑ h : MIPStarRE.LDT.Polynomial params, strategy.state.ev (strategy.state.L (T.outcome h * GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h u))) = strategy.state.ev (strategy.state.L Z)

The final algebraic rewrite in the helper-completeness Cauchy--Schwarz argument, isolated from the two analytic estimates.

After the two Cauchy--Schwarz moves in references/ldt-paper/self_improvement.tex, lines 360--399, the remaining linear expression is

E_u Σ_h ⟨ψ, (T_h A^u_{h(u)}) ⊗ I ψ⟩.

This theorem reindexes the average to Σ_h ⟨ψ, (T_h E_u A^u_{h(u)}) ⊗ I ψ⟩, applies the complementary-slackness identity T_h E_u A^u_{h(u)} = T_h Z, and finally invokes sdp_complementary_slackness_sum_eq_dual_mass to use Σ_h T_h = I. The statement deliberately keeps complementary slackness as an explicit hypothesis; it is not a consequence of the reduced SdpOptimalPair interface.

theorem MIPRE.LIDT.Co.SelfImprovement.helper_linearized_completeness_quantity_eq_dual_mass_of_complementary_slackness {𝔓 : 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 : 𝔓) (hTtotal : T.total = 1) (hslack : ∀ (h : MIPStarRE.LDT.Polynomial params), T.outcome h * averagedPointOperator params strategy h = T.outcome h * Z) : helperLinearizedCompletenessQuantity params strategy T = strategy.state.ev (strategy.state.L Z)

The named linearized helper-completeness quantity is the SDP dual mass under complementary slackness.

theorem MIPRE.LIDT.Co.SelfImprovement.helper_sdp_complementary_slackness_sum_eq_dual_mass {𝔓 : 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) (eps delta : ℝ) {T : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓} {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (hhelper : SelfImprovementHelperConclusion params strategy T Hhat Z eps delta) (hcomp : ∀ (h : MIPStarRE.LDT.Polynomial params), sdpComplementarySlacknessEquation params strategy T.toSubMeas Z h) : ∑ h : MIPStarRE.LDT.Polynomial params, strategy.state.ev (strategy.state.L (T.outcome h * averagedPointOperator params strategy h)) = strategy.state.ev (strategy.state.L Z)

Complementary-slackness conversion specialized to the SDP witness packaged inside SelfImprovementHelperConclusion.

noncomputable def MIPRE.LIDT.Co.SelfImprovement.helperBracketedCompletenessQuantity {𝔓 : 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) 𝔓) : ℝ

The bracketed scalar expression before the first Cauchy--Schwarz move in helper completeness.

This is the right-hand side of eq:bracketize-the-expression:

E_u Σ_a ⟨ψ, (A^u_a · T_[h(u)=a] · A^u_a) ⊗ I ψ⟩.

The finite sum Σ_{h : h(u)=a} T_h represents the paper's fiber operator T_[h(u)=a].

Equations

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

theorem MIPRE.LIDT.Co.SelfImprovement.helper_first_move_abs_sub_bracketed_le_two_sqrt_delta {𝔓 : 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) 𝔓) (delta : ℝ) (hssc : strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas delta) : |helperFirstMovedCompletenessQuantity params strategy T - helperBracketedCompletenessQuantity params strategy T| ≤ 2 * √delta

The first Cauchy--Schwarz move in the helper-completeness proof.

Assuming bipartite strong self-consistency of the point measurement with error delta, the bracketed expression E_u Σ_a ⟨ψ, (A^u_a T_[h(u)=a] A^u_a) ⊗ I ψ⟩ differs from E_u Σ_a ⟨ψ, (T_[h(u)=a] A^u_a) ⊗ A^u_a ψ⟩ by at most 2 sqrt delta. The proof is the paper's eq:yet-another-move-a: twoNotionsOfSelfConsistency supplies the first square-root factor, while helper_first_move_second_factor_operator_le_one supplies the second.

theorem MIPRE.LIDT.Co.SelfImprovement.helper_hhat_vs_z_of_cauchy_schwarz_and_complementary_slackness {𝔓 : 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) (eps delta : ℝ) {T : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓} {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (hhelper : SelfImprovementHelperConclusion params strategy T Hhat Z eps delta) (hmove_left : |helperFirstMovedCompletenessQuantity params strategy T.toSubMeas - strategy.state.subMeasMass (SubMeas.liftLeft strategy.state Hhat)| ≤ 2 * √delta) (hremove_right : |helperLinearizedCompletenessQuantity params strategy T.toSubMeas - helperFirstMovedCompletenessQuantity params strategy T.toSubMeas| ≤ √delta) (hslack : ∀ (h : MIPStarRE.LDT.Polynomial params), T.outcome h * averagedPointOperator params strategy h = T.outcome h * Z) : strategy.state.ev (strategy.state.L Z) - 3 * √delta ≤ strategy.state.subMeasMass (SubMeas.liftLeft strategy.state Hhat)

The recorded Hhat-versus-Z comparison follows from the two Cauchy--Schwarz scalar bounds and complementary slackness.

The first hypothesis is the bound for moving the leftmost copy of A^u_a across the bipartition; the second is the bound for removing the remaining copy of A^u_a on the right register. Together with complementary slackness, these are precisely the estimates leading to eq:gonna-use-this-later-H-versus-Z in the paper.

theorem MIPRE.LIDT.Co.SelfImprovement.helper_completeness_of_dual_mass_lower_bound {𝔓 : 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) (eps delta nu : ℝ) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (hHhat_vs_Z : strategy.state.ev (strategy.state.L Z) - 3 * √delta ≤ strategy.state.subMeasMass (SubMeas.liftLeft strategy.state Hhat)) (hdualMass : 1 - nu ≤ strategy.state.ev (strategy.state.L Z)) : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state Hhat) (1 - nu - MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta)

Helper-stage completeness from the Hhat-versus-Z comparison and the dual-mass lower bound.

The paper proves subMeasMass ψ Hhat.liftLeft ≥ ⟨ψ, Z ⊗ I, ψ⟩ - 3 √δ by the two Cauchy--Schwarz moves in the helper-completeness paragraph. Once the separate input-consistency argument gives 1 - ν ≤ ⟨ψ, Z ⊗ I, ψ⟩, this theorem performs the scalar assembly and absorbs the loss 3 √δ into the helper threshold ζ̂ = selfImprovementHelperError params eps delta.

theorem MIPRE.LIDT.Co.SelfImprovement.helper_completeness_of_input_consistency {𝔓 : 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) 𝔓) (eps delta nu : ℝ) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) {T : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓} {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (hhelper : SelfImprovementHelperConclusion params strategy T Hhat Z eps delta) (hHhat_vs_Z : strategy.state.ev (strategy.state.L Z) - 3 * √delta ≤ strategy.state.subMeasMass (SubMeas.liftLeft strategy.state Hhat)) (hcons : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) nu) : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state Hhat) (1 - nu - MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta)

Helper-stage completeness from input consistency and the Hhat-versus-Z comparison.

This is the checked assembly of the final part of the helper-completeness paragraph in thm:self-improvement. The only analytic input still external is the paper's Cauchy--Schwarz comparison subMeasMass ψ Hhat.liftLeft ≥ ⟨ψ, Z ⊗ I, ψ⟩ - 3 √δ; the SDP dual-feasibility fields of SelfImprovementHelperConclusion and the input consistency of G produce the dual-mass lower bound internally.

theorem MIPRE.LIDT.Co.SelfImprovement.helper_completeness_of_cauchy_schwarz_input_consistency {𝔓 : 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) 𝔓) (eps delta nu : ℝ) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) {T : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓} {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (hhelper : SelfImprovementHelperConclusion params strategy T Hhat Z eps delta) (hmove_left : |helperFirstMovedCompletenessQuantity params strategy T.toSubMeas - strategy.state.subMeasMass (SubMeas.liftLeft strategy.state Hhat)| ≤ 2 * √delta) (hremove_right : |helperLinearizedCompletenessQuantity params strategy T.toSubMeas - helperFirstMovedCompletenessQuantity params strategy T.toSubMeas| ≤ √delta) (hslack : ∀ (h : MIPStarRE.LDT.Polynomial params), T.outcome h * averagedPointOperator params strategy h = T.outcome h * Z) (hcons : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) nu) : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state Hhat) (1 - nu - MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta)

Helper-stage completeness from the two Cauchy--Schwarz scalar bounds, complementary slackness, and input consistency.

This theorem is the completeness paragraph with the Hhat-versus-Z comparison assembled internally from its two analytic estimates and the exact SDP rewrite. The remaining external hypotheses are therefore the two Cauchy--Schwarz estimates themselves and the complementary-slackness equation.