Helper completeness: input consistency and the SDP bridge

The part of the helper-completeness argument that relates input consistency, SDP dual feasibility and complementary slackness (the lower-bound calculation at the end of the completeness proof): the counterpart of the vendored SelfImprovement/Theorems/Results/HelperCompleteness/InputSdp.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. The SDP witnesses T : SubMeas (Polynomial params) 𝔓 and Z : 𝔓 are local; the joint operators are strategy.state.L and strategy.state.opTensor in K →L[ℂ] K.

• input_consistency_match_mass_lower_bound calls cons_rel_uniform_full_total_match_mass_lower_bound without the vendored strategy.isNormalized, a theorem of the model.
• sdp_overlap_le_dual_mass uses dual feasibility 0 ≤ Z - A_g as an exact operator inequality in 𝔓, placed by strategy.state.opTensor through the keystone's opTensor_mono_left, then opTensor_le_leftTensor and ev_mono.
• sdp_complementary_slackness_sum_eq_dual_mass keeps the vendored per-h hypothesis sdpComplementarySlacknessEquation params strategy T Z h, that is T.outcome h * Z = T.outcome h * averagedPointOperator params strategy h in 𝔓, field for field with SdpOptimalPairWithSlackness; the vendored final Matrix.one_mul is one_mul.

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 406--414
• blueprint/src/chapter/ch07_self_improvement.tex

theorem MIPRE.LIDT.Co.SelfImprovement.input_consistency_match_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) (G : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓) (nu : ℝ) (hcons : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) nu) : 1 - nu ≤ MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) fun (u : MIPStarRE.LDT.Point params) => strategy.state.qBipartiteMatchMass (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.

theorem MIPRE.LIDT.Co.SelfImprovement.input_sdp_overlap_fiberwise_sum_eq {𝔓 : 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 : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (u : MIPStarRE.LDT.Point params) : ∑ g : MIPStarRE.LDT.Polynomial params, strategy.state.ev (strategy.state.opTensor (GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy g u) (G.outcome g)) = ∑ a : MIPStarRE.LDT.Fq params, ∑ g : MIPStarRE.LDT.Polynomial params with g.toFun u = a, strategy.state.ev (strategy.state.opTensor (GlobalVariance.pointConditionedOutcomeOperatorAtPolynomial params strategy g u) (G.outcome g))

Reindex a polynomial sum by the value of the polynomial at a fixed point.

This is the finite fiber decomposition used in the input-mass SDP bridge. The lemma keeps the Finset.sum_fiberwise invocation separate from the tensor algebra in input_match_mass_eq_sdp_overlap.

theorem MIPRE.LIDT.Co.SelfImprovement.input_sdp_bracketed_sum_eq_match_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) (G : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (u : MIPStarRE.LDT.Point params) : ∑ a : MIPStarRE.LDT.Fq params, strategy.state.ev (strategy.state.opTensor ((strategy.pointMeasurement u).outcome a) (∑ g : MIPStarRE.LDT.Polynomial params with g.toFun u = a, G.outcome g)) = strategy.state.qBipartiteMatchMass (strategy.pointMeasurement.toIdxSubMeas u) (polynomialEvaluationFamily params G u)

The bracketed fiber expression is exactly the bipartite matching mass of the point measurement against the polynomial measurement evaluated at u.

theorem MIPRE.LIDT.Co.SelfImprovement.input_match_mass_eq_sdp_overlap {𝔓 : 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 : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) fun (u : MIPStarRE.LDT.Point params) => strategy.state.qBipartiteMatchMass (strategy.pointMeasurement.toIdxSubMeas u) (polynomialEvaluationFamily params G u)) = ∑ g : MIPStarRE.LDT.Polynomial params, strategy.state.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.

theorem MIPRE.LIDT.Co.SelfImprovement.sdp_overlap_le_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) (G : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) (hZ : 0 ≤ Z) (hdual : ∀ (g : MIPStarRE.LDT.Polynomial params), 0 ≤ sdpDualSlackOperator params strategy Z g) : ∑ g : MIPStarRE.LDT.Polynomial params, strategy.state.ev (strategy.state.opTensor (averagedPointOperator params strategy g) (G.outcome g)) ≤ strategy.state.ev (strategy.state.L 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 MIPRE.LIDT.Co.SelfImprovement.input_consistency_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) (G : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) (nu : ℝ) (hZ : 0 ≤ Z) (hdual : ∀ (g : MIPStarRE.LDT.Polynomial params), 0 ≤ sdpDualSlackOperator params strategy Z g) (hcons : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params G.toSubMeas) nu) : 1 - nu ≤ strategy.state.ev (strategy.state.L 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.

theorem MIPRE.LIDT.Co.SelfImprovement.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) (T : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (Z : 𝔓) (hT_total : T.total = 1) (hcomp : ∀ (h : MIPStarRE.LDT.Polynomial params), sdpComplementarySlacknessEquation params strategy T 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 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 ψ⟩.