reduction_attraction

R5 F3 — the hLandsInΓ₁ discharge and the rung-closing rewire

Seal

Rung R5 · Status interfaced — all four theorems axiom-clean (#print axioms verbatim in 5. The machine seal), no sorryAx. T8-A and T8-B are sealed outright (no interface anywhere in their proofs); T8-C consumes the row-23 output; T8-D is the rung-closing rewire: reduction_asymptotic_stability with BOTH Appendix-A cores discharged, resting on hUSA alone. This closes R5’s destination: ledger rows 23 (hStable) and 24 (hLandsInΓ₁) are both DISCHARGED.
Links: module index · interface ledger · consumes Reduction (L4a), L-A), ReductionStabilityFinish (L-C) · recon (~/Code/notes/ctrllib_r5_f3_recon.md) · source elhawwary2013reduction

What this seals, in one paragraph

EHM-2013 Theorem 8 (local branch, Appendix A.2, corpus elhawwary2013reduction.md:1470-1511) supplies the second topology core that reduction_asymptotic_stability assumed: near a compact Γ₁, orbits are forward-precompact with ω-limit sets inside Γ₁. Unlike Theorem 6’s finish, A.2 is self-contained — its citations (:1472-1475) are inspiration, not load-bearing — so no interface cut was needed anywhere in this lane (recon finding 1). Three parallel-lane seals (T8-A, T8-B, T8-C, all first-elaboration-pass) plus the composition T8-D close the rung: the reduction theorem now stands on the single external core hUSA (EHM-2009 Lemma 2.5), exactly the boundary the F2 decision sanctioned. No SymPy pin — pure topology, nothing numeric to cross-check.

1. The four theorems

T8-A omegaLimit_subset_of_tendsto_infDist (sealed, metric-only): a trajectory drawn to a closed nonempty Γ₂ has its ω-limit set inside Γ₂. One application of the L3 engine eq_on_omegaLimit_of_tendsto to infDist(·)\,Γ₂, then closed-membership. The exact dual of tendsto_infDist_of_omegaLimit_subset.

T8-B omegaLimit_subset_of_stableRelativeTo (sealed, metric-only — the recon’s long pole, sealed first-pass): the backward-orbit core, A.2 steps 4–7. If a forward-precompact orbit’s ω-limit set lies in Γ₂, each of its points is drawn to Γ₁, and Γ₁ is stable relative to Γ₂, the ω-limit set lies in Γ₁. Proof: pick w in the ω-limit set at distance ε > 0 from Γ₁; the backward sequence ϕ(−k)\,w lives in the compact invariant ω-limit set, so Bolzano–Weierstrass gives a limit point q; q’s forward orbit enters the relative-stability tube, and following it forward to time σ(j) reassembles w — which relative stability then pins strictly inside the ε-tube, contradiction. Deviation from the paper’s letter, recorded loudly: the α-limit set L⁻(ω) of A.2 is replaced by the single limit point q (recon §6.2’s pre-registered primary route; the faithful omegaLimit atBot fallback was never needed).

T8-C exists_forwardPrecompact_omegaLimit_subset_of_stableSet (consumes row 23): the assembly producing the character-exact hLandsInΓ₁ formula of Reduction.lean:157-158. Its distinctive content: the paper’s condition (iii) (precompactness near Γ₁) is derived from set stability — stability at level δa/2 confines orbits from a δ₀-tube into a bounded tube strictly inside the relative basin (the (A.5) inclusion), giving forward precompactness via Bornology.IsBounded.thickening + forwardPrecompact_of_isBounded. This is the Theorem-10 combination glue EHM leave implicit at :308.

T8-D reduction_asymptotic_stability_of_uniformSemiAttractor (the rewire): AsymStableSet ϕ Γ₁ from hUSA + the standing conditions of EHM Theorems 8/10 — conditions (i) (hStabRel/hAttrRel, i.e. AsymStableRelativeTo unbundled), (ii) (hLSN, hLAN), the LUB rider, positive invariance, [FiniteDimensional ℝ E], and the compact two-set setup. A pure composition: L-C’s assembly produces hStable; T8-C turns it into hLandsInΓ₁; L4a’s reduction_asymptotic_stability finishes.

