Helper completeness: input consistency and the SDP bridge

This file contains the part of the helper-completeness argument which relates input consistency, SDP dual feasibility, and complementary slackness. These lemmas correspond to the lower-bound calculation at the end of the completeness proof in references/ldt-paper/self_improvement.tex, lines 406--414.

References

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

theorem MIPStarRE.LDT.SelfImprovement.input_consistency_match_mass_lower_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : Measurement (Polynomial params) ι) (nu : Error) (hcons : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) nu) : 1 - nu ≤ avgOver (uniformDistribution (Point params)) fun (u : Point params) => qBipartiteMatchMass strategy.state (strategy.pointMeasurement.toIdxSubMeas u) (polynomialEvaluationFamily params G.toSubMeas u)

The incoming consistency of the original polynomial measurement gives the matching-mass lower bound used in the helper-stage completeness proof.

This is the last step of the proof of references/ldt-paper/self_improvement.tex, lines 407--414: after evaluating the original input measurement G at a random point, ConsRel ... nu says the off-diagonal mass is at most nu, hence the diagonal matching mass is at least 1 - nu. The blueprint mirror is blueprint/src/chapter/ch07_self_improvement.tex, lines 137--142.

theorem MIPStarRE.LDT.SelfImprovement.input_match_mass_eq_sdp_overlap {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => qBipartiteMatchMass strategy.state (strategy.pointMeasurement.toIdxSubMeas u) (polynomialEvaluationFamily params G u)) = ∑ g : Polynomial params, ev strategy.state (opTensor (averagedPointOperator params strategy g) (G.outcome g))

Reindex the averaged input-consistency overlap as the SDP overlap Σ_g ⟨ψ, A_g ⊗ G_g⟩.

This is the algebraic content of references/ldt-paper/self_improvement.tex, lines 410--411: the pointwise match mass E_u Σ_a ⟨ψ, A^u_a ⊗ G_[g(u)=a] ψ⟩ is the same expression as Σ_g ⟨ψ, (E_u A^u_{g(u)}) ⊗ G_g ψ⟩, after reindexing by the value of g at u. The blueprint mirror is blueprint/src/chapter/ch07_self_improvement.tex, lines 137--141.

theorem MIPStarRE.LDT.SelfImprovement.sdp_overlap_le_dual_mass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : SubMeas (Polynomial params) ι) (Z : Quantum.Op ι) (hZ : 0 ≤ Z) (hdual : ∀ (g : Polynomial params), 0 ≤ sdpDualSlackOperator params strategy Z g) : ∑ g : Polynomial params, ev strategy.state (opTensor (averagedPointOperator params strategy g) (G.outcome g)) ≤ ev strategy.state (leftTensor Z)

Dual feasibility upper-bounds the SDP overlap by the dual mass ⟨ψ, Z ⊗ I ψ⟩.

This formalizes references/ldt-paper/self_improvement.tex, lines 408--410: since G is a submeasurement, Z ⊗ I dominates Z ⊗ G, and since the SDP dual is feasible, each Z dominates the averaged point operator E_u A^u_{g(u)}.

theorem MIPStarRE.LDT.SelfImprovement.input_consistency_dual_mass_lower_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (G : Measurement (Polynomial params) ι) (Z : Quantum.Op ι) (nu : Error) (hZ : 0 ≤ Z) (hdual : ∀ (g : Polynomial params), 0 ≤ sdpDualSlackOperator params strategy Z g) (hcons : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) nu) : 1 - nu ≤ ev strategy.state (leftTensor Z)

The input-consistency lower bound, after the SDP reindexing and dual feasibility steps, gives the lower bound on the dual mass used in helper completeness.

This packages references/ldt-paper/self_improvement.tex, lines 406--412, without asserting the later Cauchy--Schwarz comparison from Hhat to Z or any of the projective final-fields transport handled by PR #1071.

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

Complementary slackness converts the averaged-point sum to the dual mass.

This is the exact algebraic replacement used at the end of references/ldt-paper/self_improvement.tex, lines 397--403: after the Cauchy--Schwarz moves have produced Σ_h ⟨ψ, T_h · (E_u A^u_{h(u)}) ⊗ I ψ⟩, complementary slackness replaces T_h · (E_u A^u_{h(u)}) by T_h · Z, and the primal completeness Σ_h T_h = I reduces the sum to ⟨ψ, Z ⊗ I ψ⟩.