[Lean Squad] feat(formal-verification): GetBinAtAngle — Tasks 2+3+4+5, 13 theorems 0 sorry (run 67)

[github-actions]

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

Summary

Formal verification of ObstacleMath::get_bin_at_angle and get_offset_bin_index from src/lib/collision_prevention/ObstacleMath.cpp.

Tasks completed: 2 (Informal Spec) + 3 (Formal Spec) + 4 (Implementation) + 5 (Proofs) — all in one run.

New theorems: 13 proved, 0 sorry.

---

Background

The collision-prevention module divides the 360° horizontal plane into n equal angular bins. Two functions are critical:

// Returns bin index [0, n) for a given angle (degrees clockwise from North)
int get_bin_at_angle(float bin_width, float angle) {
    int bin_at_angle = (int)round(matrix::wrap(angle, 0.f, 360.f) / bin_width);
    return wrap_bin(bin_at_angle, 360 / bin_width);
}

// Returns bin index after rotating reference frame by angle_offset
int get_offset_bin_index(int bin, float bin_width, float angle_offset) {
    int offset = get_bin_at_angle(bin_width, angle_offset);
    return wrap_bin(bin - offset, 360 / bin_width);
}

---

Lean Model

The integer model captures exact behaviour when angles are integer multiples of bin_width. The key insight: the full pipeline wrap_360 → divide → round → wrap_bin collapses to a single modular reduction:

def getBinI (n : Nat) (k : Int) : Nat := (k % n).toNat

def getOffsetBinI (n : Nat) (b k_offset : Int) : Nat :=
  getBinI n (b - getBinI n k_offset)

---

Theorems Proved (13, 0 sorry)

Theorem	Statement
getBinI_range	getBinI n k < n — always in [0, n)
getBinI_zero	getBinI n 0 = 0 — 0° → bin 0
getBinI_in_range	identity for k ∈ [0, n)
getBinI_periodic	getBinI n (k + n) = getBinI n k — 360° periodicity
getBinI_periodic_k	periodic for any integer multiple
getBinI_idempotent	getBinI n (getBinI n k) = getBinI n k
getOffsetBinI_range	result always in [0, n)
getOffsetBinI_zero_offset	zero offset = identity
getOffsetBinI_eq_getBinI_sub	KEY: getOffsetBinI n b k = getBinI n (b - k)
getOffsetBinI_periodic_offset	periodic in offset
getOffsetBinI_periodic_bin	periodic in bin
getOffsetBinI_self	getOffsetBinI n k k = 0 — bin meets its own offset
getOffsetBinI_inverse	getBinI n (getOffsetBinI n b k + k) = getBinI n b — round-trip

---

Key Result

getOffsetBinI_eq_getBinI_sub formally proves that get_offset_bin_index implements a rotation on the n-bin circle: the result is (b - k_offset) mod n. Combined with getOffsetBinI_inverse, this verifies invertibility of the sensor frame rotation:

-- Rotating by k and then adding k back recovers the original bin
theorem getOffsetBinI_inverse (n : Nat) (b k : Int) (hn : 0 < n) :
    getBinI n ((getOffsetBinI n b k : Int) + k) = getBinI n b

This is relevant for correctness of collision prevention: sensor data in different reference frames can be correctly merged and round-trip converted.

---

Approximations

• Float rounding: the model is exact for angles that are integer multiples of bin_width. For general float angles, the model gives the intended bin (nearest bin after round()).
• get_lower_bound_angle: involves bin_width/2 (half-integer boundaries). Modelled separately.

---

Verification

🔄 Partial verification: lake build passed with Lean 4.29.0. 0 sorry in GetBinAtAngle.lean. 6 sorry remain in WrapAngle.lean (floor arithmetic, needs Mathlib.Algebra.Order.Floor — unchanged from prior run).

Build command: cd formal-verification/lean && lake build

---

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

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