[Lean Squad] feat(fv): Tasks 5+10 — IsInRange (13 theorems, 0 sorry) + REPORT.md updated to 383 theorems (run 76)

[github-actions]

🔬 Lean Squad automated formal verification — run 76

Task 5: math::isInRange Formal Verification

Adds formal-verification/lean/FVSquad/IsInRange.lean — formal proofs of
math::isInRange from src/lib/mathlib/math/Limits.hpp (line 91), the generic
closed-interval predicate used throughout PX4 for range-checking sensor readings,
control outputs, and safety limits.

C++ Source

template<typename _Tp>
constexpr bool isInRange(_Tp val, _Tp min_val, _Tp max_val)
{
    return (min_val <= val) && (val <= max_val);
}
```

### Model

We model `isInRange` over `Int` (unbounded integers), capturing the exact
closed-interval semantics via `Bool` decisions on `Int.le`.

### Theorems Proved (13 total, 0 sorry)

| Theorem | Property |
|---------|----------|
| `isInRange_eq_true_iff` | Fundamental iff characterisation |
| `isInRange_eq_false_iff` | Complement: out-of-range iff `val < min ∨ max < val` |
| `isInRange_of_le_of_le` | Direct introduction from two inequalities |
| `isInRange_min_in_range` | Lower bound is always in range (when non-empty) |
| `isInRange_max_in_range` | Upper bound is always in range (when non-empty) |
| `isInRange_self` | Every value is in its own singleton interval |
| `isInRange_singleton_iff` | Singleton interval ↔ exact equality |
| `isInRange_empty` | Empty interval (`max < min`) always returns `false` |
| `isInRange_mono_bounds` | Widening the interval preserves membership |
| `isInRange_shift` | Shift invariance: translating val and bounds preserves result |
| `isInRange_nonneg_iff` | Specialisation: non-negative range `[0, n]` |
| `isInRange_symmetric_iff` | Specialisation: symmetric range `[-r, r]` |
| `isInRange_eq_decide` | Decidable Bool characterisation |

Also adds `formal-verification/specs/isInRange_informal.md` — informal spec per Task 2.

---

## Task 10: REPORT.md Updated

- **383 theorems, 110 `#eval` examples, 0 sorry, 31 files** (audited from source)
- Status upgraded: **first `0 sorry` milestone** (achieved in run 73)
- File Inventory table corrected with actual per-file counts from source
- Layer 7 expanded: `Crc32Sig` added (UAVCAN bootloader CRC-32/ISO-HDLC, 9 theorems)
- `WrapAngle` row updated: 0 sorry (resolved via axioms in run 73)
- Run history timeline extended: runs 72–76 entries added

---

## 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, commit 98dc76e3c0a9b856c9b98726b713fb04fab16740, Release)
LAKE_BUILD=passed

33 build jobs completed successfully.

---

TARGETS.md

Added target #39 math::isInRange at Phase 5 (Proved).

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