Final-fields self-closeness construction

This module contains the self-closeness transport used to fill the selfCloseness field of SelfImprovementFinalFields. The statements formalize the triangle transport through helper self-consistency and the orthonormalization SDD step in references/ldt-paper/self_improvement.tex, lines 727--741.

Final-fields self-closeness construction

Same playbook as final_fields_completeness_of_helper_completeness, but for the selfCloseness field. Unlike completeness, this field is closed without any new analytic obligation: the helper-stage strong self-consistency hssc and the orthonormalization SDD bound horth already supplied to selfImprovement together suffice, by combining the bipartite-SSC left↔right transport (twoNotionsOfSelfConsistency), the perm-inv left↔right SDD reflection (MakingMeasurementsProjective.sddRel_liftRight_of_liftLeft_permInv), and the three-step SDD triangle inequality (Preliminaries.stateDependentDistanceRel_triangle_three).

Concretely the chain is H.liftLeft → Hhat.liftLeft → Hhat.liftRight → H.liftRight, with edges of error ε, 2δ, ε and the triangle constant 3, giving the final 3 * (ε + 2δ + ε) bound. The remaining gap to the literal selfImprovementError threshold used inside SelfImprovementFinalFields is a separate numerical comparison on the explicit error definitions.

This is not an additional residual hypothesis: this construction derives the entire selfCloseness field from data already present in the selfImprovement proof. It does not assume the projective self-closeness it produces and does not restate a combined final-fields hypothesis block.

Paper anchors:

• references/ldt-paper/self_improvement.tex lines 727--741 — projective self-closeness Hhat ⊗ I ≈ I ⊗ Hhat → H ⊗ I ≈ I ⊗ H via the triangle. The corresponding blueprint paragraph is blueprint/src/chapter/ch07_self_improvement.tex \emph{Proof of \ref{item:self-improvement-self-closeness}}.

theorem MIPStarRE.LDT.SelfImprovement.self_closeness_transport_through_orthonormalization {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} [Fintype α] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (A B : SubMeas α ι) (δ ε : Error) (hssc : BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily A) δ) (horth : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily A).liftLeft (constSubMeasFamily B).liftLeft ε) : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily B.liftLeft) (constSubMeasFamily B.liftRight) (3 * (ε + 2 * δ + ε))

Generic self-closeness transport through helper-stage strong self-consistency and the orthonormalization SDD step, for the Unit-indexed constant-family setting used by the self-improvement pipeline.

Given:

• hssc — bipartite strong self-consistency of the helper submeasurement A (helper SSC).
• horth — orthonormalization SDD bound between the left lifts of A and the projective replacement B.

Conclusion: SDD between the left and right placements of B, with the natural three-step paper sum 3 * (ε + 2δ + ε).

Proof: twoNotionsOfSelfConsistency gives A.liftLeft ≃_{2δ} A.liftRight; sddRel_liftRight_of_liftLeft_permInv reflects horth to a right-lift bound; the triangle B.liftLeft ↔ A.liftLeft ↔ A.liftRight ↔ B.liftRight then applies stateDependentDistanceRel_triangle_three.

theorem MIPStarRE.LDT.SelfImprovement.final_fields_self_closeness {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (Hhat : SubMeas (Polynomial params) ι) (H : ProjSubMeas (Polynomial params) ι) (hssc : BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily Hhat) (selfImprovementHelperError params eps delta)) (horth : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily Hhat.liftLeft) (constSubMeasFamily H.liftLeft) (selfImprovementOrthogonalizationError params eps delta)) : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas H.toSubMeas)) (3 * (selfImprovementOrthogonalizationError params eps delta + 2 * selfImprovementHelperError params eps delta + selfImprovementOrthogonalizationError params eps delta))

Final-fields self-closeness construction.

Specializes self_closeness_transport_through_orthonormalization to the self-improvement parameters. Given the helper-stage bipartite SSC of Hhat and the orthonormalization SDD bound between Hhat.liftLeft and H.toSubMeas.liftLeft (both already produced inside selfImprovement), this checked theorem derives the selfCloseness field of SelfImprovementFinalFields with the natural paper sum-of-errors 3 * (selfImprovementOrthogonalizationError + 2 * selfImprovementHelperError + selfImprovementOrthogonalizationError).

Crucially, this construction adds no new analytic hypothesis: both hssc and horth are already supplied to selfImprovement, so the selfCloseness field of SelfImprovementFinalFields is now fully derivable up to a numerical threshold comparison.

theorem MIPStarRE.LDT.SelfImprovement.final_fields_self_closeness_of_small_errors {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (heps : 0 ≤ eps) (heps_le_one : eps ≤ 1) (hdelta : 0 ≤ delta) (hdelta_le_one : delta ≤ 1) (hd_le_q : ↑params.d ≤ ↑params.q) (Hhat : SubMeas (Polynomial params) ι) (H : ProjSubMeas (Polynomial params) ι) (hssc : BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily Hhat) (selfImprovementHelperError params eps delta)) (horth : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily Hhat.liftLeft) (constSubMeasFamily H.liftLeft) (selfImprovementOrthogonalizationError params eps delta)) : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas H.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas H.toSubMeas)) (selfImprovementError params eps delta)

Literal-threshold self-closeness construction under the standard unit-interval hypotheses.

This wraps final_fields_self_closeness with the numerical absorption final_fields_self_closeness_error_le_selfImprovementError, giving exactly the selfCloseness threshold used in SelfImprovementFinalFields.