Markdown sanitization when applying the body of safe outputs like "create-issue" appears to be mishandling fenced code blocks.
🔬 *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
````cpp
// 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](https://github.com/dsyme/PX4-Autopilot/actions/runs/24468137822)
> Generated by 📐 Lean Squad, see [workflow run](https://github.com/dsyme/PX4-Autopilot/actions/runs/24468137822). [Learn more](https://github.com/githubnext/agentics/blob/main/docs/lean-squad.md).
>
> To install this [agentic workflow](https://github.com/githubnext/agentics/blob/97143ac59cb3a13ef2a77581f929f06719c7402a/workflows/lean-squad.md), run
> ```
> gh aw add githubnext/agentics/workflows/lean-squad.md@97143ac59cb3a13ef2a77581f929f06719c7402a
> ```
<!-- gh-aw-agentic-workflow: Lean Squad, engine: copilot, model: auto, id: 24468137822, workflow_id: lean-squad, run: https://github.com/dsyme/PX4-Autopilot/actions/runs/24468137822 -->
<!-- gh-aw-workflow-id: lean-squad -->
Markdown sanitization when applying the body of safe outputs like "create-issue" appears to be mishandling fenced code blocks.
For example one issue created by
create-issuesafe output is here fsprojects/PX4-Autopilot#39 . If you look at the sanitized markdown for the body of the issue there is a problem with the fencing where a four-backtick fence is terminated by a three-backtick fence. This feels like it has been done by sanitization in GH-AW unless the model actually generated it wrong which seems unlikely. The agentic workflow run that produced this is here: https://github.com/dsyme/PX4-Autopilot/actions/runs/24468137822/job/71500889647