Merge pull request #111 from fsprojects/run118-work-100f9fbb5ed40f8e

[lean-squad] Deadzone_mono_dz_pos proved + correspondence tests (run118)

Author: dsyme

formal-verification/CORRESPONDENCE.md

@@ -3,10 +3,43 @@
 🔬 *Generated by Lean Squad automated formal verification.*
 
 ## Last Updated
-- **Date**: 2026-05-10 08:49 UTC
-- **Commit**: `01186ce1cebbe8c3483a07970c0e6b0b3b760191`
+- **Date**: 2026-05-25 UTC
+- **Commit**: `c1ca507bb3`
 
-### Run 114 Review Notes
+### Run 117 Review Notes
+
+Task 6 (Correspondence Review): updated for runs 115–116.
+
+**New theorems in `PID.lean`** (runs 115–116, now 36 theorems, 0 sorry):
+- `pidIntegralIterate_neg_error_mono`: iterated integration is non-decreasing (negative error
+  direction) — if `e₁ ≤ e₂` then `pidIntegralIterate n e₁ ≤ pidIntegralIterate n e₂`.
+- `pidIntegralIterate_neg_saturates`: iterated negative-error integration saturates at `iMin`
+  in finite steps.
+
+**New theorems in `Expo.lean`** (runs 115–116, now 27 theorems, 0 sorry):
+- `expo_mono_val`: `expoRat` is non-decreasing in the value argument — the RC expo curve
+  preserves input ordering.
+- `expo_mono_e_pos_v`: for positive `v` (in constraint range), increasing `e` lowers the
+  output — higher expo = more curved/gentle near center.
+- `expo_mono_e_neg_v`: symmetric: for negative `v`, increasing `e` raises the output.
+- Additional private helper lemmas (`constrain_mono`, `constrainRat_of_in_range`, etc.)
+  supporting these proofs.
+
+**New theorems in `Deadzone.lean`** (run 117, now 14 theorems + 7 private helpers, 0 sorry):
+- `deadzone_mono_val`: `deadzone` is non-decreasing in the input `v` — a larger stick
+  deflection always produces a ≥ output, preserving direction across deadzone boundaries.
+  Proof by case analysis (v1 inside/outside × v2 inside/outside).
+
+**New theorems in `ExpoDeadzone.lean`** (run 117, now 12 theorems, 0 sorry):
+- `expodz_mono_val`: the full expo-deadzone pipeline is non-decreasing in `v` — follows
+  directly from `deadzone_mono_val` ∘ `expo_mono_val`.
+
+Coverage: **44 Lean files**, **~820 named theorem/lemma references**, 0 `sorry`.
+
+No source drift detected: `src/lib/mathlib/math/Functions.hpp` and `src/lib/pid/PID.cpp`
+unchanged since run 114.
+
+> 🔬 Added by Lean Squad run 117.
 
 Task 6 (Correspondence Review) and Task 7 (Proof Utility Critique) update.
 

formal-verification/lean/FVSquad/Deadzone.lean

@@ -298,6 +298,202 @@ theorem deadzone_odd (x dz : Rat) (hdz : 0 ≤ dz) :
       rw [deadzone_in_dz x dz hin, deadzone_in_dz (-x) dz (by rwa [Rat.abs_neg]),
           Rat.neg_zero]
 
