Forward-Orbit Stability for Discrete Systems in Lean

Begin with a moving reference orbit

Let \(f(x)=x+3\) on the real line. Start one trajectory at \(p=10\) and a nearby trajectory at \(x=10.2\).

For every natural number \(n\),

The reference point is not fixed: \(f(10)=13\). Nevertheless, every nearby trajectory remains exactly as close to the reference trajectory as it was at time zero. This example refutes any universal identification of orbit stability with fixed-point stability.

The calculation exhibits a forward-stable reference orbit that is not a fixed point. It does not establish attraction, robustness under changing the map, or a classification of all stable systems.

The interface decision

The module makes four choices explicit:

1. The reference object is a point together with its entire forward orbit.
2. Time is indexed by \(\mathbb N\), so time zero is included and no inverse map is assumed.
3. The primary definition is uniform-space equicontinuity of the iterate family.
4. Fixedness is an additional conjunct, not a consequence of orbit stability.

The core definition is

def IsForwardStableAt [UniformSpace X]
    (f : X → X) (p : X) : Prop :=
  EquicontinuousAt (fun n : ℕ ↦ f^[n]) p

Here f^[n] is the \(n\)-fold function iterate. EquicontinuousAt requires one neighborhood of p that works simultaneously for every member of the family indexed by n.

The fixed-point specialization is separate:

def IsLyapunovStableFixedPoint [UniformSpace X]
    (f : X → X) (p : X) : Prop :=
  IsFixedPt f p ∧ IsForwardStableAt f p

IsFixedPt f p means f p = p. The conjunction records two independent facts: the reference orbit is stationary, and nearby forward orbits remain close to it.

theorem isForwardStableAt_iff [UniformSpace X] :\n    IsForwardStableAt f p ↔\n      ∀ U ∈ 𝓤 X, ∀ᶠ x in nhds p, ∀ n : ℕ,\n        (f^[n] p, f^[n] x) ∈ U

The metric theorem

In a pseudo-metric space, the definition becomes

This is isForwardStableAt_iff_dist. A pseudo-metric is sufficient because the proof uses distances but never needs distinct points to have positive distance.

theorem isForwardStableAt_iff_dist [PseudoMetricSpace X] :\n    IsForwardStableAt f p ↔\n      ∀ ε > 0, ∃ δ > 0, ∀ x, dist x p < δ →\n        ∀ n : ℕ, dist (f^[n] p) (f^[n] x) < ε

At a fixed point, Function.iterate_fixed rewrites \(f^n(p)\) to \(p\). isLyapunovStableFixedPoint_iff_dist therefore yields the usual stationary form

Both directions retain IsFixedPt f p. The distance estimate at time zero cannot manufacture fixedness.

Consequences and examples

The iterate at index one is f, so IsForwardStableAt.continuousAt extracts ordinary one-step continuity at the reference point. This implication is one-way; the source never claims that one-step continuity controls every iterate uniformly.

If \(f\) is nonexpansive,

then Mathlib’s LipschitzWith.iterate gives \(d(f^n(x),f^n(y))\le d(x,y)\) for every \(n\). Taking \(\delta=\varepsilon\) proves isForwardStableAt_of_lipschitzWith_one.

The wrapper isLyapunovStableFixedPoint_of_lipschitzWith_one adds an explicit fixed-point hypothesis. The endpoint examples are isForwardStableAt_id, isForwardStableAt_add_const, forwardStableAt_add_const_not_fixed, and isLyapunovStableFixedPoint_const. Identity and the constant map supply fixed points; nonzero translation supplies a stable moving orbit.

Declaration-complete source map

The frozen source contains twelve public declarations:

Six #print axioms commands audit the central equivalences, consequence, and examples. Every report is exactly [propext, Classical.choice, Quot.sound]; none contains sorryAx.

Reproduce the project check

This is a full project check using the pinned Lean and Mathlib dependencies. It may require substantial disk space and build time.

git clone https://github.com/tdj28/nonlinear-dynamics-lean.git
cd nonlinear-dynamics-lean/formalization
lake env lean -DwarningAsError=true \
  NonlinearDynamics/Deterministic/Discrete/Stability.lean

lake env lean selects the project environment. -DwarningAsError=true rejects warnings. The command is portable across macOS and Linux once the pinned dependencies are installed. The paired Forward-Orbit and Fixed-Point Stability Deep Dive also supplies a small standalone tutorial importing only Std. The Forward Stability glossary chapter gives a shorter first pass.

Exact nonclaims

The module proves no attraction result: translated trajectories retain their gap rather than converging. It proves no asymptotic or exponential stability, invariant-set stability, basin theorem, Lyapunov-function criterion, two-sided-time result, structural stability, robustness under perturbing f, or stable-manifold theorem. It also does not claim that continuity implies forward stability.

These are interface boundaries. Attraction needs a distance-to-target limit or comparable neighborhood condition. Two-sided time needs invertibility or a \(\mathbb Z\)-action. Perturbation stability compares different maps, whereas IsForwardStableAt fixes one map and varies only the initial condition.

The later Lyapunov Functions Research Note supplies a scalar-certificate criterion while preserving this module’s separation between stability and attraction. The Conjugacies and Semiconjugacies Research Note explains why topology alone does not automatically transport this uniform-space forward-stability predicate.

References

1. Ethan Akin, “On Chain Continuity,” Discrete and Continuous Dynamical Systems 2(1), 111–120 (1996), doi:10.3934/dcds.1996.2.111.
2. Saber Elaydi and H. R. Farran, “On Variation of Equicontinuity in Dynamical Systems,” Bulletin of the Australian Mathematical Society 42(3), 391–397 (1990), doi:10.1017/S0004972700028550.
3. J. P. LaSalle, “Difference Equations and Discrete Semidynamical Systems,” Chapter 1 of The Stability of Dynamical Systems, SIAM CBMS 25 (1976), doi:10.1137/1.9781611970432.ch1.
4. Mathlib, Topology.UniformSpace.Equicontinuity, pinned revision 81a5d257.
5. Mathlib, Topology.MetricSpace.Equicontinuity, pinned revision 81a5d257.