reduction_stability_finish

R5 L-C — the Theorem-6 finish: StableSet from the uniform semi-attractor

Seal

Rung R5 · Status interfaced — all eight theorems axiom-clean (#print axioms verbatim in 6. The machine seal), no sorryAx. The core theorem was sealed with three named interfaces (hUSA, hFirstExit, hContDep); the two flow-side interfaces were discharged in-module the same evening by parallel tightening lanes, so the public assembly stableSet_of_uniformSemiAttractor_of_forwardInvariant rests on hUSA alone. This module discharges ledger rows hStable, hFirstExit, hContDep: the L4a hypothesis hStable : StableSet ϕ Γ₁ is now a proved conclusion whose entire remaining trust boundary is EHM-2009 Lemma 2.5.
Links: module index · interface ledger · consumes L-A) and Reduction (L4a) · recon (/Code/notes/ctrllib_r5_mathlib_recon.md) · R6 recon (/Code/notes/ctrllib_r6_lemma25_recon.md) · sources elhawwary2013reduction + EHM-2009 (arXiv:0907.0686, corpus filing in flight)

What this seals, in one paragraph

EHM-2013 Theorem 6 (compact branch) proves set stability of ${\Gamma }_1$ by contradiction: if ${\Gamma }_1$ were unstable, Lemma 22 extracts an escape sequence whose base points converge to some $\bar{x}\in {\Gamma }_1$, and a µ-tube compactness argument around $\bar{x}$ forces the escaping orbits back into the tube they were supposed to leave — contradiction. The proof text (corpus elhawwary2013reduction.md:1317-1461) invokes, at :1347, “Lemma 2.5 in El-Hawwary and Maggiore (2009)” to convert relative attractivity into the uniform semi-attractor property (A.1). That external bridge is taken here as the named hypothesis hUSA; two flow-regularity steps of the finish are likewise named (hFirstExit, hContDep); everything else is sealed: the uniform-basin extraction (A.2)+(A.3), the ball-nesting claim, the segment-approaches-${\Gamma }_2$ step, and the final contradiction glue. The module is (~/Code/vault/lean/ReductionStabilityFinish.lean), build copy ~/lean/ctrllib/Ctrllib/ReductionStabilityFinish.lean.

No SymPy pin: pure metric topology, no numeric content (sympy_pin: ""), same deliberate omission as reduction_stability.

1. The mathematical objects

Same conventions as L4a and reduction_stability: real normed space $E$, Metric.infDist x Γ for the point-to-set distance, EHM’s $B_{\delta }(\Gamma )$ = the predicate $\mathrm{infDist}(x,\Gamma )<\delta$, flow application ${\phi }_{t}x$ = ϕ t x. The one new definition transcribes EHM-2009 Def 2.1(iv) in its relative form — the property the 2013 finish labels (A.1):

$\text{UniformSemiAttractorRelativeTo}\phi {\Gamma }_1{\Gamma }_2:=\forall x\in {\Gamma }_1,\exists \mu >0,\forall {\epsilon }^{\prime }>0,\exists T>0,\forall y,\Vert y-x\Vert <\mu \Rightarrow y\in {\Gamma }_2\Rightarrow \forall t\ge T,\mathrm{infDist}({\phi }_{t}y,{\Gamma }_1)<{\epsilon }^{\prime }.$

The R6 recon verified this is a quantifier-for-quantifier transcription of the 2009 paper’s eq. (18) (p. 21) — the exact formula Lemma 2.5 produces — so no adapter theorem will be needed when hUSA is discharged.

2. The graded interfaces — what is assumed, and why each is honest

Per the charter’s honest-boundary discipline, an interface hypothesis must be a true, later-derivable fact with a named seal route — never a restatement of the conclusion.

hypothesis	content (paper site)	fate
hUSA	Lemma 2.5’s output: ${\Gamma }_1$ is a uniform semi-attractor relative to ${\Gamma }_2$ (:1347-1351)	OPEN — the module’s only interface. Discharge = formalize EHM-2009 Appendix A — the R6 rung; go/no-go GO per (~/Code/notes/ctrllib_r6_lemma25_recon.md), 2 theorems + 1 rewire, route decided by the user: compact-branch direct. EHM condition (i) hAttr and ${\Gamma }_2$-side hypotheses are consumed there, which is why they do not appear in this module’s statement.
hFirstExit	Lemma 22 in first-exit form: ONE base sequence $x_i\to {\Gamma }_1$, and per level $\epsilon \le {\epsilon }_0$ an exit-time sequence with $\mathrm{infDist}({\phi }_{t_i}{x}_i,{\Gamma }_1)=\epsilon$, orbit inside the $\epsilon$-tube on $[0,t_i)$, and $t_i\to \infty$ (:1318-1322, :1421)	DISCHARGED same evening by firstExit_of_not_stableSet: Brick 1 exists_firstExitTime = hitting-time infimum (sInf of the closed hitting set + left-limit, IsClosed.csInf_mem); Brick 3 exists_uniform_tube_radius = the tube lemma on [0,B] ×ˢ Γ₁ inside the open sublevel set of the jointly-continuous tube function (generalized_tube_lemma + IsCompact.exists_thickening_subset_open) — no subsequence extraction, no finite dimension; Brick 2 = assembly over L-A’s base sequence. Positive invariance hfi is consumed exactly here (:1303, :1421).
hContDep	continuous dependence at the fixed time $T$ on a ball (:1447)	DISCHARGED same evening by contDep_of_flow: Heine–Cantor (IsCompact.uniformContinuousOn_of_continuous) on the compact closedBall p (r+1) from Flow.continuous_toFun, with a min δ 1 cap keeping both points in the collar.

