allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

docs: Update AGENTS.md with FisherRigidity module completion and build count

Browse source 
Build: 3328 jobs, 0 errors (lake build SilverSightRRC)
This commit is contained in:
allaun 2026-06-24 10:39:57 -05:00
parent ed08c7ff32
commit aec571d7c1
1 changed files with 16 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
AGENTS.md
View file

@ -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. **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:** 6. **Every new module needs:**
- `@[simp]` theorems for key computations - `@[simp]` theorems for key computations
@ -78,6 +78,21 @@
| Receipt.lean | Complete | 0 | | Receipt.lean | Complete | 0 |
| Bind.lean | Complete | 0 | | Bind.lean | Complete | 0 |
| PIST/Spectral.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) ## BMCTE Eigensolid Threshold (p/N = 1/7)