reduction_stability

R5 hStable-discharge groundwork — L-B and L-A

Seal

Rung R5 · Status sealed — both theorems axiom-clean (#print axioms verbatim in 5. The machine seal), no sorryAx, no named interface hypotheses. These are the two lowest-risk pieces of the El-Hawwary–Maggiore Lemma-22 → Theorem-6 set-stability argument, banked standalone toward discharging the L4a hypothesis hStable : StableSet ϕ Γ₁.
Links: module index · interface ledger · consumes Reduction (L4a) (the StableSet predicate, the Flow conventions) · recon (~/Code/notes/ctrllib_r5_mathlib_recon.md) · source elhawwary2013reduction (no wiki page yet)

What this seals, in one paragraph

L4a’s reduction_asymptotic_stability ((/Code/vault/lean/Reduction.lean) :155) takes the EHM Appendix-A set-stability core as a named hypothesis hStable : StableSet ϕ Γ₁ (EHM Theorem 6, compact branch). R5 works toward proving that hypothesis from primitive inputs. The recon (/Code/notes/ctrllib_r5_mathlib_recon.md) sliced the hStable side into three rungs — L-B (Bolzano–Weierstrass wrapper), L-A (escape-sequence extraction from instability), L-C (the Lemma-22 assembly + Theorem-6 finish). This module seals L-B and L-A: the two that are pure Mathlib topology and pure logic respectively, each provable without the external EHM-2009 lemma that bites in L-C. Neither carries a sorry or a named interface; they are honest standalone lemmas. The module is (~/Code/vault/lean/ReductionStability.lean), build copy ~/lean/ctrllib/Ctrllib/ReductionStability.lean.

No SymPy pin: L-B and L-A are pure topology and pure logic with no numeric computation, so there is nothing for a symbolic machine-check to verify (sympy_pin: ""). This is deliberate, not an omission — unlike the algebraic rungs (DetGamma has a pin), a Bolzano–Weierstrass wrapper and a negation-unpacking have no numeric content to cross-check.

1. The mathematical objects

We work on a real normed space $E$ ([NormedAddCommGroup E] [NormedSpace ℝ E]), matching the L4a conventions. $\mathrm{infDist}(x,\Gamma )$ is the point-to-set distance Metric.infDist x Γ; the EHM ball $B_{\delta }(\Gamma )$ is the predicate $\mathrm{infDist}(x,\Gamma )<\delta$. The set-stability predicate is L4a’s

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

verbatim from (~/Code/vault/lean/Reduction.lean) :62. The flow is a Mathlib Flow ℝ E, application ${\phi }_{t}x$ written ϕ t x.

2. L-B — Bolzano–Weierstrass wrapper (proved)

Theorem (exists_subseq_tendsto_mem_of_infDist_tendsto_zero). Let $E$ be finite-dimensional, $\Gamma \subseteq E$ nonempty closed and bounded, and $\{x_i\}$ a sequence with $\mathrm{infDist}(x_i,\Gamma )\to 0$. Then some subsequence $x_{\phi (i)}\to \bar{x}\in \Gamma$.

$\text{[FiniteDimensional R E]}(h_{ne}:\Gamma .\mathrm{Nonempty})(h_{cl}:\mathrm{IsClosed}\Gamma )(h_{bd}:\mathrm{IsBounded}\Gamma )\Rightarrow \exists \bar{x}\in \Gamma ,\exists \phi ,\mathrm{StrictMono}\phi \wedge x\circ \phi \to \bar{x}.$

Proof idea. Because $\mathrm{infDist}(x_i,\Gamma )\to 0$, eventually $\mathrm{infDist}(x_i,\Gamma )<1$, so the tail of $\{x_i\}$ lies in the open $1$-thickening Metric.thickening 1 Γ, which is bounded since $\Gamma$ is. Bolzano–Weierstrass (tendsto_subseq_of_frequently_bounded) then extracts a strictly monotone $\phi$ with $x\circ \phi \to \bar{x}$. The limit lies in $\Gamma$: the two limits $\mathrm{infDist}(x_{\phi (i)},\Gamma )\to \mathrm{infDist}(\bar{x},\Gamma )$ (continuity of $\mathrm{infDist}(\cdot ,\Gamma )$ along the subsequence) and $\mathrm{infDist}(x_{\phi (i)},\Gamma )\to 0$ (a subsequence of a null sequence) force $\mathrm{infDist}(\bar{x},\Gamma )=0$ by uniqueness of limits, and $\Gamma$ closed gives $\bar{x}\in \Gamma$.

Why $\Gamma .\mathrm{Nonempty}$ is required, not cosmetic. In Mathlib $\mathrm{infDist}(x,\varnothing )=0$. So for empty $\Gamma$ the hypothesis $\mathrm{infDist}(x_i,\Gamma )\to 0$ holds vacuously while the conclusion $\exists \bar{x}\in \Gamma$ is false — the statement is simply untrue without nonemptiness. IsClosed.mem_iff_infDist_zero demands it too. In the application $\Gamma ={\Gamma }_1$ is the compact (hence nonempty) target set $\bar{\mathbf{z}}$, so the hypothesis is free.

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

lemma	file:line
Metric.tendsto_atTop (ε–N unfolding, as in Reduction.lean:127)	Topology/MetricSpace/Pseudo/Defs
Metric.mem_thickening_iff_infDist_lt	Topology/MetricSpace/Thickening.lean:145
Bornology.IsBounded.thickening	Topology/MetricSpace/Thickening.lean:172
tendsto_subseq_of_frequently_bounded	Topology/MetricSpace/Sequences.lean:29
FiniteDimensional.proper_real (the ProperSpace gate, priority-900 instance)	Analysis/Normed/Module/FiniteDimension.lean:532
Metric.continuous_infDist_pt	Topology/MetricSpace/HausdorffDistance.lean:673
StrictMono.tendsto_atTop ({φ : ℕ → ℕ})	Order/Filter/AtTopBot/Tendsto.lean:84
tendsto_nhds_unique	Topology/Separation/Hausdorff.lean:179
IsClosed.mem_iff_infDist_zero	Topology/MetricSpace/HausdorffDistance.lean:697
Metric.infDist_nonneg	Topology/MetricSpace/HausdorffDistance.lean:582

The [FiniteDimensional ℝ E] gate is what unlocks the whole family: proper_real is a priority-900 instance, so ProperSpace E and Bolzano–Weierstrass fire by typeclass resolution with no manual witness — exactly the recon’s linchpin.

3. L-A — escape sequence from instability (proved)

Theorem (escape_sequence_of_not_stableSet). From the negation of set-stability, extract an escape magnitude and two sequences:

$\neg \text{StableSet}\phi \Gamma \Rightarrow \exists \epsilon >0,\exists \{x_i\},\{t_i\},(\forall i,0\le t_i)\wedge \mathrm{infDist}(x_i,\Gamma )\to 0\wedge (\forall i,\epsilon \le \mathrm{infDist}({\phi }_{t_i}{x}_i,\Gamma )).$

Proof idea. Pure logic. Unfold StableSet and push_neg: the negation yields one $\epsilon >0$ such that for every $\delta >0$ there is an $x$ with $\mathrm{infDist}(x,\Gamma )<\delta$ and a $t\ge 0$ with $\epsilon \le \mathrm{infDist}({\phi }_{t}x,\Gamma )$ (push-neg turns $\neg (a<\epsilon )$ into $\epsilon \le a$). Instantiate $\delta :=1/(i+1)>0$ and choose the sequences $\{x_i\},\{t_i\}$ with their properties. Finally $\mathrm{infDist}(x_i,\Gamma )\to 0$ is a squeeze: $0\le \mathrm{infDist}(x_i,\Gamma )$ (Metric.infDist_nonneg) and $\mathrm{infDist}(x_i,\Gamma )<1/(i+1)$, with $1/(i+1)\to 0$.

This is the first-exit-time-free version: it delivers $\epsilon \le \mathrm{infDist}({\phi }_{t_i}{x}_i,\Gamma )$, not the equality $=\epsilon$ of the full Lemma 22. The $=\epsilon$ refinement needs the intermediate-value first-hitting-time construction, which the recon flags as an interface-cut candidate; that is L-C’s problem, deliberately not this lane’s.

Mathlib lemmas / tactics used:

lemma / tactic	file:line
push_neg, choose (core tactics)	—
tendsto_of_tendsto_of_tendsto_of_le_of_le (the squeeze)	Topology/Order/Basic.lean:230
tendsto_const_nhds	Topology/Basic
tendsto_one_div_add_atTop_nhds_zero_nat	Analysis/SpecificLimits/Basic.lean:69
Metric.infDist_nonneg	Topology/MetricSpace/HausdorffDistance.lean:582

4. How L-B and L-A feed the hStable discharge (L-C)

Lemma 22’s compact-branch reading (recon §4) is: instability of ${\Gamma }_1$ produces an escape $\epsilon$ and a sequence $\{x_i\}$ with $\mathrm{infDist}(x_i,{\Gamma }_1)\to 0$ but $\mathrm{infDist}({\phi }_{t_i}{x}_i,{\Gamma }_1)$ bounded away from $0$ by $\epsilon$ — that sequence is L-A’s output. When ${\Gamma }_1$ is compact the sequence is automatically bounded, so L-B hands back a subsequence $x_{\phi (i)}\to \bar{x}\in {\Gamma }_1$. L-C then forms the escape set $S=\{x\in B_{\epsilon }({\Gamma }_1):\exists t>0,\mathrm{infDist}({\phi }_{t}x,{\Gamma }_1)=\epsilon \}$ (closed via isClosed_le), lifts the neighbourhood of ${\Gamma }_1$ to a uniform tube (IsCompact.exists_cthickening_subset_open), and closes the contradiction with positive invariance ($S\cap {\Gamma }_1=\varnothing$) to conclude StableSet ϕ Γ₁. L-C is the long pole — it leans on an external El-Hawwary–Maggiore 2009 lemma not in the corpus (recon §5) — and is the second interface-cut candidate. R5 banks L-B and L-A first precisely because they seal cleanly on their own; the go/no-go on L-C is a separate call.

5. The machine seal

#print axioms on the two sealed theorems, verbatim from the per-file build (lake build Ctrllib.ReductionStability, 2026-07-09; the full project builds clean at 2658 jobs):

info: Ctrllib/ReductionStability.lean:111:0: 'Ctrllib.exists_subseq_tendsto_mem_of_infDist_tendsto_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Ctrllib/ReductionStability.lean:112:0: 'Ctrllib.escape_sequence_of_not_stableSet' depends on axioms: [propext, Classical.choice, Quot.sound]

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

6. Scope, honestly (ponytail)

• Proved outright: L-B (BW wrapper, thin glue over tendsto_subseq_of_frequently_bounded + IsClosed.mem_iff_infDist_zero) and L-A (negation-unpacking + reciprocal squeeze).
• Corrections vs. the recon sketch: squeeze_zero does not exist in this Mathlib pin — the squeeze is tendsto_of_tendsto_of_tendsto_of_le_of_le (Topology/Order/Basic.lean:230); the bounded-set step uses the open Bornology.IsBounded.thickening + strict-< membership Metric.mem_thickening_iff_infDist_lt rather than cthickening, matching the <1 eventual bound directly; L-B needs the extra hypothesis $\Gamma .\mathrm{Nonempty}$ (else false, since $\mathrm{infDist}(x,\varnothing )=0$); the binder x̄ was renamed xbar (a combining macron is not a valid Lean identifier token).
• Not built here: L-C (Lemma-22 assembly + Theorem-6 finish, the StableSet producer) and the first-exit-time $=\epsilon$ refinement — both flagged interface-cut candidates, out of this lane.