The level-family quantifier in hFirstExit is load-bearing. The paper’s footnote 3 (:1396-1398) shrinks $\epsilon$ below $\mu$ after $\mu$ is extracted — sound only because $\mu$ depends on $(\bar{x},m)$ alone, and the same base sequence admits first-exit times at every smaller level (an orbit that reaches distance ${\epsilon }_0$ crosses every level below it). A single-level interface would have made the Lean statement circular ($\mu$ needs $\bar{x}$, $\bar{x}$ needs the sequence, the sequence would need $\epsilon <\mu$).

3. Theorem 1 — ball-nesting brick (infDist_subCollar_of_mem_inter, sealed)

${\Gamma }_1\ne \varnothing ,\bar{x}\in {\Gamma }_1,m>0,\mathrm{infDist}(z,{\Gamma }_1)<\mu ,\Vert z-\bar{x}\Vert <m\Rightarrow \mathrm{infDist}(z,{\Gamma }_1\cap {\overline{B}}_{2m}(\bar{x}))<\mu .$

The paper’s claim at :1382-1408: $B_{\mu }({\Gamma }_1)\cap B_m(\bar{x})\subseteq B_{\mu }({\Gamma }_1^{\prime })$ with ${\Gamma }_1^{\prime }={\Gamma }_1\cap \mathrm{cl}(B_{2m}(\bar{x}))$. Sealed unchanged from the previous session. (The R6 recon found the 2009 paper’s Appendix D, pp. 21–22, contains a clean twin of this claim — a useful un-scrambled cross-check on the 2013 OCR.)

Why we need it. The uniform basin radius $\mu$ of Theorem 2 is only valid at centers inside the compact set ${\Gamma }_1^{\prime }$ — but the point the main proof produces is merely close to ${\Gamma }_1$, which may be unbounded. This brick converts “close to ${\Gamma }_1$ and close to $\bar{x}$” into “close to the compact collar,” which is where the basin machinery lives.

Proof. Let $z$ be a point with $\mathrm{infDist}(z,{\Gamma }_1)<\mu$ and $\Vert z-\bar{x}\Vert <m$. We must exhibit a point of ${\Gamma }_1\cap {\overline{B}}_{2m}(\bar{x})$ within distance $\mu$ of $z$. There are two cases, split on whether $\mu \le m$.

Case $\mu \le m$. Since $\mathrm{infDist}(z,{\Gamma }_1)<\mu$ and ${\Gamma }_1$ is nonempty, there is a witness $y\in {\Gamma }_1$ with $\Vert z-y\Vert <\mu$. We claim this same $y$ lies in the collar. Indeed, by the triangle inequality through $z$,

$\Vert y-\bar{x}\Vert \le \Vert y-z\Vert +\Vert z-\bar{x}\Vert <\mu +m\le 2m$

so $y\in {\Gamma }_1\cap {\overline{B}}_{2m}(\bar{x})$, and the distance from $z$ to the collar is at most $\Vert z-y\Vert <\mu$, as desired.

Case $\mu >m$. Here the collar’s own center does the job: $\bar{x}$ belongs to ${\Gamma }_1$ by hypothesis and to ${\overline{B}}_{2m}(\bar{x})$ trivially (its radius $2m$ is positive), and $\Vert z-\bar{x}\Vert <m<\mu$. Hence the distance from $z$ to the collar is below $\mu$ in this case too. $■$

The moral. Nothing about flows here — the brick is a statement about metric geometry alone, which is why it sealed axiom-clean in a single sitting. The paper’s two cases are exactly the two branches of the Lean by_cases.

4. Theorem 2 — uniform basin over a compact set (uniform_basin_of_uniformSemiAttractor, sealed)

