diff --git a/AGENTS.md b/AGENTS.md
index 0c687b26..f4c7b9bc 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -34,7 +34,7 @@
 
 5. **No `native_decide` unless required without alternative.** Use `norm_num`, `omega`, `simp`, `decide`, or explicit proof terms. `native_decide` is a last resort when no other tactic can close the goal. Document why `native_decide` is required when used.
 
-5. **Build gate:** `lake build SilverSight` must pass (3307 jobs, 0 errors as of 2026-06-22).
+5. **Build gate:** `lake build SilverSight` must pass (3328 jobs, 0 errors as of 2026-06-24).
 
 6. **Every new module needs:**
    - `@[simp]` theorems for key computations
@@ -78,6 +78,21 @@
 | Receipt.lean | Complete | 0 |
 | Bind.lean | Complete | 0 |
 | PIST/Spectral.lean | Complete | 0 |
+| PIST/FisherRigidity.lean | Complete | 0 |
+
+## FisherRigidity — Parabola Focal-Chord to Fisher-Rao Bridge
+
+**Purpose:** Bridges parabola focal-chord perpendicularity (s₁·s₂ = -1) to Fisher-Rao geometric rigidity and Hachimoji eigensolid braid dynamics.
+
+**Key structures:**
+- `ConjugatePair` — slope pair encoding perpendicularity
+- `IsOrthogonal` — Fisher inner product vanishing predicate
+- `eigensolidSpectralGap` — 9984 Q16.16 (≈0.152), near 1/7 threshold
+
+**Eval witnesses:**
+- `parabolaConjugatePair one` → { slope_large := 158217, slope_small := -27147 }
+- `eigensolidSpectralGap` → 9984
+- `div eigensolidSpectralGap 65536` → 9984 (0.152 normalized)
 
 ## BMCTE Eigensolid Threshold (p/N = 1/7)