v1.105 — strict Lyapunov exponential certificate + CI-gate the orphaned Lean proofs#244
Merged
Conversation
…ate the orphaned Lean proofs P2 first slice (closed-loop Lyapunov). Two advances: 1. proofs/lean/StrictLyapunov.lean — the negative-DEFINITE upgrade of the semidefinite V̇ ≤ 0 core. GeometricLyapunov/PositionLyapunov prove V̇ ≤ 0 and DEFER "trajectory ⇒ converges" to LaSalle (absent from Mathlib). This follows Lee 2010 Prop. 2: a cross-term Lyapunov makes V̇ negative-definite (Sylvester 2×2 criterion) and assembles c_hi·V̇ ≤ −c_D·V — which is exactly the GRÖNWALL hypothesis, and Mathlib DOES have flows/Grönwall. So the deferred gap shrinks from "formalize LaSalle" (multi-year) to "apply Grönwall" (exists). Theorems: quad_complete, quad_form_nonneg, quad_radial_lower/upper, exp_decay_inequality, strict_lyapunov_exp_decay, + a non-vacuity witness (concrete gains ⇒ γ=½). No sorry, no axiom. 2. .github/workflows/lean.yml — the proofs/lean/ Lean proofs were authored + locally kernel-verified but NEVER gated in any CI workflow (same orphaned- proof gap that left the Kani control/estimator harnesses unenforced until v1.104). New lean.yml runs `bazel test //proofs/lean:all` (Lean 4.29.1 + Mathlib v4.29.1) as a required check — all six proofs re-checked per PR. Also: README toolchain pin corrected 4.27.0 → 4.29.1 (matches MODULE.bazel) + PositionLyapunov/StrictLyapunov table rows; FV-FALCON-LYAP-002 rivet artifact (status implemented — moves to verified once lean.yml is green; local kernel-check was unavailable this cycle, Mathlib's multi-GB build did not fit host disk, so the lean.yml gate is the verifying oracle). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
First lean.yml run failed "No space left on device" extracting the Lean 4.29.1 toolchain: ubuntu-latest's ~14 GB free could not hold the toolchain + Mathlib oleans + the transitive rules_* toolchain graph the sibling checkouts pull in. Free the ~25 GB of preinstalled SDKs (dotnet/android/ghc/CodeQL/…) this job never uses, via plain rm (no third-party action — minimal CI surface). Infra-only; the proofs were never reached. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…proofs pass) The lean.yml gate ran `bazel test //proofs/lean:all` green: "Executed 6 out of 6 tests: 6 tests pass", incl strict_lyapunov_test. StrictLyapunov.lean is kernel-checked at Lean 4.29.1 / Mathlib v4.29.1. 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 first slice — closed-loop Lyapunov
Two advances, one closing the deferred dynamic step, one closing an orphaned-proof gap.
1.
proofs/lean/StrictLyapunov.lean— the negative-definite upgradeGeometricLyapunov/PositionLyapunovprove the closed-loop derivative is negative semi-definite (V̇ ≤ 0) and defer "trajectory ⇒ converges" to LaSalle — which Mathlib does not have.This follows Lee 2010 Prop. 2: a cross-term-coupled Lyapunov function makes
V̇negative-definite (certified by Sylvester's 2×2 criterion) and assembles the exponential-decay inequalityc_hi·V̇ ≤ −c_D·V. That is exactly the Grönwall hypothesis — and Mathlib does have flows/Grönwall (arXiv:2602.13247). So the remaining deferred step shrinks from "formalize LaSalle" (multi-year) to "apply Grönwall to the flow".Theorems (all in the
ring/nlinarithfragment, nosorry, no axiom):quad_complete,quad_form_nonneg,quad_radial_lower/upper,exp_decay_inequality,strict_lyapunov_exp_decay, + a non-vacuity witness (concrete gains ⇒ rateγ=½).2.
.github/workflows/lean.yml— gate the orphaned Lean proofsThe
proofs/lean/proofs were authored + locally kernel-verified but never gated in any CI workflow — the same orphaned-proof gap that left the Kani control/estimator harnesses unenforced until v1.104. Newlean.ymlrunsbazel test //proofs/lean:all(Lean 4.29.1 + Mathlib v4.29.1) as a required check, re-checking all six proofs per PR.Also: README pin corrected
4.27.0 → 4.29.1(matchesMODULE.bazel);FV-FALCON-LYAP-002rivet artifact.Verification status (honest)
Local kernel-checking was unavailable this cycle — Mathlib's multi-GB build did not fit the host disk. The new
lean.ymlgate is the verifying oracle: this is the first run that kernel-checksStrictLyapunov.lean. The rivet artifact isimplemented, moving toverifiedoncelean.ymlis green on main. If CI surfaces a tactic or Mathlib-API issue, I'll iterate on this PR.🤖 Generated with Claude Code