Lean 4 Nonlinear Dynamics & Stability
Guide to formalizing dynamical systems, stability theory, and bifurcation in Lean 4.
Routing
- USE FOR: nonlinear dynamical systems, Lyapunov stability, bifurcation theory, catastrophe theory, control theory, phase-portrait analysis, attractor classification, and any deterministic system with state evolution over time in Lean 4.
- DO NOT USE FOR: stochastic dynamics (delegate to
@lean-math-stochastic); pure analysis / topology (delegate to @lean-math-analysis); optimization-only control problems (delegate to @lean-math-optimization); writing one specific proof (delegate to @lean-proof).
- TRIGGERS: Lyapunov, stability, bifurcation, cusp catastrophe, attractor, phase portrait, dynamical system, control theory, equilibrium.
Workflow
- Classify the system (Part 1) — discrete-time, continuous-time, gradient, conservative, controlled.
- Pick the appropriate technique below (Lyapunov, contraction, bifurcation-normal-form, catastrophe-classification).
- Handoff to
@lean-proof for the concrete proof; if it bottoms out in a derivative / measure step, handoff to @lean-math-analysis.
Recovery & STOP
- STOP if the proof depends on a manifold or smooth-structure API not in Mathlib at the current pin — escalate to
@lean-research.
- STOP if a stochastic perturbation enters the model — re-route to
@lean-math-stochastic; this skill covers only deterministic dynamics.
Handoffs
- Predecessors:
agent:gateway, skill:lean-proof (mid-proof stability goal), skill:lean-research (catastrophe-theory result survey).
- Successors:
skill:lean-proof (apply the dynamical pattern), skill:lean-proof-review (audit Lyapunov candidate), skill:lean-math-analysis (continuous-derivative or contraction reduction).
Detailed reference
Full encyclopaedia content (Parts 1 through 6) lives in
references/lean4-math-dynamical.md. Load that file
when authoring; the SKILL.md only carries the dispatch contract and
the high-frequency pitfalls / recipes (kept inline below).
| Part |
Topic |
Covers |
| Part 1 |
Dynamical Systems Taxonomy |
discrete-time, continuous-time, gradient, conservative, controlled |
| Part 2 |
Lyapunov Stability Theory |
candidate construction, positive-definiteness, LaSalle |
| Part 3 |
Bifurcation and Catastrophe Theory |
cusp / fold / pitchfork normal forms |
| Part 4 |
Phase Space Analysis |
phase portraits, equilibria classification |
| Part 5 |
Control Theory Connections |
Lyapunov-control, control-Lyapunov functions |
| Part 6 |
Nonlinear Methods Toolbox |
linearisation, normal-form reduction, numerical-continuation hints |
Part 7 — Research Council Integration
Consolidated into the single canonical routing matrix:
references/research-council-skill-map.md
(see the "Dynamical" section). When dispatching a question to a
council member, cite that table rather than restating the rows here.
Part 8 — IVT Sign-Change Pattern
Extracted to single canonical reference:
references/lean4-ivt-patterns.md.
That file owns the canonical incantation, the
asymmetric_three_roots_ivt walk-through, and the polynomial-continuity
prerequisite.
Part 9 — Common Pitfalls (Stability & Bifurcation)
| Pitfall |
Symptom |
Recovery |
| Lyapunov candidate not positive-definite |
V 0 = 0 proved, but V x > 0 for x ≠ 0 fails |
Add a quadratic-form witness (x^T Q x with Q PSD); check posDef_iff_eigenvalues_pos family |
Contraction map without [CompleteSpace α] |
ContractingWith.fixedPoint won't apply |
Add [CompleteSpace α] instance or restrict to a closed subset and use IsCompact.completeSpace |
| IVT sign-error in bifurcation diagram |
Existential ∃ c, f c = 0 won't close |
Re-check sign of f a and f b; see references/lean4-ivt-patterns.md for the canonical asymmetric_three_roots_ivt walk-through |
| Catastrophe normal form drifted from repository canon |
cusp / fold polynomial signs don't match expectations |
Compare against Mathlib.Analysis.SpecialFunctions.Pow.Real; there is no canonical catastrophe API in Mathlib — keep local definitions in the host repository's catastrophe namespace |
| Discrete- vs continuous-time confusion |
Tendsto with the wrong filter |
Discrete: atTop on ℕ; continuous: atTop on ℝ (often with a measure-preserving step) |
Spurious equilibrium from simp overreach |
f x = x "proved" by simplifying both sides to 0 |
Disable simp for the candidate equilibrium proof; use linear_combination or explicit substitution |
Cross-reference: repository stability tactics
- Host-repository Lyapunov modules — quadratic-form Lyapunov constructions for local cusp + phase-portrait models.
- Host-repository catastrophe modules — cusp-form polynomial bifurcation (the 3-real-roots case).
references/lean4-ivt-patterns.md — asymmetric_three_roots_ivt walk-through (canonical entry-point for sign-change existence).references/lean4-contraction-catalog.md — catalog of contraction-mapping templates (uses ContractingWith / LipschitzWith).
Part 10 — Banach Fixed-Point Recipe
The most common "I need a fixed point" pattern in this corpus:
-- Given a self-map f : α → α and a contraction constant K < 1:
example {α : Type*} [MetricSpace α] [CompleteSpace α]
(f : α → α) {K : NNReal} (hK : K < 1)
(hC : ContractingWith K f) :
∃! x, f x = x :=
⟨hC.fixedPoint, hC.fixedPoint_isFixedPt,
fun y hy => hC.fixedPoint_unique hy⟩
Project-relevant adaptations:
- Sub-Banach setting:
IsCompact.completeSpace lets you restrict to a closed ball when global completeness is unwieldy.
- Iteration bounds:
ContractingWith.aux_dist_le gives dist (f^[n] x) (fixedPoint) ≤ K^n * dist x (fixedPoint) / (1 - K).
- Existence-only (no uniqueness): Schauder fixed-point — not in Mathlib at the current pin; use
@lean-research to confirm before authoring.
See also
1---2name: lean-math-dynamical3description: USE FOR: nonlinear dynamical systems, Lyapunov stability, bifurcation theory, catastrophe theory, control theory, phase-portrait analysis, attractor classification, and any deterministic system with state evolution over time in Lean 4. DO NOT USE FOR: stochastic dynamics (use @lean-math-stochastic); pure analysis / topology (use @lean-math-analysis); optimization-only control problems (use @lean-math-optimization); writing one specific proof (use @lean-proof). TRIGGERS: Lyapunov, stability, bifurcation, cusp catastrophe, attractor, phase portrait, dynamical system, control theory, equilibrium.4---56# Lean 4 Nonlinear Dynamics & Stability78Guide to formalizing dynamical systems, stability theory, and bifurcation in Lean 4.910## Routing1112- **USE FOR:** nonlinear dynamical systems, Lyapunov stability, bifurcation theory, catastrophe theory, control theory, phase-portrait analysis, attractor classification, and any deterministic system with state evolution over time in Lean 4.13- **DO NOT USE FOR:** stochastic dynamics (delegate to `@lean-math-stochastic`); pure analysis / topology (delegate to `@lean-math-analysis`); optimization-only control problems (delegate to `@lean-math-optimization`); writing one specific proof (delegate to `@lean-proof`).14- **TRIGGERS:** Lyapunov, stability, bifurcation, cusp catastrophe, attractor, phase portrait, dynamical system, control theory, equilibrium.1516## Workflow17181. Classify the system (Part 1) — discrete-time, continuous-time, gradient, conservative, controlled.192. Pick the appropriate technique below (Lyapunov, contraction, bifurcation-normal-form, catastrophe-classification).203. Handoff to `@lean-proof` for the concrete proof; if it bottoms out in a derivative / measure step, handoff to `@lean-math-analysis`.2122## Recovery & STOP2324- STOP if the proof depends on a manifold or smooth-structure API not in Mathlib at the current pin — escalate to `@lean-research`.25- STOP if a stochastic perturbation enters the model — re-route to `@lean-math-stochastic`; this skill covers only deterministic dynamics.2627## Handoffs2829- **Predecessors:** `agent:gateway`, `skill:lean-proof` (mid-proof stability goal), `skill:lean-research` (catastrophe-theory result survey).30- **Successors:** `skill:lean-proof` (apply the dynamical pattern), `skill:lean-proof-review` (audit Lyapunov candidate), `skill:lean-math-analysis` (continuous-derivative or contraction reduction).3132## Detailed reference3334Full encyclopaedia content (Parts 1 through 6) lives in35[`references/lean4-math-dynamical.md`](../../references/lean4-math-dynamical.md). Load that file36when authoring; the SKILL.md only carries the dispatch contract and37the high-frequency pitfalls / recipes (kept inline below).3839| Part | Topic | Covers |40|---|---|---|41| Part 1 | Dynamical Systems Taxonomy | discrete-time, continuous-time, gradient, conservative, controlled |42| Part 2 | Lyapunov Stability Theory | candidate construction, positive-definiteness, LaSalle |43| Part 3 | Bifurcation and Catastrophe Theory | cusp / fold / pitchfork normal forms |44| Part 4 | Phase Space Analysis | phase portraits, equilibria classification |45| Part 5 | Control Theory Connections | Lyapunov-control, control-Lyapunov functions |46| Part 6 | Nonlinear Methods Toolbox | linearisation, normal-form reduction, numerical-continuation hints |4748## Part 7 — Research Council Integration4950Consolidated into the single canonical routing matrix:51[`references/research-council-skill-map.md`](../../references/research-council-skill-map.md)52(see the "Dynamical" section). When dispatching a question to a53council member, cite that table rather than restating the rows here.5455---5657## Part 8 — IVT Sign-Change Pattern5859Extracted to single canonical reference:60[`references/lean4-ivt-patterns.md`](../../references/lean4-ivt-patterns.md).61That file owns the canonical incantation, the62`asymmetric_three_roots_ivt` walk-through, and the polynomial-continuity63prerequisite.6465---6667## Part 9 — Common Pitfalls (Stability & Bifurcation)6869| Pitfall | Symptom | Recovery |70|---|---|---|71| Lyapunov candidate not positive-definite | `V 0 = 0` proved, but `V x > 0` for `x ≠ 0` fails | Add a quadratic-form witness (`x^T Q x` with `Q` PSD); check `posDef_iff_eigenvalues_pos` family |72| Contraction map without `[CompleteSpace α]` | `ContractingWith.fixedPoint` won't apply | Add `[CompleteSpace α]` instance or restrict to a closed subset and use `IsCompact.completeSpace` |73| IVT sign-error in bifurcation diagram | Existential `∃ c, f c = 0` won't close | Re-check sign of `f a` and `f b`; see `references/lean4-ivt-patterns.md` for the canonical `asymmetric_three_roots_ivt` walk-through |74| Catastrophe normal form drifted from repository canon | `cusp` / `fold` polynomial signs don't match expectations | Compare against `Mathlib.Analysis.SpecialFunctions.Pow.Real`; there is *no* canonical catastrophe API in Mathlib — keep local definitions in the host repository's catastrophe namespace |75| Discrete- vs continuous-time confusion | `Tendsto` with the wrong filter | Discrete: `atTop` on `ℕ`; continuous: `atTop` on `ℝ` (often with a measure-preserving step) |76| Spurious equilibrium from `simp` overreach | `f x = x` "proved" by simplifying both sides to `0` | Disable `simp` for the candidate equilibrium proof; use `linear_combination` or explicit substitution |7778### Cross-reference: repository stability tactics7980- Host-repository Lyapunov modules — quadratic-form Lyapunov constructions for local cusp + phase-portrait models.81- Host-repository catastrophe modules — cusp-form polynomial bifurcation (the 3-real-roots case).82- [`references/lean4-ivt-patterns.md`](../../references/lean4-ivt-patterns.md) — `asymmetric_three_roots_ivt` walk-through (canonical entry-point for sign-change existence).83- [`references/lean4-contraction-catalog.md`](../../references/lean4-contraction-catalog.md) — catalog of contraction-mapping templates (uses `ContractingWith` / `LipschitzWith`).8485---8687## Part 10 — Banach Fixed-Point Recipe8889The most common "I need a fixed point" pattern in this corpus:9091```lean92-- Given a self-map f : α → α and a contraction constant K < 1:93example {α : Type*} [MetricSpace α] [CompleteSpace α]94 (f : α → α) {K : NNReal} (hK : K < 1)95 (hC : ContractingWith K f) :96 ∃! x, f x = x :=97 ⟨hC.fixedPoint, hC.fixedPoint_isFixedPt,98 fun y hy => hC.fixedPoint_unique hy⟩99```100101Project-relevant adaptations:102103- **Sub-Banach setting:** `IsCompact.completeSpace` lets you restrict to a closed ball when global completeness is unwieldy.104- **Iteration bounds:** `ContractingWith.aux_dist_le` gives `dist (f^[n] x) (fixedPoint) ≤ K^n * dist x (fixedPoint) / (1 - K)`.105- **Existence-only (no uniqueness):** Schauder fixed-point — *not* in Mathlib at the current pin; use `@lean-research` to confirm before authoring.106107---108109## See also110111- [`../../references/lean4-math-dynamical.md`](../../references/lean4-math-dynamical.md) — Nonlinear Dynamics Encyclopaedia (full encyclopaedia, extracted from this skill)112- [`../../templates/Template_Dynamics.md`](../../templates/Template_Dynamics.md) — Template: Lyapunov / Markov / contraction mappings113- [`../../references/lean4-proof-strategy.md`](../../references/lean4-proof-strategy.md) — Proof strategy: real-valued contraction patterns
r-irbe