1b. The proofs, in full

A remark on technique before we start. Three of the four proofs are confinement arguments of the same species as the Theorem-6 finish, and one (T8-B) is a genuinely different animal: a backward-in-time argument. The paper reaches backward through the α-limit set; we reach backward through a single subsequence limit. Watching where “backward” is legal is the whole game — the flow is two-sided by type, but invariance of the ω-limit set is what lets us evaluate at negative times without leaving home.

T8-A. Suppose the trajectory of $x$ is drawn to the closed nonempty set ${\Gamma }_2$, meaning $\mathrm{infDist}({\phi }_{t}x,{\Gamma }_2)\to 0$. The engine lemma eq_on_omegaLimit_of_tendsto (lasalle_invariance) says: a continuous observable that converges along a trajectory is constant on the trajectory’s ω-limit set, with the limit as its value. Apply it to the observable $y\mapsto \mathrm{infDist}(y,{\Gamma }_2)$, which is continuous. Every point $y$ of the ω-limit set therefore satisfies $\mathrm{infDist}(y,{\Gamma }_2)=0$; and for a closed nonempty set, zero distance is membership. $■$ Three lines in Lean — the engine did the work in L3.

T8-B. Assume the setup: the orbit of $x$ is forward-precompact, its ω-limit set lies in ${\Gamma }_2$, every point of the ω-limit set is drawn to ${\Gamma }_1$ in forward time, and ${\Gamma }_1$ is stable relative to ${\Gamma }_2$. We must show the ω-limit set lies in ${\Gamma }_1$.

Proof idea. Take a point $w$ of the ω-limit set at positive distance $\epsilon$ from ${\Gamma }_1$, and run time backward from $w$ — staying inside the ω-limit set, which is invariant. Somewhere back there, a limit point $q$ exists (compactness), and $q$‘s forward orbit dives toward ${\Gamma }_1$ (the basin hypothesis). But once an orbit inside ${\Gamma }_2$ is that close to ${\Gamma }_1$, relative stability forbids it from ever climbing back out to distance $\epsilon$ — and yet, following it forward far enough must reproduce $w$ exactly. Contradiction.

Proof. Suppose, for contradiction, that some $w$ in the ω-limit set is not in ${\Gamma }_1$. Since ${\Gamma }_1$ is closed and nonempty, the distance $\epsilon :=\mathrm{infDist}(w,{\Gamma }_1)$ is strictly positive. Relative stability of ${\Gamma }_1$ with respect to ${\Gamma }_2$, invoked at the level $\epsilon$, provides $\delta >0$ such that any ${\Gamma }_2$-point within $\delta$ of ${\Gamma }_1$ has its whole forward orbit strictly inside the $\epsilon$-tube of ${\Gamma }_1$ (the paper’s neighbourhood $N_4$, :1500-1502).

The ω-limit set is closed, sits inside the closure of the forward orbit — which is compact by forward precompactness — and is therefore compact. It is also invariant under the flow for all real times, by the same shift argument the LaSalle module uses. Consequently the backward points ${\phi }_{-k}w$, for natural numbers $k$, all remain in the ω-limit set, and compactness extracts a subsequence ${\phi }_{-\sigma (j)}w\to q$ with $q$ in the ω-limit set (:1502-1509).

The basin hypothesis at $q$ says $\mathrm{infDist}({\phi }_{s}q,{\Gamma }_1)\to 0$ as $s\to \infty$, so there is a time $s\ge 0$ with $\mathrm{infDist}({\phi }_{s}q,{\Gamma }_1)<\delta /2$. The time-$s$ map is continuous, so applying it along the subsequence, ${\phi }_s({\phi }_{-\sigma (j)}w)\to {\phi }_{s}q$; pick an index $j$ large enough that this image is within $\delta /2$ of ${\phi }_{s}q$ and $\sigma (j)\ge s$. Write $z:={\phi }_s({\phi }_{-\sigma (j)}w)$.

Now audit $z$‘s addresses. It lies in the ω-limit set (invariance twice), hence in ${\Gamma }_2$. Its distance to ${\Gamma }_1$ obeys, by the Lipschitz property of the point-to-set distance,

