Final-fields self-closeness construction #
The self-closeness transport that fills the selfCloseness field of
SelfImprovementFinalFields: the triangle through helper self-consistency and the
orthonormalization SDD step. The counterpart of the vendored
SelfImprovement/Theorems/Results/SelfImprovementTop/SelfCloseness.lean (under
MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10,
section "Port conventions").
Contents #
self_closeness_transport_through_orthonormalization: the generic transport alongB.liftLeft → A.liftLeft → A.liftRight → B.liftRight, with edgesε,2δ,εand the triangle constant3.final_fields_self_closenessand…_of_small_errors: its specialization to the self-improvement errors, at the natural and at the literal threshold.
The theorems take the orthonormalization SDD bound as a hypothesis and call no orthonormalization,
so they carry no finite-pair, abelian-projection or ζ > 0 hypothesis.
The translation is that of BoundednessTransport/BoundednessGap.lean: a strategy is a
SymStrat params 𝔓 K, A.liftLeft is A.liftLeft strategy.state, IdxSubMeas.liftLeft F and
IdxSubMeas.liftRight F are IdxSubMeas.liftLeft strategy.state F and
IdxSubMeas.liftRight strategy.state F, leftPlacedSubMeas (ιB := ι) and
rightPlacedSubMeas (ιA := ι) are strategy.state.leftPlacedSubMeas and
strategy.state.rightPlacedSubMeas, the relations are read on strategy.state, and Error is
ℝ. Swap symmetry is a theorem of the model, so the vendored
MakingMeasurementsProjective.sddRel_liftRight_of_liftLeft_permInv strategy.permInvState … is
M8's MakingMeasurementsProjective.sddRel_liftRight_of_liftLeft_permInv strategy.state …, and the
vendored hypothesis ⟨strategy.permInvState, hssc⟩ of Preliminaries.twoNotionsOfSelfConsistency
is hssc (M3). No statement of the vendored file carries a swap, density or normalization
hypothesis, so no statement changed beyond the translation; the file sets no option, the vendored
file-wide respectTransparency false not being needed.
The classical threshold lemma final_fields_self_closeness_error_le_selfImprovementError
(vendored Thresholds/Final.lean) is imported; the imports mirror the vendored ones.
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.texlines 727--741blueprint/src/chapter/ch07_self_improvement.tex, the proof ofitem:self-improvement-self-closeness
Generic self-closeness transport through helper-stage strong self-consistency and the
orthonormalization SDD step, for the Unit-indexed constant families of the self-improvement
pipeline.
From the bipartite strong self-consistency hssc of A at δ and the orthonormalization SDD
bound horth between the left lifts of A and B at ε, the left and right placements of B
are 3 (ε + 2δ + ε)-close: twoNotionsOfSelfConsistency gives A.liftLeft ≃_{2δ} A.liftRight,
sddRel_liftRight_of_liftLeft_permInv reflects horth to the right lifts, and
stateDependentDistanceRel_triangle_three closes
B.liftLeft → A.liftLeft → A.liftRight → B.liftRight.
Final-fields self-closeness construction.
self_closeness_transport_through_orthonormalization at the self-improvement errors: from the
helper-stage bipartite SSC of Hhat and the orthonormalization SDD bound between Hhat.liftLeft
and H.toSubMeas.liftLeft, both produced inside selfImprovement, the selfCloseness field of
SelfImprovementFinalFields at the natural paper sum
`3 (selfImprovementOrthogonalizationError + 2 selfImprovementHelperError
- selfImprovementOrthogonalizationError)`, with no new analytic hypothesis.
Literal-threshold self-closeness construction under the standard unit-interval hypotheses:
final_fields_self_closeness with the numerical absorption
final_fields_self_closeness_error_le_selfImprovementError, giving exactly the selfCloseness
threshold of SelfImprovementFinalFields.