The paper’s (A.2)+(A.3) (:1352-1381): from the per-point radii $\mu (x)$ of hUSA, compactness of $K\subseteq {\Gamma }_1$ yields a single $\mu >0$, and then per tube level ${\epsilon }^{\prime }$ a single $T>0$:

$\exists \mu >0,\forall {\epsilon }^{\prime }>0,\exists T>0,\forall x\in K,\phi ([T,\infty ),B_{\mu }(x)\cap {\Gamma }_2)\subseteq B_{{\epsilon }^{\prime }}({\Gamma }_1).$

Scratch work — why the paper’s own sentence needs repair. The paper says “the infimum of $\mu (x)$, in (A.1), for all $x\in {\Gamma }_1^{\prime }$ exists and is greater than zero” (:1352-1360). As stated this is not a theorem: an infimum of positive numbers over an infinite set can perfectly well be zero, and the function $x\mapsto \mu (x)$ handed to us by hUSA carries no continuity whatsoever (it comes from the axiom of choice). What is true is that compactness lets us replace the infinite family by a finite one — and a finite minimum of positive numbers is positive. The standard device is to cover with half-radius balls, so that a point covered by the ball at $w$ still has half of $\mu (w)$ to spare for its own neighbourhood.

Proof. For each $x\in {\Gamma }_1$, the hypothesis hUSA provides a basin radius $\mu (x)>0$ such that for every tube level ${\epsilon }^{\prime }>0$ there is a time $T(x,{\epsilon }^{\prime })>0$ with

$\phi ([T(x,{\epsilon }^{\prime }),\infty ),B_{\mu (x)}(x)\cap {\Gamma }_2)\subseteq B_{{\epsilon }^{\prime }}({\Gamma }_1)$

(the property (A.1); in Lean the two choose! calls make $\mu (\cdot )$ and $T(\cdot ,\cdot )$ honest functions). Now cover the compact set $K$ by the open balls $B_{\mu (x)/2}(x)$ as $x$ ranges over $K$ — each is a neighbourhood of its center since $\mu (x)>0$. By compactness (IsCompact.elim_nhds_subcover) finitely many centers $w_1,\dots ,w_n\in K$ suffice, and the finite set is nonempty because $K$ is. Define

$\mu :={\min }_{1\le i\le n}\frac{\mu (w_i)}{2}T({\epsilon }^{\prime }):={\max }_{1\le i\le n}T(w_i,{\epsilon }^{\prime })$

Both are positive, being a finite minimum (respectively maximum) of positive numbers.

We verify the claim. Let $x\in K$, let $y$ be any point with $\Vert y-x\Vert <\mu$ and $y\in {\Gamma }_2$, and let $t\ge T({\epsilon }^{\prime })$. The point $x$ lies in some covering ball, say $\Vert x-w_i\Vert <\mu (w_i)/2$. Then by the triangle inequality through $x$,

$\Vert y-w_i\Vert \le \Vert y-x\Vert +\Vert x-w_i\Vert <\mu +\frac{\mu (w_i)}{2}\le \frac{\mu (w_i)}{2}+\frac{\mu (w_i)}{2}=\mu (w_i)$

where the middle step used that $\mu$ is the minimum of the half-radii. Hence $y$ lies in the per-point basin $B_{\mu (w_i)}(w_i)\cap {\Gamma }_2$, and since $t\ge T({\epsilon }^{\prime })\ge T(w_i,{\epsilon }^{\prime })$, property (A.1) at $w_i$ gives $\mathrm{infDist}({\phi }_{t}y,{\Gamma }_1)<{\epsilon }^{\prime }$, as desired. $■$

The moral. Compactness converts a pointwise promise into a uniform one — but only through a finite intermediary. The half-radius trick is what makes the paper’s infimum sentence rigorous without ever taking an infimum over an infinite set.

Mathlib lemmas used (paths relative to ~/lean/ctrllib/.lake/packages/mathlib/Mathlib/):

lemma	file
IsCompact.elim_nhds_subcover	Topology/Compactness/Compact.lean:226
Metric.ball_mem_nhds	Topology/MetricSpace/Pseudo/Defs
Finset.lt_inf'_iff (to_dual of sup'_lt_iff), Finset.inf'_le, Finset.le_sup'	Data/Finset/Lattice/Fold.lean — requires an explicit import Mathlib.Data.Finset.Lattice.Fold, not in the module’s transitive closure (same import-scope gotcha class as le_or_lt last session)
choose! (total-function choice through ∀ x ∈ Γ₁ binders)	core tactic

5. Theorem 3 — the finish (stableSet_of_uniformSemiAttractor, interfaced)

