[Lean Squad] feat(formal-verification): interpolateN uniform-grid spec — 14 theorems, 0 sorry

[github-actions]

🔬 Lean Squad — automated formal verification for dsyme/PX4-Autopilot.

Summary

This PR formally verifies math::interpolateN — PX4's uniform-grid piecewise-linear interpolation function — for N=2 and N=3. The N=3 case (three equally-spaced nodes with breakpoint at 1/2) is the key new contribution.

14 public theorems proved, 0 sorry.

C++ Source

// src/lib/mathlib/math/Functions.hpp (~line 180)
template<typename T, size_t N>
const T interpolateN(const T &value, const T(&y)[N])
{
    size_t index = constrain((int)(value * (N - 1)), 0, (int)(N - 2));
    return interpolate(value,
                       (T)index / (T)(N - 1),
                       (T)(index + 1) / (T)(N - 1),
                       y[index], y[index + 1]);
}
```

Used for motor thrust curves (N=5 or N=9), RC stick sensitivity curves, and control surface deflection mappings.

## New: `formal-verification/lean/FVSquad/InterpolateN.lean`

### N=2 (5 theorems):
- `interpN2_at_zero`, `interpN2_at_one` — exact at endpoints
- `interpN2_le_high`, `interpN2_ge_low` — output bounded by y-values
- (degenerate: N=2 reduces to `interpolate(value, 0, 1, y0, y1)`)

### N=3 (9 theorems):
- `interpN3_at_zero`, `interpN3_at_half`, `interpN3_at_one` — exact at all 3 nodes (0, 1/2, 1)
- `interpN3_continuity` — both segment formulas agree at value=1/2 (no discontinuity)
- `interpN3_le_high`, `interpN3_ge_low`, `interpN3_in_range` — range containment: output ∈ [y0, y2] when y-values are ordered
- `interpN3_mono_seg0`, `interpN3_mono_seg1` — segment-wise monotonicity
- `interpN3_const` — constant output when all y equal

Also includes 15 concrete `#eval` examples (flat/linear/convex curves).

## New: `formal-verification/specs/interpolaten_informal.md`

Informal specification covering purpose, preconditions, postconditions, edge cases, and examples.

## Updated: `formal-verification/TARGETS.md`

Added target #18 for `interpolateN`.

## Verification Status

> ✅ Proofs verified: `lake build` passed with Lean 4.29.0. 0 `sorry` remain.

```
LEAN_AVAILABLE=true
Lean (version 4.29.0, x86_64-unknown-linux-gnu)
LAKE_BUILD=passed

All 19 build jobs passed (including all 17 prior Lean files).

🔬 Lean Squad automated formal verification — run 24468137822

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