[Lean Squad] feat(formal-verification): AlphaFilter Lean spec + Deadzone sorry elimination

[github-actions]

Overview

This PR delivers two completed tasks and contributes to a third:

• Task 5 (Proof Assistance): Eliminates the 2 remaining sorry in Deadzone.lean — the range-bound theorems deadzone_le_one and deadzone_ge_neg_one are now fully proved. Deadzone.lean now has 12 proved theorems and 0 sorry.

• Task 2 (Informal Spec): Adds a precise informal specification for AlphaFilter::update documenting pre/postconditions, no-overshoot safety property, and open questions for maintainers.

• Task 4+5 (Lean Spec + Proofs): Adds AlphaFilter.lean with 9 proved theorems and 3 documented sorry.

---

Changes

formal-verification/lean/FVSquad/Deadzone.lean

Proves the two theorems that previously required sorry:

deadzone_le_one (negative branch): When x < 0 and |x| > dz, the output is (x + dz)/(1 − dz) < 0 ≤ 1. Key steps: |x| = −x via Rat.abs_of_nonpos, then x < −dz via Rat.neg_lt_neg_iff, then show x + dz < 0 using the same pattern as deadzone_neg.

deadzone_ge_neg_one: Full case split: (1) in-deadzone → output = 0 ≥ −1; (2) positive branch → output > 0 ≥ −1; (3) negative branch → uses −(1−dz) ≤ x+dz (from −1 ≤ x, add dz) and the calc chain −1 = −(1−dz)·(1−dz)⁻¹ ≤ (x+dz)·(1−dz)⁻¹.

formal-verification/specs/alphafilter_informal.md (new)

Informal specification for AlphaFilter::updateCalculation:

• Core update: new = (1−α)·old + α·sample (convex blend)
• No-overshoot safety property: min(state, sample) ≤ new_state ≤ max(state, sample)
• Fixed point, boundary cases (α=0, α=1), multi-step convergence formula
• Concrete examples table, edge cases, open questions for maintainers

formal-verification/lean/FVSquad/AlphaFilter.lean (new)

Lean 4 model over Rat:

Proved (9 theorems):

• alphaUpdate_fixed: sample = state → no change
• alphaUpdate_alpha_zero: α=0 → state frozen
• alphaUpdate_alpha_one: α=1 → state = sample immediately
• alphaUpdate_le_sample / alphaUpdate_ge_state: no-overshoot upper/lower bound (upward case)
• alphaUpdate_no_overshoot_up: combined state ≤ new_state ≤ sample
• alphaUpdate_le_state: upper bound downward case (new_state ≤ state)
• alphaUpdate_mono_sample: monotone in sample input
• alphaIterate_formula (base case): state₀ = target + (state₀ − target) · (1−α)⁰

3 sorry remain (documented):

• alphaUpdate_ge_sample: needs multiply-by-nonpositive lemma (mul_le_mul_of_nonpos_right, not in stdlib without Mathlib)
• alphaUpdate_mono_state: ring step — (s₁−s₂)·(1−α) ≤ 0
• alphaIterate_formula (inductive step): ring manipulation

---

Verification Status

🔄 Partial verification: lake build passed with Lean 4.29.0. 3 sorry remain in AlphaFilter.lean (listed in summary table). Deadzone.lean is now fully proved (0 sorry).

lake build — Build completed successfully (8 jobs)
Lean (version 4.29.0, x86_64-unknown-linux-gnu)

---

Key Correctness Properties Proved

The no-overshoot upward case is the key safety property: when state ≤ sample, the filter output strictly remains in [state, sample] — it never overshoots. This is critical for autopilot rate/attitude controllers where filter transients could destabilise the aircraft.

theorem alphaUpdate_no_overshoot_up (state alpha sample : Rat)
    (h_le : state ≤ sample) (ha0 : 0 ≤ alpha) (ha1 : alpha ≤ 1) :
    state ≤ alphaUpdate state alpha sample ∧ alphaUpdate state alpha sample ≤ sample

---

🔬 This PR was created by Lean Squad automated formal verification.

Generated by 📐 Lean Squad, see workflow run. Learn more.

To install this agentic workflow, run

gh aw add githubnext/agentics/workflows/lean-squad.md@4b17e80c4ba005a7d9b3507ca5facf9d1fce3b66