Statement. [FiniteDimensional ℝ E], ${\Gamma }_1$ compact nonempty, ${\Gamma }_1\subseteq {\Gamma }_2$, hLUB (local uniform boundedness, EHM Def 5), hLSN (${\Gamma }_2$ locally stable near ${\Gamma }_1$, EHM Def 3 = assumption (ii)), plus the three interfaces ⟹ StableSet ϕ Γ₁.

Proof spine, matched to the paper (:1317-1461):

1. by_contra; hFirstExit yields ${\epsilon }_0$, the base sequence $x_i\to {\Gamma }_1$, and the level family.
2. L-B (reduction_stability) extracts a subsequence $x_{\sigma (j)}\to \bar{x}\in {\Gamma }_1$ (compactness of ${\Gamma }_1$ gives closed + bounded).
3. hLUB at $\bar{x}$: radii $\lambda ,m$ with $\phi ({\mathbb{R}}_{+},B_{\lambda }(\bar{x}))\subseteq B_m(\bar{x})$ (:1323-1324).
4. Theorem 2 on the widened collar $K={\Gamma }_1\cap {\overline{B}}_{2(m+1)}(\bar{x})$: the uniform $\mu$ (depends only on $\bar{x},m$ — this is why footnote 3 is non-circular).
5. Working level $\epsilon :=\min ({\epsilon }_0,\mu /2)$ (footnote 3, :1396-1398); exit times $t_i$ at level $\epsilon$; uniform time $T$ at tube level $\epsilon /4$; hContDep radius ${\delta }_{cd}$ at $(T,\bar{x},m+1,\epsilon /2)$; working radius $\delta :=\min (\min ({\delta }_{cd},(\mu -\epsilon )/2),1)$.
6. Segment-approaches-${\Gamma }_2$, sealed inline (:1325-1343): hLSN at $(p=\bar{x},c=m,\epsilon =\delta )$ gives ${\delta }^{\prime }$; for $j$ large, $\mathrm{infDist}(x_{\sigma (j)},{\Gamma }_1)<{\delta }^{\prime }$ and $x_{\sigma (j)}\in B_{\lambda }(\bar{x})$, so hLUB keeps the whole segment in $B_m(\bar{x})$ and hLSN pushes it within $\delta$ of ${\Gamma }_2$. Correction vs. the handoff: the source derives this from local stability (ii) + local uniform boundedness — hLSN + hLUB, not hLSN + hAttr — and it needs no flow regularity, so it is sealed here rather than interfaced.
7. One eventual index $k=\sigma (j)$: $z:={\phi }_{t_k-T}(x_k)$ is pre-exit (so $\mathrm{infDist}(z,{\Gamma }_1)<\epsilon$), inside $B_m(\bar{x})$, and within $\delta$ of ${\Gamma }_2$; take the witness $z^{\prime }\in {\Gamma }_2$, $\Vert z-z^{\prime }\Vert <\delta$ (:1417-1441).
8. $z^{\prime }$ is in the $\mu$-tube ($\epsilon +\delta <\mu$ by construction) and in $B_{m+1}(\bar{x})$ ($\delta \le 1$ absorbs the witness slack — see §7); Theorem 1 nests it into $B_{\mu }(K)$, giving a collar center $x^{\ast }\in K$ with $\Vert z^{\prime }-x^{\ast }\Vert <\mu$.
9. Theorem 2 at $x^{\ast }$: $\mathrm{infDist}({\phi }_T{z}^{\prime },{\Gamma }_1)<\epsilon /4$. hContDep: $\Vert {\phi }_{T}z-{\phi }_T{z}^{\prime }\Vert <\epsilon /2$. Flow law ${\phi }_{t_k}{x}_k={\phi }_T({\phi }_{t_k-T}{x}_k)$ (Flow.map_add, :1424-1426).
10. $\mathrm{infDist}({\phi }_{t_k}{x}_k,{\Gamma }_1)<\epsilon /4+\epsilon /2<\epsilon$, contradicting the first-exit equality $=\epsilon$ (:1442-1461). $■$

The proof, in full

Technique. Contradiction — the natural choice, since instability is a “there exists an escape” statement and our tools (the uniform basin, local uniform boundedness) are all confinement statements. We assume an escape exists and confine it to death.

Proof idea in one breath. If ${\Gamma }_1$ were unstable, some orbits would start arbitrarily close to it yet reach a fixed distance $\epsilon$. Follow one such orbit and photograph it a fixed time $T$ before its first exit. That photograph lands close to ${\Gamma }_2$ (by local stability of ${\Gamma }_2$), so a genuine ${\Gamma }_2$-point $z^{\prime }$ sits next to it — and $z^{\prime }$ is inside the uniform basin of the collar around the limit point $\bar{x}$. The basin machinery then drags $z^{\prime }$‘s orbit into a thin tube ($\epsilon /4$) within time $T$, and continuous dependence says the photographed orbit — whose time-$T$ image is exactly the exit point — cannot be more than $\epsilon /2$ away. So the exit point is inside the $3\epsilon /4$-tube. But the exit point sits at distance exactly $\epsilon$. Contradiction.

