[Lean Squad] feat(fv): interpolateNXY 3-pt spec (Task 4) + deadzone/expodz odd symmetry (Task 5) — run36

[github-actions]

🔬 Lean Squad — automated formal verification run 36.

Summary

Two tasks completed this run:

Task 4 — Implementation Extraction: interpolateNXY (new target)

New file: formal-verification/lean/FVSquad/InterpolateNXY.lean

Formal specification and proofs for math::interpolateNXY from
src/lib/mathlib/math/Functions.hpp. Models the 3-point case (N=3) as interp3:

// C++ original (N=3 case):
// - v > x[1]: use interpolate(v, x[1], x[2], y[1], y[2])
// - v ≤ x[1]: use interpolate(v, x[0], x[1], y[0], y[1])

9 theorems proved, 0 sorry:

Theorem	Property
interp3_low_clamp	v ≤ x0 → output = y0 (clamped at low end)
interp3_high_clamp	v > x2 → output = y2 (clamped at high end)
interp3_at_x0	At first breakpoint: output = y0
interp3_at_x1	At interior breakpoint: output = y1 (from segment 0)
interp3_seg1_at_x1	Continuity: segment 1 also gives y1 at x1
interp3_at_x2	At last breakpoint: output = y2
interp3_le_y2	Upper range bound: output ≤ y2 when y-values ordered
interp3_ge_y0	Lower range bound: output ≥ y0 when y-values ordered
interp3_mono_seg0	Monotone within segment 0: larger v → larger output

The continuity proof (interp3_at_x1 + interp3_seg1_at_x1) is particularly
important: it confirms the two piecewise segments join smoothly at y[1], ruling out
discontinuous "jumps" at the interior breakpoint that could cause actuator transients.

New file: formal-verification/specs/interpolatenxy_informal.md — informal spec
with purpose, preconditions, postconditions, edge cases and worked examples.

Task 5 — Proof Assistance: Odd Symmetry for deadzone and expo-deadzone

deadzone_odd (Deadzone.lean)

New theorem: deadzone_odd — the deadzone is an odd function:

theorem deadzone_odd (x dz : Rat) (hdz : 0 ≤ dz) :
    deadzone (-x) dz = -(deadzone x dz)

Three-case proof: positive branch (x > dz), negative branch (x < -dz),
in-deadzone (|x| ≤ dz). Each case uses the existing deadzone_pos_eq/deadzone_neg_eq
lemmas and rational arithmetic (Rat.neg_sub, Rat.neg_add, Rat.div_def).

This is a key structural property: the RC stick deadzone preserves sign symmetry.

expodz_odd (ExpoDeadzone.lean)

New theorem: expodz_odd — the expo-deadzone pipeline is an odd function:

theorem expodz_odd (v e dz : Rat) (hdz : 0 ≤ dz) :
    expodz (-v) e dz = -(expodz v e dz)

Proof by composition: deadzone_odd + expo_odd (expo already had this theorem).
This was the gap flagged in the previous run's CRITIQUE.md.

---

Verification Status

✅ Proofs verified: lake build passed with Lean 4.29.0. 0 sorry in new/modified files.

All 19 modules built successfully. Only pre-existing 6 sorry warnings in WrapAngle.lean
(wrapRat theorems requiring Mathlib floor arithmetic — unchanged).

---

Files Changed

• formal-verification/lean/FVSquad/InterpolateNXY.lean — new (9 theorems, 0 sorry)
• formal-verification/specs/interpolatenxy_informal.md — new (informal spec)
• formal-verification/lean/FVSquad/Deadzone.lean — add deadzone_odd theorem
• formal-verification/lean/FVSquad/ExpoDeadzone.lean — add expodz_odd theorem
• formal-verification/lean/FVSquad.lean — add InterpolateNXY import
• formal-verification/TARGETS.md — add targets 16 and 17

---

Generated by 🔬 Lean Squad, see workflow run.

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

To install this agentic workflow, run

gh aw add githubnext/agentics/workflows/lean-squad.md@97143ac59cb3a13ef2a77581f929f06719c7402a