[Lean Squad] feat(formal-verification): math::lerp Lean spec + 9 proofs (run13)

[github-actions]

Summary

This PR adds a formal Lean 4 specification and proofs for PX4's math::lerp function from src/lib/mathlib/math/Functions.hpp.

🔬 Lean Squad automated formal verification (run13).

---

New files

• formal-verification/specs/lerp_informal.md — informal specification covering purpose, preconditions, postconditions, edge cases, and open questions
• formal-verification/lean/FVSquad/Lerp.lean — Lean 4 spec and proofs
• formal-verification/TARGETS.md — updated to advance math::lerp to phase 5

---

C++ source

// src/lib/mathlib/math/Functions.hpp
template<typename T>
const T lerp(const T &a, const T &b, const T &s) {
    return (static_cast<T>(1) - s) * a + s * b;
}

Used throughout PX4 for flight-task setpoint blending, RC stick processing, and gain scheduling.

---

Theorems proved (9 proved, 1 sorry)

Theorem	Property	Status
lerp_zero	lerp(a, b, 0) = a	✅
lerp_one	lerp(a, b, 1) = b	✅
lerp_const	lerp(a, a, s) = a	✅
lerp_alt_form	lerp(a,b,s) = a + s*(b-a)	✅
lerp_lower	s∈[0,1], a≤b ⊢ a ≤ lerp(a,b,s)	✅
lerp_upper	s∈[0,1], a≤b ⊢ lerp(a,b,s) ≤ b	✅
lerp_in_range	Combined range containment	✅
lerp_comm	lerp(a,b,s) = lerp(b,a,1-s)	✅
lerp_mono_s	Monotone non-decreasing in s when a≤b	✅
lerp_half	lerp(a,b,½) = (a+b)/2	🔄 sorry — 1/2 literal needs Rat.inv arithmetic

The no-overshoot safety property (lerp_in_range) is key for control systems: when s ∈ [0, 1] and a ≤ b, lerp stays strictly within [a, b], ruling out runaway setpoints.

---

Model

Over Rat (rational numbers); IEEE 754 NaN/infinity and integer truncation are excluded. No Mathlib dependency.

---

Verification status

🔄 Partial verification: lake build passed with Lean 4.29.0. 1 sorry remains (lerp_half).

Lean version: leanprover/lean4:v4.29.0
lake build: ✅ passed
Sorries: 1 (lerp_half — midpoint theorem, requires Rat.inv arithmetic for 1/2 literal)

---

Task 9 — CI audit

Reviewed .github/workflows/lean-ci.yml:

• Toolchain pinned to lean-toolchain ✅
• Cache keyed on lake-manifest.json hash ✅
• lake build with exit code propagation ✅
• Upload artifacts on failure ✅

No changes needed. CI is healthy.

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