Proof. Suppose, by way of contradiction, that ${\Gamma }_1$ is not stable. The hypothesis hFirstExit (discharged below in §5b) then provides a level ${\epsilon }_0>0$ and a single base sequence $\{x_i\}$ with $\mathrm{infDist}(x_i,{\Gamma }_1)\to 0$, together with — for every level $\epsilon \in (0,{\epsilon }_0]$ — a sequence of first-exit times. We deliberately do not fix the level yet; the freedom to shrink it is footnote 3’s whole point, and we will spend it in step 4.

Step 1 (the limit point). Since ${\Gamma }_1$ is compact, it is closed and bounded, so L-B (reduction_stability) applies to the base sequence: there is a subsequence $x_{\sigma (j)}\to \bar{x}$ with $\bar{x}\in {\Gamma }_1$.

Step 2 (local uniform boundedness). The hypothesis hLUB at the point $\bar{x}$ provides radii $\lambda >0$ and $m>0$ such that every orbit starting in $B_{\lambda }(\bar{x})$ remains in $B_m(\bar{x})$ for all forward time (:1323-1324).

Step 3 (the uniform basin). Form the widened collar $K:={\Gamma }_1\cap {\overline{B}}_{2(m+1)}(\bar{x})$ — compact, as the intersection of the compact ${\Gamma }_1$ with a closed ball, and nonempty since it contains $\bar{x}$. Theorem 2 applied to $K$ yields a single radius $\mu >0$, and for each tube level a single time. Note the dependency order: $\mu$ depends only on $\bar{x}$ and $m$, not on any escape level — this is what makes the next step legitimate.

Step 4 (fixing the level — footnote 3). Set $\epsilon :=\min ({\epsilon }_0,\mu /2)$, so that $0<\epsilon \le {\epsilon }_0$ and $\epsilon <\mu$. Take from hFirstExit the exit-time sequence $\{t_i\}$ for this level: eventually in $i$, the orbit of $x_i$ satisfies $\mathrm{infDist}({\phi }_s{x}_i,{\Gamma }_1)<\epsilon$ for all $s\in [0,t_i)$ and $\mathrm{infDist}({\phi }_{t_i}{x}_i,{\Gamma }_1)=\epsilon$, with $t_i\to \infty$. Had we fixed $\epsilon$ before $\mu$, this step would be circular; the paper’s footnote 3 (:1396-1398) is precisely the observation that the same base sequence exits at every smaller level, so the level may be chosen after the basin radius.

Step 5 (the remaining constants). From Theorem 2 take $T>0$ for the tube level $\epsilon /4$. From hContDep (discharged in §5b) at time $T$, center $\bar{x}$, ball radius $m+1$, and output tolerance $\epsilon /2$, take ${\delta }_{cd}>0$. Set $\delta :=\min (\min ({\delta }_{cd},(\mu -\epsilon )/2),1)$ — positive since $\epsilon \le \mu /2$ forces $\mu -\epsilon \ge \mu /2>0$. Finally, from hLSN at the point $\bar{x}$ with confinement radius $m$ and output tolerance $\delta$, take ${\delta }^{\prime }>0$ (:1325-1330).

Step 6 (one sufficiently late index). Along the subsequence, four things happen eventually, so they happen simultaneously at some index: writing $k:=\sigma (j)$ for that index, we have $\Vert x_k-\bar{x}\Vert <\lambda$ (convergence to $\bar{x}$), $\mathrm{infDist}(x_k,{\Gamma }_1)<{\delta }^{\prime }$ (the base sequence approaches ${\Gamma }_1$), $t_k>T$ (exit times tend to infinity), and the first-exit properties at level $\epsilon$ hold at $k$.

Step 7 (the photograph and its three addresses). Define $z:={\phi }_{t_k-T}(x_k)$ — the orbit of $x_k$ photographed exactly $T$ before its first exit. Since $0\le t_k-T<t_k$, the photograph is pre-exit, so $\mathrm{infDist}(z,{\Gamma }_1)<\epsilon$. Since $x_k\in B_{\lambda }(\bar{x})$, local uniform boundedness places the whole segment — hence $z$ — inside $B_m(\bar{x})$. And since $\mathrm{infDist}(x_k,{\Gamma }_1)<{\delta }^{\prime }$ while the segment up to time $t_k$ stays in $B_m(\bar{x})$, the hypothesis hLSN pushes the whole segment within $\delta$ of ${\Gamma }_2$; in particular $\mathrm{infDist}(z,{\Gamma }_2)<\delta$. This last step is the paper’s :1325-1343, and note what it consumed: local stability of ${\Gamma }_2$ and local uniform boundedness — no flow regularity, which is why it needed no interface.