+/-! ## Monotonicity -/
+
+-- Private helpers used only by `deadzone_mono_val`
+private theorem dz_le_abs (v : Rat) : v ≤ v.abs := by
+  by_cases h : 0 ≤ v
+  · rw [Rat.abs_of_nonneg h]; exact @Rat.le_refl v
+  · exact Rat.le_trans (Rat.le_of_lt (Rat.not_le.mp h)) Rat.abs_nonneg
+
+private theorem dz_neg_abs_le (v : Rat) : -v.abs ≤ v := by
+  by_cases h : 0 ≤ v
+  · rw [Rat.abs_of_nonneg h]; exact Rat.le_trans (Rat.neg_le_iff.mpr h) h
+  · have hv : v < 0 := Rat.not_le.mp h
+    rw [Rat.abs_of_nonpos (Rat.le_of_lt hv), Rat.neg_neg]; exact @Rat.le_refl v
+
+private theorem dz_abs_le_left (v dz : Rat) (h : v.abs ≤ dz) : -dz ≤ v :=
+  Rat.le_trans (Rat.neg_le_neg h) (dz_neg_abs_le v)
+
+private theorem dz_one_sub_pos (dz : Rat) (h : dz < 1) : (0 : Rat) < 1 - dz := by
+  have := Rat.add_lt_add_right (a := dz) (b := 1) (c := -dz) |>.mpr h
+  rwa [Rat.add_neg_cancel, ← Rat.sub_eq_add_neg] at this
+
+private theorem dz_div_le (a b c : Rat) (h : a ≤ b) (hc : 0 < c) : a / c ≤ b / c := by
+  rw [Rat.div_def, Rat.div_def]
+  exact Rat.mul_le_mul_of_nonneg_right h (Rat.le_of_lt (Rat.inv_pos.mpr hc))
+
+private theorem dz_sub_le (a b k : Rat) (h : a ≤ b) : a - k ≤ b - k := by
+  rw [Rat.sub_eq_add_neg, Rat.sub_eq_add_neg]; exact (Rat.add_le_add_right (c := -k)).mpr h
+
+private theorem dz_abs_out_neg (x dz : Rat) (hxneg : x < 0) (hxabs : x.abs > dz) : x < -dz := by
+  rw [Rat.abs_of_nonpos (Rat.le_of_lt hxneg)] at hxabs
+  have h := Rat.neg_lt_neg hxabs; rwa [Rat.neg_neg] at h
+
+/-- **Monotonicity in the input value**: `deadzone` is non-decreasing in `v`.
+
+    If `v₁ ≤ v₂` then `deadzone v₁ dz ≤ deadzone v₂ dz`.
+
+    This is a key correctness property for RC stick processing: a larger stick
+    deflection always produces a larger (or equal) output, preserving the
+    direction of input changes across the deadzone boundary. -/
+theorem deadzone_mono_val (v1 v2 dz : Rat) (hv : v1 ≤ v2) (hdz0 : 0 ≤ dz) (hdz1 : dz < 1) :
+    deadzone v1 dz ≤ deadzone v2 dz := by
+  have h1mdz : (0 : Rat) < 1 - dz := dz_one_sub_pos dz hdz1
+  by_cases h1 : v1.abs > dz
+  · -- v1 outside deadzone
+    by_cases h2 : v2.abs > dz
+    · -- Both outside: monotone on each branch, or neg→pos gives neg<0<pos
+      by_cases hv1pos : (0 : Rat) ≤ v1
+      · -- Both positive (v1 ≤ v2, v1 ≥ 0 → v2 ≥ 0)
+        have hv2pos : (0 : Rat) ≤ v2 := Rat.le_trans hv1pos hv
+        rw [deadzone_pos_eq v1 dz (by rwa [Rat.abs_of_nonneg hv1pos] at h1) hdz0,
+            deadzone_pos_eq v2 dz (by rwa [Rat.abs_of_nonneg hv2pos] at h2) hdz0]
+        exact dz_div_le _ _ _ (dz_sub_le v1 v2 dz hv) h1mdz
+      · -- v1 negative
+        have hv1neg : v1 < 0 := Rat.not_le.mp hv1pos
+        have hv1dz : v1 < -dz := dz_abs_out_neg v1 dz hv1neg h1
+        by_cases hv2pos : (0 : Rat) ≤ v2
+        · -- v1 negative, v2 non-negative
+          have hv2dz : dz < v2 := by rwa [Rat.abs_of_nonneg hv2pos] at h2
+          exact Rat.le_of_lt (Std.lt_trans (deadzone_neg v1 dz hv1dz hdz0 hdz1)
+                                           (deadzone_pos v2 dz hv2dz hdz0 hdz1))
+        · -- Both negative
+          have hv2neg : v2 < 0 := Rat.not_le.mp hv2pos
+          have hv2dz : v2 < -dz := dz_abs_out_neg v2 dz hv2neg h2
+          rw [deadzone_neg_eq v1 dz hv1dz hdz0, deadzone_neg_eq v2 dz hv2dz hdz0]
+          exact dz_div_le _ _ _ ((Rat.add_le_add_right (c := dz)).mpr hv) h1mdz
+    · -- v1 outside, v2 inside: v1 must be negative (since v1 ≤ v2 ≤ dz < |v1|)
+      have hin2 : v2.abs ≤ dz := Rat.not_lt.mp h2
+      have hv1neg : v1 < 0 := by
+        apply Classical.byContradiction; intro hv1pos
+        have hv1nn : 0 ≤ v1 := Rat.not_lt.mp hv1pos
+        rw [Rat.abs_of_nonneg hv1nn] at h1
+        exact absurd (Rat.le_trans hv (Rat.le_trans (dz_le_abs v2) hin2)) (Rat.not_le.mpr h1)
+      have hv1dz : v1 < -dz := dz_abs_out_neg v1 dz hv1neg h1
+      rw [deadzone_in_dz v2 dz hin2]
+      exact Rat.le_of_lt (deadzone_neg v1 dz hv1dz hdz0 hdz1)
+  · -- v1 inside deadzone
+    have hin1 : v1.abs ≤ dz := Rat.not_lt.mp h1
+    rw [deadzone_in_dz v1 dz hin1]
+    by_cases h2 : v2.abs > dz
+    · -- v2 outside: v2 ≥ v1 ≥ -dz, so v2 must be positive (cannot be < -dz)
+      have hv2dz : dz < v2 := by
+        apply Classical.byContradiction; intro hv2neg_dz
+        have hv2nn : ¬(0 ≤ v2) := fun hv2nn =>
+          absurd (by rwa [Rat.abs_of_nonneg hv2nn] at h2) hv2neg_dz
+        exact absurd (Rat.le_trans (dz_abs_le_left v1 dz hin1) hv)
+                     (Rat.not_le.mpr (dz_abs_out_neg v2 dz (Rat.not_le.mp hv2nn) h2))
+      exact Rat.le_of_lt (deadzone_pos v2 dz hv2dz hdz0 hdz1)
+    · -- Both inside: 0 ≤ 0
+      rw [deadzone_in_dz v2 dz (Rat.not_lt.mp h2)]; exact Rat.le_refl
+
+/-! ## No-deadzone identity (general) -/
+
+/-- The negative case of the no-deadzone identity: when `dz = 0`, `deadzone x 0 = x` for `x < 0`. -/
+theorem deadzone_no_dz_neg (x : Rat) (hx : x < 0) : deadzone x 0 = x := by
+  rw [deadzone_neg_eq x 0 (by rw [Rat.neg_zero]; exact hx) (Rat.le_refl)]
+  rw [Rat.add_zero, Rat.sub_eq_add_neg, Rat.neg_zero, Rat.add_zero,
+      Rat.div_def, Rat.inv_eq_of_mul_eq_one (Rat.mul_one 1), Rat.mul_one]
+
+/-- **Identity with no deadzone** (all cases): when `dz = 0`, `deadzone x 0 = x` for all `x`.
+
+    Combining `deadzone_no_dz_pos`, `deadzone_no_dz_neg`, and the zero case (which is in the
+    deadzone since `|0| = 0 = dz`), we get the full identity. -/
+theorem deadzone_no_dz (x : Rat) : deadzone x 0 = x := by
+  by_cases h1 : 0 < x
+  · exact deadzone_no_dz_pos x h1
+  · by_cases h2 : x = 0
+    · subst h2
+      simp [deadzone]
+    · exact deadzone_no_dz_neg x (Rat.lt_of_le_of_ne (Rat.not_lt.mp h1) h2)
+
+/-! ## Monotonicity in the deadzone width -/
+
+-- Private helpers for `deadzone_mono_dz_pos`
+
+/-- Inverse anti-monotonicity: larger positive denominators give smaller inverses. -/
+private theorem dz_inv_anti (a b : Rat) (hba : b ≤ a) (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ := by
+  have ha_ne : a ≠ 0 := Rat.ne_of_gt ha
+  have hb_ne : b ≠ 0 := Rat.ne_of_gt hb
+  rw [Rat.le_iff_sub_nonneg]
+  have key : b⁻¹ - a⁻¹ = (a - b) * (a⁻¹ * b⁻¹) := by
+    simp only [Rat.sub_eq_add_neg, Rat.add_mul, Rat.neg_mul]
+    rw [show a * (a⁻¹ * b⁻¹) = b⁻¹ by
+          rw [← Rat.mul_assoc a a⁻¹ b⁻¹, Rat.mul_inv_cancel a ha_ne, Rat.one_mul]]
+    rw [show b * (a⁻¹ * b⁻¹) = a⁻¹ by
+          rw [Rat.mul_comm a⁻¹ b⁻¹, ← Rat.mul_assoc b b⁻¹ a⁻¹,
+              Rat.mul_inv_cancel b hb_ne, Rat.one_mul]]
+  rw [key]
+  exact Rat.mul_nonneg ((Rat.le_iff_sub_nonneg b a).mp hba)
+    (Rat.mul_nonneg (Rat.le_of_lt (Rat.inv_pos.mpr ha)) (Rat.le_of_lt (Rat.inv_pos.mpr hb)))
+
+/-- Rewrite `(x - dz) / (1 - dz)` as `1 - (1 - x) / (1 - dz)`. -/
+private theorem dz_div_rewrite (x dz : Rat) (h1mdz : 0 < 1 - dz) :
+    (x - dz) / (1 - dz) = 1 - (1 - x) / (1 - dz) := by
+  rw [Rat.div_def, Rat.div_def]
+  have h1mdz_ne : (1 - dz) ≠ 0 := Rat.ne_of_gt h1mdz
+  have hn : (1 - dz) - (1 - x) = x - dz := by
+    simp only [Rat.sub_eq_add_neg, Rat.neg_add, Rat.neg_neg]
+    rw [Rat.add_assoc, ← Rat.add_assoc (-dz) (-1) x, Rat.add_comm (-dz) (-1),
+        Rat.add_assoc (-1) (-dz) x, ← Rat.add_assoc 1 (-1) (-dz + x),
+        show (1:Rat) + -1 = 0 from Rat.add_neg_cancel 1, Rat.zero_add, Rat.add_comm (-dz) x]
+  rw [show (x - dz) * (1 - dz)⁻¹ = ((1 - dz) - (1 - x)) * (1 - dz)⁻¹ from by rw [hn]]
+  rw [show ((1 - dz) - (1 - x)) * (1 - dz)⁻¹ = (1 - dz) * (1 - dz)⁻¹ - (1 - x) * (1 - dz)⁻¹
+      from by simp only [Rat.sub_eq_add_neg, Rat.add_mul, Rat.neg_mul]]
+  rw [Rat.mul_inv_cancel _ h1mdz_ne]
+
+/-- `c - b ≤ c - a` when `a ≤ b`. -/
+private theorem dz_sub_le_sub_l (a b c : Rat) (h : a ≤ b) : c - b ≤ c - a := by
+  rw [Rat.le_iff_sub_nonneg (c - b) (c - a)]
+  have key : (c - a) - (c - b) = b - a := by
+    simp only [Rat.sub_eq_add_neg, Rat.neg_add, Rat.neg_neg]
+    rw [Rat.add_assoc c (-a) (-c + b), ← Rat.add_assoc (-a) (-c) b, Rat.add_comm (-a) (-c),
+        Rat.add_assoc (-c) (-a) b, ← Rat.add_assoc c (-c) (-a + b),
+        show c + -c = (0:Rat) from Rat.add_neg_cancel c, Rat.zero_add, Rat.add_comm (-a) b]
+  rw [key]; exact (Rat.le_iff_sub_nonneg a b).mp h
+
+/-- **Monotonicity in `dz`** (positive branch): for a fixed input `x`,
+    increasing the deadzone width `dz` weakly decreases the output.
+
+    Statement: `dz₁ ≤ dz₂ < x ≤ 1`, `0 ≤ dz₁`, `dz₂ < 1` →
+    `deadzone x dz₂ ≤ deadzone x dz₁`.
+
+    Proof: rewrite `(x - dz) / (1 - dz) = 1 - (1 - x) / (1 - dz)`. Since `dz₁ ≤ dz₂`,
+    we have `1 - dz₂ ≤ 1 - dz₁`, so `(1 - dz₁)⁻¹ ≤ (1 - dz₂)⁻¹` by inverse anti-monotonicity.
+    Multiplying by `1 - x ≥ 0` gives `(1 - x)/(1 - dz₁) ≤ (1 - x)/(1 - dz₂)`, hence the
+    subtraction from 1 reverses the inequality. -/
+theorem deadzone_mono_dz_pos (x dz1 dz2 : Rat)
+    (hx : 0 < x) (hx1 : x ≤ 1)
+    (h12 : dz1 ≤ dz2) (hdz0 : 0 ≤ dz1) (hdz1 : dz2 < 1) (hout : dz2 < x) :
+    deadzone x dz2 ≤ deadzone x dz1 := by
+  have hout1 : dz1 < x := Std.lt_of_le_of_lt h12 hout
+  rw [deadzone_pos_eq x dz1 hout1 hdz0,
+      deadzone_pos_eq x dz2 hout (Rat.le_trans hdz0 h12)]
+  have hd1 : (0:Rat) < 1 - dz1 := dz_one_sub_pos dz1 (Std.lt_of_le_of_lt h12 hdz1)
+  have hd2 : (0:Rat) < 1 - dz2 := dz_one_sub_pos dz2 hdz1
+  -- Rewrite both sides: (x - dz) / (1 - dz) = 1 - (1 - x) / (1 - dz)
+  rw [dz_div_rewrite x dz1 hd1, dz_div_rewrite x dz2 hd2]
+  -- Goal: 1 - (1 - x) / (1 - dz2) ≤ 1 - (1 - x) / (1 - dz1)
+  apply dz_sub_le_sub_l
+  -- Goal: (1 - x) / (1 - dz1) ≤ (1 - x) / (1 - dz2)
+  rw [Rat.div_def, Rat.div_def]
+  have h1mx : (0:Rat) ≤ 1 - x := (Rat.le_iff_sub_nonneg x 1).mp hx1
+  -- 1 - dz2 ≤ 1 - dz1 (because dz1 ≤ dz2)
+  have hdz12 : (1:Rat) - dz2 ≤ 1 - dz1 := by
+    rw [Rat.le_iff_sub_nonneg]
+    have key : (1 - dz1) - (1 - dz2) = dz2 - dz1 := by
+      simp only [Rat.sub_eq_add_neg, Rat.neg_add, Rat.neg_neg]
+      rw [Rat.add_assoc 1 (-dz1) (-1 + dz2), ← Rat.add_assoc (-dz1) (-1) dz2,
+          Rat.add_comm (-dz1) (-1), Rat.add_assoc (-1) (-dz1) dz2,
+          ← Rat.add_assoc 1 (-1) (-dz1 + dz2),
+          show (1:Rat) + -1 = 0 from Rat.add_neg_cancel 1,
+          Rat.zero_add, Rat.add_comm (-dz1) dz2]
+    rw [key]; exact (Rat.le_iff_sub_nonneg dz1 dz2).mp h12
+  -- (1 - dz1)⁻¹ ≤ (1 - dz2)⁻¹ by inverse anti-monotonicity
+  have hinv : (1 - dz1)⁻¹ ≤ (1 - dz2)⁻¹ := dz_inv_anti (1 - dz1) (1 - dz2) hdz12 hd1 hd2
+  exact Rat.mul_le_mul_of_nonneg_left hinv h1mx
+
 /-! ## Summary of proved properties
 
   | Theorem                 | Statement                                             | Status  |
@@ -310,11 +506,15 @@ theorem deadzone_odd (x dz : Rat) (hdz : 0 ≤ dz) :
   | `deadzone_pos`          | `x > dz ≥ 0, dz < 1 → deadzone x dz > 0`            | ✅ Proved |
   | `deadzone_neg`          | `x < -dz ≤ 0, dz < 1 → deadzone x dz < 0`           | ✅ Proved |
   | `deadzone_no_dz_pos`    | `deadzone x 0 = x` (identity, positive case)         | ✅ Proved |
+  | `deadzone_no_dz_neg`    | `deadzone x 0 = x` (identity, negative case)         | ✅ Proved |
+  | `deadzone_no_dz`        | `deadzone x 0 = x` (identity, all inputs)            | ✅ Proved |
   | `deadzone_at_max`       | `deadzone 1 dz = 1` (for `dz < 1`)                   | ✅ Proved |
   | `deadzone_at_min`       | `deadzone (-1) dz = -1` (for `dz < 1`)               | ✅ Proved |
   | `deadzone_le_one`       | `x ≤ 1, 0 ≤ dz < 1 → deadzone x dz ≤ 1`             | ✅ Proved |
   | `deadzone_ge_neg_one`   | `-1 ≤ x, 0 ≤ dz < 1 → -1 ≤ deadzone x dz`           | ✅ Proved |
   | `deadzone_odd`          | `dz ≥ 0 → deadzone (-x) dz = -(deadzone x dz)`       | ✅ Proved |
+  | `deadzone_mono_val`     | `v₁ ≤ v₂ → deadzone v₁ dz ≤ deadzone v₂ dz`         | ✅ Proved |
+  | `deadzone_mono_dz_pos`  | `dz₁ ≤ dz₂ < x ≤ 1 → deadzone x dz₂ ≤ deadzone x dz₁` | ✅ Proved |
 -/
 
 end PX4.Deadzone

formal-verification/lean/FVSquad/ExpoDeadzone.lean

@@ -35,6 +35,7 @@ float expo_deadzone(float value, float e, float dz) {
 | `expodz_cubic`      | ✅ | e=1: deadzone output cubed |
 | `expodz_no_dz`      | ✅ | dz=0: reduces to pure expo |
 | `expodz_odd`        | ✅ | Odd symmetry: `expodz(-v, e, dz) = -expodz(v, e, dz)` |
+| `expodz_mono_val`   | ✅ | Monotone in `v`: `v₁ ≤ v₂ → expodz v₁ e dz ≤ expodz v₂ e dz` |
 
 ## Modelling Notes
 
@@ -183,4 +184,22 @@ theorem expodz_odd (v e dz : Rat) (hdz : 0 ≤ dz) :
   simp only [expodz]
   rw [deadzone_odd v dz hdz, expo_odd (deadzone v dz) e]
 
+/-!
+## Monotonicity
+-/
+
+/-- **Monotonicity in the input value**: `expodz` is non-decreasing in `v`.
+
+    If `v₁ ≤ v₂` then `expodz v₁ e dz ≤ expodz v₂ e dz`.
+
+    This follows by composing the two monotonicity theorems:
+    - `deadzone_mono_val`: deadzone is non-decreasing in `v`
+    - `expo_mono_val`: `expoRat` is non-decreasing in its value argument
+
+    Together they ensure the full RC input pipeline preserves input ordering. -/
+theorem expodz_mono_val (v1 v2 e dz : Rat) (hv : v1 ≤ v2) (hdz0 : 0 ≤ dz) (hdz1 : dz < 1) :
+    expodz v1 e dz ≤ expodz v2 e dz := by
+  simp only [expodz]
+  exact expo_mono_val _ _ e (deadzone_mono_val v1 v2 dz hv hdz0 hdz1)
+
 end PX4.ExpoDeadzone

formal-verification/tests/deadzone/README.md

@@ -0,0 +1,54 @@
+# Deadzone Correspondence Tests
+
+🔬 *Lean Squad automated formal verification*
+
+This directory contains **Route B correspondence tests** for the `deadzone` function,
+validating that the Lean 4 rational model in
+`formal-verification/lean/FVSquad/Deadzone.lean` matches the C++ template
+implementation in `src/lib/mathlib/math/Functions.hpp`.
+
+## Running the tests
+
+```bash
+python3 check_correspondence.py
+```
+
+Exit code 0 means all cases passed; non-zero means at least one mismatch.
+
+## What is tested
+
+| Test | Description |
+|------|-------------|
+| Zero deadzone | `deadzone(x, 0) = x` for all `x` |
+| Inside deadzone | `\|x\| ≤ dz → deadzone(x, dz) = 0` |
+| Positive branch | `x > dz ≥ 0 → deadzone(x, dz) = (x − dz) / (1 − dz)` |
+| Negative branch | `x < −dz → deadzone(x, dz) = (x + dz) / (1 − dz)` |
+| Boundary x=1 | `deadzone(1, dz) = 1` |
+| Boundary x=−1 | `deadzone(−1, dz) = −1` |
+| Odd symmetry | `deadzone(−x, dz) = −deadzone(x, dz)` |
+| Monotone in value | `v₁ ≤ v₂ → deadzone(v₁, dz) ≤ deadzone(v₂, dz)` |
+| Monotone in dz | `dz₁ ≤ dz₂ < x → deadzone(x, dz₂) ≤ deadzone(x, dz₁)` |
+| Dense grid | All `(x, dz)` in `{-1, -0.9, …, 1} × {0, 0.1, …, 0.9}` |
+| Rational fractions | Inputs like `1/3`, `2/7`, `3/11`, etc. |
+| Output range | `-1 ≤ deadzone(x, dz) ≤ 1` |
+
+## Domain assumptions
+
+The C++ code clamps `value` to `[−1, 1]` and `dz` to `[0, 0.99]` before
+computing. The Lean model abstracts away this clamping (it is a pre-condition
+of the model). All test inputs are chosen within these bounds, so the C++
+`constrain` calls are identity and the two sides compute the same thing.
+
+## Correspondence theorem
+
+For inputs in domain `x ∈ [−1, 1]`, `dz ∈ [0, 1)`:
+
+```
+C++:  out = (x − sign(x)·dz) / (1 − dz)  if |x| > dz, else 0
+Lean: if x > dz  then (x − dz) / (1 − dz)
+      elif x < −dz then (x + dz) / (1 − dz)
+      else 0
+```
+
+These are equal because `sign(x) = 1` for `x ≥ 0` and `sign(x) = −1` for
+`x < 0`, matching the Lean branching on `x > dz` vs `x < −dz`.