$\mathrm{infDist}(z,{\Gamma }_1)\le \mathrm{infDist}({\phi }_{s}q,{\Gamma }_1)+\Vert z-{\phi }_{s}q\Vert <\frac{\delta }{2}+\frac{\delta }{2}=\delta$

So $z$ is exactly the kind of point relative stability governs. Finally, the flow law reassembles $w$ from $z$: writing $t:=\sigma (j)-s\ge 0$,

${\phi }_{t}z={\phi }_{\sigma (j)-s}({\phi }_s({\phi }_{-\sigma (j)}w))={\phi }_{(\sigma (j)-s)+s-\sigma (j)}w={\phi }_{0}w=w$

Relative stability now delivers the blow: since $z\in {\Gamma }_2$ with $\mathrm{infDist}(z,{\Gamma }_1)<\delta$ and $t\ge 0$, the forward image satisfies $\mathrm{infDist}({\phi }_{t}z,{\Gamma }_1)<\epsilon$. But ${\phi }_{t}z=w$, whose distance to ${\Gamma }_1$ is $\epsilon$. A quantity cannot be strictly less than itself, so no such $w$ exists. $■$

The moral. The paper’s α-limit set is bookkeeping for “some backward limit point exists” — and one Bolzano–Weierstrass point is all the argument consumes. That is the deviation from the paper’s letter (pre-registered in the recon, §6.2), and seeing the proof written out is the best argument that it is the same proof.

T8-C. We must produce a radius $\delta >0$ such that every $x$ within $\delta$ of ${\Gamma }_1$ has a forward-precompact orbit with ω-limit set inside ${\Gamma }_1$ — the exact hLandsInΓ₁ formula.

Proof. Unpack the three tube-producing hypotheses. Relative attractivity provides a basin radius ${\delta }_a>0$: every ${\Gamma }_2$-point within ${\delta }_a$ of ${\Gamma }_1$ is drawn to ${\Gamma }_1$. Set stability — the row-23 output — invoked at the level ${\delta }_a/2$, provides ${\delta }_0>0$: orbits starting within ${\delta }_0$ of ${\Gamma }_1$ remain within ${\delta }_a/2$ of it forever. Local attractivity of ${\Gamma }_2$ provides ${\delta }_L>0$: orbits starting within ${\delta }_L$ of ${\Gamma }_1$ are drawn to ${\Gamma }_2$. Take $\delta :=\min ({\delta }_0,{\delta }_L)$ and let $x$ be any point within $\delta$ of ${\Gamma }_1$.

Forward precompactness (the paper’s condition (iii), derived). The whole forward orbit of $x$ stays within ${\delta }_a/2$ of the compact set ${\Gamma }_1$, hence inside a bounded thickening of a bounded set; a bounded orbit in a finite-dimensional space has compact closure. This is the step the paper’s Theorem 8 simply assumes as condition (iii) and Theorem 10 quietly needs (:308); deriving it from set stability is what makes the final assembly self-contained.

The ω-limit set lands in ${\Gamma }_2$. Since $x$ starts within ${\delta }_L$ of ${\Gamma }_1$, its orbit is drawn to ${\Gamma }_2$, and T8-A places its ω-limit set inside ${\Gamma }_2$ (closed, nonempty since it contains ${\Gamma }_1$).

The ω-limit set sits inside the basin. The orbit never leaves the ${\delta }_a/2$-tube, and the set of points at distance at most ${\delta }_a/2$ from ${\Gamma }_1$ is closed (a sublevel set of a continuous function), so it also contains the closure of the orbit — in particular the ω-limit set. Every ω-limit point is therefore a ${\Gamma }_2$-point strictly within ${\delta }_a$ of ${\Gamma }_1$ — inside the relative basin — so relative attractivity draws each one to ${\Gamma }_1$ in forward time. This is the paper’s inclusion (A.5).

Collapse. All of T8-B’s hypotheses are now verified for the orbit of $x$: forward precompactness, ω-limit set in ${\Gamma }_2$, pointwise basin, and relative stability. Hence the ω-limit set lies in ${\Gamma }_1$. $■$