Step 8 (the ${\Gamma }_2$-witness enters the basin). Since ${\Gamma }_2\supseteq {\Gamma }_1$ is nonempty, the bound $\mathrm{infDist}(z,{\Gamma }_2)<\delta$ produces a genuine point $z^{\prime }\in {\Gamma }_2$ with $\Vert z-z^{\prime }\Vert <\delta$. Two containments follow. First, since the point-to-set distance is $1$-Lipschitz,

$\mathrm{infDist}(z^{\prime },{\Gamma }_1)\le \mathrm{infDist}(z,{\Gamma }_1)+\Vert z-z^{\prime }\Vert <\epsilon +\delta \le \epsilon +\frac{\mu -\epsilon }{2}<\mu$

Second, by the triangle inequality and $\delta \le 1$,

$\Vert z^{\prime }-\bar{x}\Vert \le \Vert z^{\prime }-z\Vert +\Vert z-\bar{x}\Vert <\delta +m\le m+1$

(This is where the widened collar earns its keep: the paper takes the witness inside $B_m(\bar{x})$ directly at :1431, which its own bounds do not quite deliver; widening by one unit and capping $\delta \le 1$ repairs the constant without touching the argument.) Now Theorem 1 — the ball-nesting brick, applied with radius $m+1$ — converts “within $\mu$ of ${\Gamma }_1$ and within $m+1$ of $\bar{x}$” into “within $\mu$ of the compact collar $K$”: there is a center $x^{\ast }\in K$ with $\Vert z^{\prime }-x^{\ast }\Vert <\mu$.

Step 9 (confinement and transport). The point $z^{\prime }$ lies in $B_{\mu }(x^{\ast })\cap {\Gamma }_2$ with $x^{\ast }\in K$, so Theorem 2 confines its orbit from time $T$ onward: $\mathrm{infDist}({\phi }_T{z}^{\prime },{\Gamma }_1)<\epsilon /4$. Meanwhile hContDep — with $z\in B_m(\bar{x})\subseteq B_{m+1}(\bar{x})$ and $\Vert z-z^{\prime }\Vert <\delta \le {\delta }_{cd}$ — transports along the time-$T$ map: $\Vert {\phi }_{T}z-{\phi }_T{z}^{\prime }\Vert <\epsilon /2$.

Step 10 (the contradiction). By the flow law, ${\phi }_{t_k}{x}_k={\phi }_T\left({\phi }_{t_k-T}{x}_k\right)={\phi }_{T}z$. Therefore, using the Lipschitz property of the point-to-set distance once more,

$\mathrm{infDist}({\phi }_{t_k}{x}_k,{\Gamma }_1)\le \mathrm{infDist}({\phi }_T{z}^{\prime },{\Gamma }_1)+\Vert {\phi }_{T}z-{\phi }_T{z}^{\prime }\Vert <\frac{\epsilon }{4}+\frac{\epsilon }{2}<\epsilon$

But the first-exit property says $\mathrm{infDist}({\phi }_{t_k}{x}_k,{\Gamma }_1)=\epsilon$ exactly. A number cannot be both equal to $\epsilon$ and strictly below it, so the assumed instability is absurd, and ${\Gamma }_1$ is stable. $■$

The moral. Every quantifier in the theorem earns its place in one specific step: compactness of ${\Gamma }_1$ buys the limit point (step 1) and the collar (step 3); hLUB buys the bounded stage on which everything happens (steps 2, 7); hLSN buys the bridge from “near ${\Gamma }_1$” to “near ${\Gamma }_2$” (step 7); hUSA buys the only genuinely dynamical confinement (step 9); and the first-exit structure buys the exact equality that the confinement contradicts (step 10). The proof is long but has no idea in it beyond “photograph the escape $T$ early, and show the camera never lies by more than $3\epsilon /4$.“

5b. The tightening seals, in full

The three flow-side facts the core theorem consumes were themselves proved the same evening. Their proofs are short enough to give completely.

