[Lean Squad] feat(formal-verification): BrakingDistance — Tasks 1+2+3+4+5, 9 theorems proved (run 65)

[github-actions]

🔬 Lean Squad — automated formal verification | run 65

Summary

This PR completes formal verification of math::computeBrakingDistanceFromVelocity (Tasks 1–5) and adds two new research targets (Task 1).

Merges PRs Included

This PR incorporates merged-in content from open PRs #59 (WrapBin), #60 (SqrtLinear), and #61 (CRITIQUE/RESEARCH/TARGETS) into a clean additive branch.

---

Task 3+4+5: math::computeBrakingDistanceFromVelocity (Target 30)

Source: src/lib/mathlib/math/TrajMath.hpp line 107

inline float computeBrakingDistanceFromVelocity(
    const float velocity, const float jerk,
    const float accel, const float accel_delay_max)
{
    return velocity * (velocity / (2.0f * accel) + accel_delay_max / jerk);
}
```

**Informal spec**: `formal-verification/specs/braking_dist_informal.md`

**Lean file**: `formal-verification/lean/FVSquad/BrakingDist.lean`

### Theorems proved (9 total, 0 sorry):

| Theorem | Statement |
|---------|-----------|
| `brakingDist_zero_v` | `brakingDist 0 j a d = 0` |
| `brakingDist_nonneg` | `v ≥ 0, a > 0, j > 0, d ≥ 0 → brakingDist v j a d ≥ 0` |
| `brakingDist_pos` | `v > 0, a > 0, j > 0, d ≥ 0 → brakingDist v j a d > 0` |
| `brakingDist_mono_v` | `0 ≤ v1 ≤ v2 → brakingDist v1 j a d ≤ brakingDist v2 j a d` (**safety: faster→farther**) |
| `brakingDist_mono_d` | `0 ≤ d1 ≤ d2 → brakingDist v j a d1 ≤ brakingDist v j a d2` |
| `brakingDist_no_delay` | `brakingDist v j a 0 = v * v / (2 * a)` |
| `brakingDist_no_delay_nonneg` | `v ≥ 0, a > 0 → brakingDist v j a 0 ≥ 0` |
| `brakingDist_alt_form` | `brakingDist v j a d = v*v/(2*a) + v*d/j` |
| `brakingDist_double_v_no_delay` | `brakingDist (2*v) j a 0 = 4 * brakingDist v j a 0` (**quadratic scaling**) |

Plus 7 `native_decide` examples confirming specific rational values.

The monotonicity-in-velocity theorem is a **flight-safety property**: it formally guarantees that a faster vehicle requires at least as much braking distance, which the trajectory planner relies on for waypoint approach and obstacle avoidance.

---

## Task 1: Research — New Targets Identified

Two new targets added to `formal-verification/RESEARCH.md` and `TARGETS.md`:

- **Target 31**: `math::expo` — RC input shaping curve; bounded output ∈ [−1,1]; `expo(-1,e)=−1`, `expo(0,e)=0`, `expo(1,e)=1`; pure rational model, ≈25 Lean lines
- **Target 32**: `math::lerp` — Linear interpolation; `lerp(a,b,0)=a`, `lerp(a,b,1)=b`; convex combination for 0≤s≤1; ≈20 Lean lines, very tractable

Also removed a duplicate row 29 from `TARGETS.md`.

---

## Verification Status

> 🔄 Partial verification: `lake build` passed with Lean 4.30.0-rc2 (project toolchain: v4.29.0). 9 `sorry`-free BrakingDist theorems. 12 `sorry` remain in **pre-existing** files (WrapAngle×6, Atmosphere×3, SqrtLinear×3 — all require Mathlib which is blocked by network proxy).

```
Build completed successfully (26 jobs).
BrakingDist.lean: 0 sorry
WrapAngle.lean:   6 sorry (pre-existing, needs Mathlib Real.floor)
Atmosphere.lean:  3 sorry (pre-existing, needs Mathlib mul_lt_mul_of_neg_left)
SqrtLinear.lean:  3 sorry (pre-existing, needs Mathlib Real.sqrt)

---

Files Changed

File	Change
formal-verification/lean/FVSquad/BrakingDist.lean	New — 9 theorems, 7 examples, 0 sorry
formal-verification/specs/braking_dist_informal.md	New — informal spec
formal-verification/lean/FVSquad/Basic.lean	Added import FVSquad.BrakingDist
formal-verification/TARGETS.md	Target 30 → Phase 5 ✅; targets 31+32 added; dup row removed
formal-verification/RESEARCH.md	Run 65 section: new targets 31+32; updated priority table

Running Totals After This PR

Metric	Before	After
Theorems proved	334	343
Total theorems	346	355
sorry remaining	12	12
Lean files	24	25
Targets	30	32

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

To install this agentic workflow, run

gh aw add githubnext/agentics/workflows/lean-squad.md@13377ddf7e35c2b6e47aa58f45acb228fba902c8