v1.107 — Lyapunov exponential convergence: the deferred 'trajectory ⇒ converges' step, discharged#246
Merged
Merged
Conversation
… step discharged P2 final slice. proofs/lean/LyapunovConvergence.lean closes "trajectory ⇒ converges" for the exponential Lyapunov certificate — the step EVERY prior Lyapunov file deferred to LaSalle (absent from Mathlib) — WITHOUT LaSalle and WITHOUT the ODE flow API, by the integrating-factor argument: intfactor_antitone w(t)=v(t)·exp(γt) has deriv ≤ 0 (v'≤−γv) ⇒ antitone exp_decay_bound ⇒ v(t) ≤ v(0)·exp(−γt) for t ≥ 0 tendsto_zero_of_diff_ineq ⇒ 0 ≤ v ≤ v(0)exp(−γt) → 0 squeezes v(t) → 0 Completes the exponential Lyapunov chain: algebraic strict inequality (v1.105) → real-controller constants + rate γ≈0.056 (v1.106) → decay + convergence (v1.107). Remaining modelling assumption (v differentiable along the flow with deriv = V̇) is an explicit hypothesis — the honest interface to the vector-field certificates. No sorry, no axiom. FV-FALCON-LYAP-004 (status implemented — gated by lean.yml; local Lean kernel-check disk-blocked this cycle, so the gate is the verifying oracle). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…f_forall name lean.yml surfaced two blind-write issues (local kernel-check disk-blocked): - exp_decay_bound: Antitone-application left the lambda unreduced, so `rw` couldn't find `γ*0`; use `simp only` (beta-reduces then simplifies). - tendsto_zero_of_diff_ineq: `Filter.eventually_of_forall` was renamed to `Filter.Eventually.of_forall` in Mathlib v4.29.1. intfactor_antitone (the HasDerivAt core) compiled clean on the first run. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…proofs) //proofs/lean:lyapunov_convergence_test PASSED. The deferred trajectory⇒converges step is machine-checked for the exponential Lyapunov certificate. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
P2 final slice — closing the deferred dynamic step
Every prior Lyapunov file (
GeometricLyapunov,PositionLyapunov,StrictLyapunov) proves a differential inequality and defers "trajectory ⇒ converges" to LaSalle, which Mathlib lacks.proofs/lean/LyapunovConvergence.leandischarges it for the exponential (strict, negative-definite) formV̇ ≤ −γV— the form v1.105 proved algebraically and v1.106 confirmed on the real relay-geo controller (γ≈0.056) — without LaSalle and without the ODE flow API, by the classical integrating-factor argument:intfactor_antitonew(t)=v(t)·exp(γt)hasderiv ≤ 0(sincev'≤−γv) ⇒wantitoneexp_decay_boundv(t) ≤ v(0)·exp(−γt)fort ≥ 0tendsto_zero_of_diff_ineq0 ≤ v(t) ≤ v(0)exp(−γt) → 0squeezesv(t) → 0ast→∞All in Mathlib's calculus API (
deriv,Real.exp,antitone_of_deriv_nonpos,squeeze_zero'). Nosorry, no axiom.This completes the exponential Lyapunov chain end-to-end: algebraic strict inequality (v1.105) → real-controller constants + concrete rate (v1.106) → decay + convergence (v1.107).
Remaining modelling assumption: that the scalar
v(t)=V(state(t))is differentiable along the flow withderiv v = V̇— an explicit hypothesis, the honest interface to the vector-field certificates (the flow's existence is Mathlib PicardLindelöf, a separate wiring step).Verification (honest)
Local Lean kernel-check remains disk-blocked this cycle (host disk full), so
lean.yml(bazel test //proofs/lean:all) is the verifying oracle. This slice is calculus-heavy (more Mathlib API surface than the algebraic fragment), so if CI surfaces a lemma-name mismatch I'll iterate on this PR.FV-FALCON-LYAP-004isimplemented, →verifiedonce the gate is green.🤖 Generated with Claude Code