contDep_of_flow (continuous dependence at a fixed time). We must produce, for a time $T$, a center $p$, a ball radius $r>0$ and a tolerance $\eta >0$, a $\delta >0$ such that any $z$ in $B_r(p)$ and any $z^{\prime }$ within $\delta$ of $z$ satisfy $\Vert {\phi }_{T}z-{\phi }_T{z}^{\prime }\Vert <\eta$. Since $E$ is finite-dimensional it is a proper metric space, so the closed ball ${\overline{B}}_{r+1}(p)$ is compact. The time-$T$ map ${\phi }_T$ is continuous, and a continuous map on a compact set is uniformly continuous there (Heine–Cantor); extract ${\delta }_0>0$ for the tolerance $\eta$ and set $\delta :=\min ({\delta }_0,1)$. If $z\in B_r(p)$ and $\Vert z-z^{\prime }\Vert <\delta$, then both $z$ and $z^{\prime }$ lie in ${\overline{B}}_{r+1}(p)$ — the second because $\Vert z^{\prime }-p\Vert \le \Vert z^{\prime }-z\Vert +\Vert z-p\Vert <1+r$ — so uniform continuity applies. $■$ The $+1$ widening and the $\delta \le 1$ cap are the same trick as step 8 above: pay one unit of radius to make a boundary case disappear.

exists_firstExitTime (the hitting time). Fix one trajectory: suppose $\mathrm{infDist}(x_0,{\Gamma }_1)<\epsilon$ at time zero and $\mathrm{infDist}({\phi }_{t_1}{x}_0,{\Gamma }_1)\ge \epsilon$ at some time $t_1\ge 0$. Write $g(s):=\mathrm{infDist}({\phi }_s{x}_0,{\Gamma }_1)$ — a continuous function of $s$, being the composition of the continuous orbit map with the $1$-Lipschitz point-to-set distance. Consider the hitting set $H:=[0,t_1]\cap \{s:\epsilon \le g(s)\}$. It is closed (an intersection of a closed interval with a sublevel-complement of a continuous function), nonempty (it contains $t_1$), and bounded below by $0$; hence its infimum $\tau :=\inf H$ exists and belongs to $H$, giving $g(\tau )\ge \epsilon$. For any $s\in [0,\tau )$ minimality forbids $s\in H$, so $g(s)<\epsilon$ — the orbit is strictly inside the tube before $\tau$. The case $\tau =0$ is impossible since $g(0)<\epsilon$ by hypothesis. Finally, approaching $\tau$ from the left through values $g(s)<\epsilon$ and using continuity, $g(\tau )\le \epsilon$; combined with $g(\tau )\ge \epsilon$ this forces the exact equality $g(\tau )=\epsilon$. $■$ This is the intermediate value theorem in its “first crossing” form, done by hand because we need the minimality, not just existence.

exists_uniform_tube_radius (bounded times cannot escape). Fix a time horizon $B$ and a tolerance $\eta >0$. The set $\{(s,z):\mathrm{infDist}({\phi }_{s}z,{\Gamma }_1)<\eta \}$ is open in $\mathbb{R}\times E$, by joint continuity of the flow. It contains the product $[0,B]\times {\Gamma }_1$: for $y\in {\Gamma }_1$ and $s\ge 0$, forward invariance keeps ${\phi }_{s}y\in {\Gamma }_1$, where the distance is zero. The product of the compact interval $[0,B]$ with the compact ${\Gamma }_1$ is compact, so the tube lemma provides open sets $u\supseteq [0,B]$ and $v\supseteq {\Gamma }_1$ with $u\times v$ still inside the open set; and a compact set inside an open set admits a $\delta$-thickening still inside it. That $\delta$ is the claim: any $z$ within $\delta$ of ${\Gamma }_1$ lies in $v$, so for every $s\in [0,B]$ the pair $(s,z)$ is in $u\times v$, whence $\mathrm{infDist}({\phi }_{s}z,{\Gamma }_1)<\eta$. $■$ No subsequences, no finite dimension — the tube lemma replaces the planned Heine–Cantor-on-a-product route outright.

firstExit_of_not_stableSet (the assembly). Assume ${\Gamma }_1$ is not stable. L-A (reduction_stability) yields ${\epsilon }_0>0$, a base sequence $\{x_i\}$ with $\mathrm{infDist}(x_i,{\Gamma }_1)\to 0$, and times $t_i^{\prime }$ with $\mathrm{infDist}({\phi }_{t_i^{\prime }}{x}_i,{\Gamma }_1)\ge {\epsilon }_0$. Fix any level $\epsilon \in (0,{\epsilon }_0]$. Eventually $\mathrm{infDist}(x_i,{\Gamma }_1)<\epsilon$, and on that tail the hitting-time theorem applies to each index (the orbit starts inside the $\epsilon$-tube and reaches $\ge {\epsilon }_0\ge \epsilon$ at $t_i^{\prime }$), producing first-exit times $t_i$ with the equality and pre-exit properties. It remains to show $t_i\to \infty$. Suppose not: then some bound $B$ is exceeded by no $t_i$ along a subsequence. Apply the tube-radius theorem with horizon $B$ and tolerance $\epsilon$ to get $\delta >0$; eventually $\mathrm{infDist}(x_i,{\Gamma }_1)<\delta$, and at an index where all three conditions meet, the exit point ${\phi }_{t_i}{x}_i$ — a point of the orbit at a time $t_i\le B$ from a start within $\delta$ of ${\Gamma }_1$ — satisfies $\mathrm{infDist}({\phi }_{t_i}{x}_i,{\Gamma }_1)<\epsilon$, contradicting the exit equality $=\epsilon$. Hence the exit times are unbounded, and since they are produced along the whole tail, they tend to infinity. $■$ Positive invariance of ${\Gamma }_1$ enters the whole L-C chain exactly once — inside the tube-radius theorem above — which is why the core theorem could drop it as a hypothesis.

