reduction_uniformization

R6 — EHM-2009 Lemma 2.5 (converse): the uniform semi-attractor from relative asymptotic stability

Seal

Rung R6 · Status sealed — all three theorems axiom-clean (#print axioms verbatim in 6. The machine seal), no sorryAx, and no interface hypothesis anywhere in the module. This module discharges hUSA — the single external core the whole R5 arc rested on. After the R6-c rewire, the reduction theorem reduction_asymptotic_stability_of_asymStableRelativeTo stands on EHM standing conditions alone: the interface ledger’s EHM chain (hStable → hLandsInΓ₁ → hUSA) is closed end-to-end.
Links: module index · interface ledger · consumes ReductionStabilityFinish (L-C) and ReductionAttraction (T8-D) · recon (~/Code/notes/ctrllib_r6_lemma25_recon.md) · source elhawwary2009reduction

What this seals, in one paragraph

EHM-2009 Lemma 2.5 (p. 5, §2.3) is the bridge the EHM-2013 Theorem-6 finish invokes to convert relative asymptotic stability into the uniform semi-attractor property — the formula labelled (A.1) in 2013 and eq. (18) in the 2009 twin (Appendix D, p. 21). The R5 seals took that bridge as the named hypothesis hUSA; the R6 recon verified the Lean predicate UniformSemiAttractorRelativeTo is a quantifier-for-quantifier transcription of eq. (18), so no adapter is needed. This module proves the bridge — the converse (“furthermore”) direction, the only direction the finish consumes — and rewires it into T8-D. The module is (~/Code/vault/lean/ReductionUniformization.lean), build copy ~/lean/ctrllib/Ctrllib/ReductionUniformization.lean.

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

⚠ Route deviation — read this first

The proof formalized here is NOT the paper’s Appendix-A proof. Decided by the user 2026-07-10 (recon §5 put the call); recorded loudly per the house provenance rule.

• The paper’s route (Route A, declined): Appendix A ¶2 proves the converse direction through prolongational limit sets $J^{+}$ (Ura), with Proposition 2.6 cited to Bhatia–Szegö 1970 (Thm II.4.3, Lemma V.1.10) without proof in the paper. Mathlib has none of that machinery (the sole “prolongation” hit in the tree is homological algebra), and the Bhatia–Szegö book is out of corpus. Formalizing this route is ≥4 rung-sized theorems.
• The route sealed here (Route B): the classical compactness-and-finite-subcover argument, valid in our setting — a proper space (from [FiniteDimensional ℝ E]) with the relative-stability predicates in their tube forms. It proves the identical conclusion UniformSemiAttractorRelativeTo.
• The bridge licensing the deviation is the paper’s own: the p. 4 Remark states that for compact sets, uniform semi-attractivity coincides with the uniform attractivity used in Lin–Sontag–Wang 1996 (the paper’s [33]), for which the compactness argument is the standard proof. Our sole consumer (T8-D, hence L-C) instantiates at compact ${\Gamma }_1$, exactly the regime where the two notions coincide.
• Tube-form note (recon §2 footnote): AttractiveRelativeTo transcribes EHM Def 2.1(ii) with the basin specialized to a uniform ${\delta }_a$-tube. For noncompact ${\Gamma }_1$ that is strictly stronger than the paper’s generic neighbourhood (whose width may pinch to zero at infinity — the same p. 4 Remark); for the compact application they coincide. Route B actively exploits the tube form: the uniform radius ${\delta }_a$ is what feeds $\mu$ below. This is why the module consumes neither LUBNear nor compactness of ${\Gamma }_1$ nor ${\Gamma }_1\ne \varnothing$ — hypotheses the paper’s statement carries.

1. The statement and its objects

Conventions as in reduction_stability_finish: real normed space $E$, Metric.infDist z Γ the point-to-set distance, $B_{\alpha }(S)$ = the predicate $\mathrm{infDist}(z,S)<\alpha$ (strict, per the paper’s p. 3 notation), flow application ${\phi }_{t}y$ = ϕ t y. The hypothesis-side predicates (all Reduction.lean, EHM Def 4):

$\text{StableRelativeTo}\phi {\Gamma }_1{\Gamma }_2:=\forall \epsilon >0\exists \delta >0\forall x\in {\Gamma }_2(\mathrm{infDist}(x,{\Gamma }_1)<\delta \Rightarrow \forall t\ge 0\mathrm{infDist}({\phi }_{t}x,{\Gamma }_1)<\epsilon )$

$\text{AttractiveRelativeTo}\phi {\Gamma }_1{\Gamma }_2:=\exists {\delta }_a>0\forall x\in {\Gamma }_2(\mathrm{infDist}(x,{\Gamma }_1)<{\delta }_a\Rightarrow \mathrm{infDist}({\phi }_{t}x,{\Gamma }_1)\stackrel{t\to \infty }{\to }0)$

and the conclusion (ReductionStabilityFinish.lean, EHM-2009 Def 2.1(iv) relativized per Def 2.2 — literally eq. (18)):

$\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 load-bearing quantifier is the placement of $T$: one time per tube level ${\epsilon }^{\prime }$, independent of the initial point in $B_{\mu }(x)\cap {\Gamma }_2$. Pointwise attraction gives each initial point its own capture time; uniformization over the ball is precisely what compactness buys.

2. Theorem 1 — R6-a, the capture brick (exists_captureTime_ball, sealed)

$\mathrm{infDist}({\phi }_{t}y,{\Gamma }_1)\stackrel{t\to \infty }{\to }0,{\delta }_s>0\Rightarrow \exists T>0\exists r>0\forall z(\Vert z-y\Vert <r\Rightarrow \mathrm{infDist}({\phi }_{T}z,{\Gamma }_1)<{\delta }_s)$

One orbit drawn to ${\Gamma }_1$ yields a strictly positive capture time $T$ and a capture ball $B_r(y)$ of initial points all landing strictly inside the ${\delta }_s$-tube at that shared time.

Proof. Write $g(t)=\mathrm{infDist}({\phi }_{t}y,{\Gamma }_1)$. Since $g\to 0$ and ${\delta }_s>0$, the set of times with $g(t)<{\delta }_s$ is eventual in the atTop filter; so is the set of times $t>0$; a filter point satisfying both is a time $T>0$ with $g(T)<{\delta }_s$ (Tendsto.eventually_lt_const, eventually_gt_atTop). Now freeze $T$ and consider the time-$T$ tube function $z\mapsto \mathrm{infDist}({\phi }_{T}z,{\Gamma }_1)$. It is continuous: the fixed-time flow map ${\phi }_T$ is continuous (Flow.continuous_toFun) and the distance-to-set function is continuous (Metric.continuous_infDist_pt, indeed 1-Lipschitz). Its strict ${\delta }_s$-sublevel set is therefore open (isOpen_lt) and contains $y$; an open set in a metric space contains a ball around each of its points (Metric.isOpen_iff), giving $r>0$ with $B_r(y)$ inside the sublevel set. $■$

Why $T$ is strict. Eq. (18) demands $\exists T>0$ strict, and R6-c’s forward-invariance application consumes $0\le T$; taking the tail intersection with $t>0$ costs nothing and avoids an adapter.

3. Theorem 2 — R6-b, the uniformization (uniformSemiAttractor_of_asymStableRelativeTo, sealed)

$[E\text{fin. dim.}],{\Gamma }_2\text{closed},{\Gamma }_1\subseteq {\Gamma }_2,\phi \text{-forward-invariant }{\Gamma }_2,\text{StableRelativeTo},\text{AttractiveRelativeTo}\Rightarrow \text{UniformSemiAttractorRelativeTo}$

Proof. Fix $x\in {\Gamma }_1$. Let ${\delta }_a$ be the tube radius of relative attractivity and set

$\mu :={\delta }_a/2$

This $\mu$ depends only on $x$ (indeed not even on $x$) — it is chosen before ${\epsilon }^{\prime }$, as the quantifier order demands. Now fix ${\epsilon }^{\prime }>0$ and let ${\delta }_s>0$ be the relative-stability radius at level ${\epsilon }^{\prime }$.

The compact slab. Let $K:={\overline{B}}_{\mu }(x)\cap {\Gamma }_2$. The closed ball is compact because a finite-dimensional normed space is proper (isCompact_closedBall), and ${\Gamma }_2$ is closed, so $K$ is compact (IsCompact.inter_right). Note $x\in K$: $x\in {\Gamma }_1\subseteq {\Gamma }_2$ and the ball is centred at $x$ — so $K\ne \varnothing$ always; no empty-case split is needed.

Every slab point is in the basin. For $y\in K$: since $x\in {\Gamma }_1$ witnesses the point-to-set distance, $\mathrm{infDist}(y,{\Gamma }_1)\le \Vert y-x\Vert \le \mu <{\delta }_a$, and $y\in {\Gamma }_2$; relative attractivity applies, so $\mathrm{infDist}({\phi }_{t}y,{\Gamma }_1)\to 0$.

Finite subcover of capture balls. R6-a at level ${\delta }_s$ gives every $y\in K$ a capture time $T_y>0$ and capture ball $B_{r_y}(y)$. These balls are neighbourhoods of their centres covering $K$; compactness extracts a finite $F\subseteq K$ with $K\subseteq {\bigcup }_{w\in F}{B}_{r_w}(w)$ (IsCompact.elim_nhds_subcover). $F$ is nonempty because $x\in K$. Set

$T:=1+{\max }_{w\in F}{T}_w$

which is strictly positive (Finset sup' over the nonempty $F$; each $T_w>0$).

The tail. Take any $y$ with $\Vert y-x\Vert <\mu$ and $y\in {\Gamma }_2$, and any $t\ge T$. Then $y\in K$, so $y\in B_{r_w}(w)$ for some $w\in F$, and the capture brick gives

$\mathrm{infDist}({\phi }_{T_w}y,{\Gamma }_1)<{\delta }_s$

The capture point stays admissible: ${\phi }_{T_w}y\in {\Gamma }_2$ by forward invariance of ${\Gamma }_2$ (here is the one place hpi₂ is consumed; $T_w\ge 0$). The flow semigroup law rewrites ${\phi }_{t}y={\phi }_{t-T_w}({\phi }_{T_w}y)$ with $t-T_w\ge T-T_w\ge 1>0$ (Flow.map_add; the $+1$ in $T$ makes the tail arithmetic a one-line linarith). Relative stability at level ${\epsilon }^{\prime }$, applied to the capture point (in ${\Gamma }_2$, strictly inside the ${\delta }_s$-tube), bounds the entire remaining tail:

$\mathrm{infDist}({\phi }_{t-T_w}({\phi }_{T_w}y),{\Gamma }_1)<{\epsilon }^{\prime }$

which is the claim. $■$

Hypothesis accounting. hΓ₂closed → slab compactness only. hsub → $x\in K$ only. hpi₂ → the capture point’s ${\Gamma }_2$-membership only. Stability and attractivity are consumed exactly once each, in their tube forms. Nothing else enters — no LUBNear, no compactness of ${\Gamma }_1$, no ${\Gamma }_1\ne \varnothing$ (the basin bound uses $x$ itself as witness, never a nonemptiness axiom).

4. Theorem 3 — R6-c, the rewire (reduction_asymptotic_stability_of_asymStableRelativeTo, sealed)

T8-D (reduction_attraction) already carried hStabRel and hAttrRel in its signature — L-C’s row deliberately never consumed the stability half, and the recon (§2) located the gap as hypothesis-side and benign. The rewire therefore only threads one new primitive: hpi₂ : IsForwardInvariant ϕ.toFun Γ₂, which is paper-faithful — EHM Theorem 6’s standing setup is two closed positively invariant sets — and was simply unthreaded until now. The proof term is one application: T8-D with its hUSA slot filled by R6-b.

$\text{reduction\_asymptotic\_stability\_of\_asymStableRelativeTo}=\text{T8-D}[\text{hUSA}:=\text{R6-b}(\text{hΓ₂closed},\text{hsub},\text{hpi₂},\text{hStabRel},\text{hAttrRel})]$

Neither L-C nor T8-D is edited — they are consumed. The composed reduction theorem’s signature now reads: compact nonempty ${\Gamma }_1\subseteq {\Gamma }_2$ closed, both forward invariant, LUBNear, the Def-3 locality conditions (hLSN, hLAN), and relative asymptotic stability (both halves) — every hypothesis a standing condition of EHM Theorems 6/8/10; no interface hypothesis remains.

5. What the defense should know

• The direction proved is the converse (“furthermore”) direction only — semi-asymptotic stability relative to ${\Gamma }_2$ ⟹ uniform semi-attractor — because that is the only direction the Theorem-6 finish consumes (2009 Appendix D, p. 21: the derivation of eq. (18)). The forward direction (uniform semi-attractor ⟹ stability) is the content of the already-sealed L-C core and was never an R6 obligation (recon §3 ¶1: the paper’s own forward proof is structurally our sealed L-A + L-B).
• Where the paper’s extra hypotheses went. Lemma 2.5 as stated carries local uniform boundedness; that rider powers the $J^{+}$-machinery route for possibly-noncompact $\Gamma$. In the tube-form/proper-space setting the finite-subcover argument replaces it outright, so the Lean statement is cleaner than the paper’s — fewer hypotheses, identical conclusion formula — at the price of the route deviation documented above, licensed for compact applications by the paper’s own p. 4 Remark.
• Trust boundary after R6: the EHM reduction chain is interface-free. What remains open across the library is unrelated to this chain: IsSolutionTo (flow existence), hreal/hfield (moving-metric calculus), hsvd, and the cascade modelling inputs hsand/hdi — see interfaces.

6. The machine seal

Full lake build green (2661 jobs) with the module imported at the root; axiom prints verbatim:

'Ctrllib.exists_captureTime_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.uniformSemiAttractor_of_asymStableRelativeTo' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.reduction_asymptotic_stability_of_asymStableRelativeTo' depends on axioms: [propext, Classical.choice, Quot.sound]

No sorryAx, no interface hypotheses; interfaces_assumed: [] and the interfaces hUSA row flips to discharged with this seal.