Conversation
…ility critique update (run35) Task 5 (Proof Assistance): Add ExpoDeadzone.lean — formal specification and proofs for the combined expo(deadzone(v, dz), e) RC input pipeline. 8 theorems proved (0 sorry, lake build passes): - expodz_in_dz: inside-deadzone input → exactly 0 - expodz_in_range: output always ∈ [-1, 1] (unconditional) - expodz_zero: zero input → zero output for dz ≥ 0 - expodz_at_one / expodz_at_neg_one: ±1 are fixed points for dz ∈ [0, 1) - expodz_e0: e=0 (linear expo) reduces to pure deadzone - expodz_cubic: e=1 (full cubic expo) gives (deadzone v dz)³ - expodz_no_dz: dz=0 recovers exactly expoRat (no-deadzone degeneration) Proofs compose expo_* and deadzone_* theorems from prior Lean files, demonstrating compositional verification of the two-stage RC pipeline. Also registers ExpoDeadzone + MedianFilter + SuperExpo in FVSquad.lean. Task 7 (Proof Utility Critique): Update CRITIQUE.md to reflect current state: - 15 targets, 172 theorems, 166 proved, 6 sorry (WrapAngle wrapRat only) - Add SuperExpo, MedianFilter, ExpoDeadzone rows to proved-theorems table - Update gaps: add expodz_odd as next high-priority target - Add positive findings #10-12 (MedianFilter spike rejection, superexpo denom-positive safety, expo+deadzone composition correctness) - Update Known Sorry-Guarded section (14 files, 0 sorry except WrapAngle) > ✅ Proofs verified: lake build passed with Lean 4.29.0. 0 sorry in new file. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…-95ee7ddf980126c8
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.
🔬 Lean Squad — automated formal verification run 35.
Summary
Two tasks completed this run:
Task 5 — Proof Assistance: ExpoDeadzone.lean
New file:
formal-verification/lean/FVSquad/ExpoDeadzone.leanFormal specification and proofs for the combined
expo(deadzone(v, dz), e)RC inputprocessing pipeline. In PX4, stick input first passes through a deadzone (to ignore
drift near centre), then through an exponential curve (for sensitivity shaping).
8 theorems proved, 0 sorry:
expodz_in_dzexpodz_in_rangeexpodz_zeroexpodz_at_one/expodz_at_neg_oneexpodz_e0expodz_cubicexpodz_no_dzexpoRatProofs compose
expo_*anddeadzone_*theorems from prior files. Also registersMedianFilter,SuperExpo, andExpoDeadzoneinFVSquad.lean(they were presentbut not imported in the root module).
Task 7 — Proof Utility Critique: CRITIQUE.md update
MedianFilter,SuperExpo, andExpoDeadzonerowsexpodz_odd(anti-symmetry) as next high-priority gap,removed outdated MedianFilter "write the spec" item (now done)
denom-positive safety, expo+deadzone composition correctness
Verification Status
18 jobs, no errors. Only pre-existing
sorrywarnings fromWrapAngle.lean(wrapRat, requires Mathlib floor).Files Changed
formal-verification/lean/FVSquad/ExpoDeadzone.lean— new (8 theorems)formal-verification/lean/FVSquad.lean— add imports for MedianFilter, SuperExpo, ExpoDeadzoneformal-verification/CRITIQUE.md— proof utility critique updateformal-verification/TARGETS.md— add ExpoDeadzone as target [Lean Squad] feat(formal-verification): wrap_pi Lean spec + Critique update (run11) #15