6. The machine seal

#print axioms, verbatim from the per-file build (lake build Ctrllib.ReductionStabilityFinish, 2026-07-09 evening, post-integration; full project lake build green at 2658/2659 jobs, Built Ctrllib):

info: Ctrllib/ReductionStabilityFinish.lean:476:0: 'Ctrllib.infDist_subCollar_of_mem_inter' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/ReductionStabilityFinish.lean:477:0: 'Ctrllib.uniform_basin_of_uniformSemiAttractor' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/ReductionStabilityFinish.lean:478:0: 'Ctrllib.stableSet_of_uniformSemiAttractor' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/ReductionStabilityFinish.lean:479:0: 'Ctrllib.contDep_of_flow' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/ReductionStabilityFinish.lean:480:0: 'Ctrllib.exists_firstExitTime' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/ReductionStabilityFinish.lean:481:0: 'Ctrllib.exists_uniform_tube_radius' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/ReductionStabilityFinish.lean:482:0: 'Ctrllib.firstExit_of_not_stableSet' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/ReductionStabilityFinish.lean:483:0: 'Ctrllib.stableSet_of_uniformSemiAttractor_of_forwardInvariant' depends on axioms: [propext, Classical.choice, Quot.sound]

Nothing beyond {propext, Classical.choice, Quot.sound} on any of the eight; no sorryAx; zero sorry in the module. (Tightening-lane gotchas recorded for future modules: Ioo_mem_nhdsWithin_Iio-family names are now *_mem_nhdsLT; push_neg is deprecated in this toolchain — use push Not; omit [...] in must precede the doc comment; two whnf deterministic timeouts were avoided by building joint continuity from continuous_fst/continuous_snd and by naming the product-membership pair before exact.)

7. Scope, honestly (ponytail)

• Interfaced, not fully standalone: the public assembly’s conclusion StableSet ϕ Γ₁ rests on hUSA — one named, seal-routed external fact (EHM-2009 Lemma 2.5). The evening’s arc: boundary hStable (theorem-sized) → three named facts (the core seal) → hUSA alone (the tightening lanes, same evening). The interfaces ledger rows record each step.
• Statement deviation from the paper, on purpose: EHM’s Theorem 6 lists (i) relative asymptotic stability, (ii) hLSN, (iii) LUB, plus positive invariance and ${\Gamma }_2$ closedness. This module’s statement omits hAttr, hpi₁, and ${\Gamma }_2$-closedness because tonight’s proof never touches them — each is consumed inside a named interface’s future seal (recorded in §2). The paper-shaped assembly is the final rewire, after F3.
• One quantitative widening vs. the paper: at :1431 the paper takes the ${\Gamma }_2$-witness $z_k^{\prime }\in B_m(\bar{x})$ directly, but the witness only satisfies $\Vert z^{\prime }-\bar{x}\Vert <m+\delta$. We widen the collar to $2(m+1)$ and cap $\delta \le 1$ — same argument, airtight constants. The hcontDep ball is widened to $m+1$ accordingly.
• Sealed inline rather than interfaced (stronger than the handoff plan): the segment-approaches-${\Gamma }_2$ step — the planned third flow interface hSegΓ₂ — turned out to be pure logic from hLSN + hLUB (source :1325-1343); its tightening ticket closes with this module.
• The other two tightening tickets also closed same-evening (parallel lanes, integrated serially): hContDep by Heine–Cantor; hFirstExit by hitting-time infimum + the tube lemma — the latter replacing the planned Heine–Cantor-on-a-product route with a cleaner one needing no finite dimension. The core theorem is kept with its named hypotheses on purpose: it documents the paper’s proof structure and lets a future reader see exactly which flow facts the finish consumes.
• Identifier gotchas for future modules: the micro sign µ (U+00B5) is not a valid Lean identifier character — use Greek μ (U+03BC); Finset inf'/sup' comparison lemmas need the explicit Mathlib.Data.Finset.Lattice.Fold import; Finset.lt_inf'_iff takes the nonemptiness proof as an explicit argument.