T8-D. Pure composition, no new mathematics: the L-C assembly (reduction_stability_finish) produces hStable from hUSA and the standing conditions; T8-C turns hStable into the hLandsInΓ₁ formula; and L4a’s reduction_asymptotic_stability (reduction_cascade) combines the two into asymptotic stability of ${\Gamma }_1$. Ledger rows 23 and 24 close simultaneously, and what remains named is hUSA alone. $■$

The moral of the module. EHM’s Appendix A.2 needed no interface because it never leaves the world of flows and metric topology — every citation it makes is decorative. The single place the whole R5 chain touches un-formalized mathematics is the Lemma-2.5 bridge from attractivity to uniform semi-attraction, and that is now one theorem-shaped hole with a decided proof route, not a fog.

2. The trust boundary after this module

reduction_asymptotic_stability’s two named cores are gone. What remains named anywhere in the R5 chain is exactly hUSA (interfaces row) — EHM-2009 Lemma 2.5, the R6 rung, route decided (compact-branch direct). Every other hypothesis of T8-D is a condition the paper’s own theorems state; per the honest-boundary discipline they are modelling inputs, not debt.

3. Source-fidelity notes

• Theorem 8’s conditions verified at corpus :286-295; the :308 combination sentence; A.2’s proof at :1477-1511. All three lanes re-read the source before writing (the recon’s step map held).
• The ledger’s old row-24 attribution “Lemma 22” was imprecise — A.2 never uses Lemma 22 (its mentions at :1283/:1318/:1397 are all in A.1). Corrected in the ledger row this session.
• hsub : Γ₁ ⊆ Γ₂ (the paper’s standing Γ₁ ⊂ Γ₂, :286) is consumed only for Γ₂.Nonempty in T8-C; kept in the provenance-faithful form.

4. Mathlib inventory (new in this module; all grep-verified in the pinned tree)

isClosed_omegaLimit, omegaLimit_subset_closure_image2, Flow.isInvariant_omegaLimit (Dynamics/OmegaLimit.lean:81/:192/:314); IsCompact.of_isClosed_subset, IsCompact.tendsto_subseq (Topology/Sequences.lean:298); Flow.map_add/map_zero_apply/continuous_toFun (Dynamics/Flow.lean:125/:130/:274); Bornology.IsBounded.thickening (Thickening.lean:172); closure_minimal; tendsto_natCast_atTop_atTop (AtTopBot/Archimedean.lean:44 — the one-liner that killed the recon’s flagged ℕ→ℝ cast-bookkeeping risk); Tendsto.eventually_lt_const, Tendsto.eventually_ge_atTop, tendsto_atTop_add_const_left. Ctrllib substrate: eq_on_omegaLimit_of_tendsto, forwardPrecompact_of_isBounded, tendsto_infDist_of_omegaLimit_subset, the Reduction.lean predicates, and the full L-C chain.

5. The machine seal

#print axioms, verbatim from the full build (lake build, 2026-07-09 late evening; Built Ctrllib, 2659/2660 jobs):

info: Ctrllib/ReductionAttraction.lean:233:0: 'Ctrllib.omegaLimit_subset_of_tendsto_infDist' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/ReductionAttraction.lean:234:0: 'Ctrllib.omegaLimit_subset_of_stableRelativeTo' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/ReductionAttraction.lean:235:0: 'Ctrllib.exists_forwardPrecompact_omegaLimit_subset_of_stableSet' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/ReductionAttraction.lean:236:0: 'Ctrllib.reduction_asymptotic_stability_of_uniformSemiAttractor' depends on axioms: [propext, Classical.choice, Quot.sound]

Nothing beyond {propext, Classical.choice, Quot.sound}; no sorryAx; zero sorry.

6. Scope, honestly (ponytail)

• T8-A/T8-B are genuinely standalone seals; T8-C/T8-D are interfaced only through the L-C chain’s hUSA.
• The three bricks were proved by three parallel lanes elaborating standalone against the built object files (lean + LEAN_PATH, no lake) — every one first-pass, zero fix cycles; the orchestrator integrated serially. The pre-registered fallback cuts (tube-visit brick; omegaLimit atBot) were never fired.
• Not attempted: deriving hAttrRel from hUSA (plausibly redundant — the uniform semi-attractor should imply relative attractivity on a basin); flagged as an R6-adjacent tightening, not chased tonight.