Helper completeness: the linearized SDP expression

This file rewrites the linearized helper-completeness expression as the dual mass and assembles the Cauchy--Schwarz estimates with input consistency. The statements here are the algebraic bridge from the two analytic moves to the Hhat-versus-Z lower bound.

References

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

theorem MIPStarRE.LDT.SelfImprovement.helper_linearized_completeness_eq_dual_mass_of_complementary_slackness {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (Z : Quantum.Op ι) (hTtotal : T.total = 1) (hslack : ∀ (h : Polynomial params), T.outcome h * averagedPointOperator params strategy h = T.outcome h * Z) : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => ∑ h : Polynomial params, ev strategy.state (leftTensor (T.outcome h * GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy h u))) = ev strategy.state (leftTensor 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 current reduced SdpOptimalPair interface.

theorem MIPStarRE.LDT.SelfImprovement.helper_linearized_completeness_quantity_eq_dual_mass_of_complementary_slackness {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (Z : Quantum.Op ι) (hTtotal : T.total = 1) (hslack : ∀ (h : Polynomial params), T.outcome h * averagedPointOperator params strategy h = T.outcome h * Z) : helperLinearizedCompletenessQuantity params strategy T = ev strategy.state (leftTensor Z)

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

theorem MIPStarRE.LDT.SelfImprovement.helper_sdp_complementary_slackness_sum_eq_dual_mass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) {T : Measurement (Polynomial params) ι} {Hhat : SubMeas (Polynomial params) ι} {Z : Quantum.Op ι} (hhelper : SelfImprovementHelperConclusion params strategy T Hhat Z eps delta) (hcomp : ∀ (h : Polynomial params), sdpComplementarySlacknessEquation params strategy T.toSubMeas Z h) : ∑ h : Polynomial params, ev strategy.state (leftTensor (T.outcome h * averagedPointOperator params strategy h)) = ev strategy.state (leftTensor Z)

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

noncomputable def MIPStarRE.LDT.SelfImprovement.helperBracketedCompletenessQuantity {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) : Error

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 MIPStarRE.LDT.SelfImprovement.helper_first_move_abs_sub_bracketed_le_two_sqrt_delta {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (T : SubMeas (Polynomial params) ι) (delta : Error) (hssc : BipartiteSSCRel strategy.state (uniformDistribution (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_le_one supplies the second.

theorem MIPStarRE.LDT.SelfImprovement.helper_hhat_vs_z_of_cauchy_schwarz_and_complementary_slackness {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) {T : Measurement (Polynomial params) ι} {Hhat : SubMeas (Polynomial params) ι} {Z : Quantum.Op ι} (hhelper : SelfImprovementHelperConclusion params strategy T Hhat Z eps delta) (hmove_left : |helperFirstMovedCompletenessQuantity params strategy T.toSubMeas - subMeasMass strategy.state Hhat.liftLeft| ≤ 2 * √delta) (hremove_right : |helperLinearizedCompletenessQuantity params strategy T.toSubMeas - helperFirstMovedCompletenessQuantity params strategy T.toSubMeas| ≤ √delta) (hslack : ∀ (h : Polynomial params), T.outcome h * averagedPointOperator params strategy h = T.outcome h * Z) : ev strategy.state (leftTensor Z) - 3 * √delta ≤ subMeasMass strategy.state Hhat.liftLeft

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 MIPStarRE.LDT.SelfImprovement.helper_completeness_of_dual_mass_lower_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta nu : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) {Hhat : SubMeas (Polynomial params) ι} {Z : Quantum.Op ι} (hHhat_vs_Z : ev strategy.state (leftTensor Z) - 3 * √delta ≤ subMeasMass strategy.state Hhat.liftLeft) (hdualMass : 1 - nu ≤ ev strategy.state (leftTensor Z)) : CompletenessAtLeast strategy.state Hhat.liftLeft (1 - nu - 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 MIPStarRE.LDT.SelfImprovement.helper_completeness_of_input_consistency {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : Measurement (Polynomial params) ι) (eps delta nu : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) {T : Measurement (Polynomial params) ι} {Hhat : SubMeas (Polynomial params) ι} {Z : Quantum.Op ι} (hhelper : SelfImprovementHelperConclusion params strategy T Hhat Z eps delta) (hHhat_vs_Z : ev strategy.state (leftTensor Z) - 3 * √delta ≤ subMeasMass strategy.state Hhat.liftLeft) (hcons : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) nu) : CompletenessAtLeast strategy.state Hhat.liftLeft (1 - nu - 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 MIPStarRE.LDT.SelfImprovement.helper_completeness_of_cauchy_schwarz_input_consistency {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : Measurement (Polynomial params) ι) (eps delta nu : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) {T : Measurement (Polynomial params) ι} {Hhat : SubMeas (Polynomial params) ι} {Z : Quantum.Op ι} (hhelper : SelfImprovementHelperConclusion params strategy T Hhat Z eps delta) (hmove_left : |helperFirstMovedCompletenessQuantity params strategy T.toSubMeas - subMeasMass strategy.state Hhat.liftLeft| ≤ 2 * √delta) (hremove_right : |helperLinearizedCompletenessQuantity params strategy T.toSubMeas - helperFirstMovedCompletenessQuantity params strategy T.toSubMeas| ≤ √delta) (hslack : ∀ (h : Polynomial params), T.outcome h * averagedPointOperator params strategy h = T.outcome h * Z) (hcons : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) nu) : CompletenessAtLeast strategy.state Hhat.liftLeft (1 - nu - 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.