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 ChentsovFinite sorry count to 8

Browse source 
- Count verified: apply-sum (109), fisher-inv (244), uniform-N≥3 (504-510 x3), refinement (533), rational (557), theorem (584)
- Build: 3307 jobs, 0 errors
This commit is contained in:
allaun 2026-06-25 21:46:42 -05:00
parent 13285b3d40
commit d408aa6c73
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
AGENTS.md
View file

@ -105,7 +105,7 @@ Target: `formal/SilverSight/HachimojiN8.lean` — provable by `native_decide` on
|----|----------------------|--------------------|--------|
| `nuvmap-port` | `Semantics.InvariantReceipt.Instances.NUVMAP` | `formal/SilverSight/InvariantReceipt/NUVMAP.lean` | ❌ Not started |
| `lambda-threshold` | (no RS source — new theorem) | `formal/SilverSight/PIST/BmcteThreshold.lean` | ❌ Not started |
| `chentsov-core` | (ported) | `ChentsovFinite.lean` | ⚠️ 7 sorry blocks: apply-sum, fisher-inv, uniform-N≥3, refinement, rational, theorem |
| `chentsov-core` | (ported) | `ChentsovFinite.lean` | ⚠️ 8 sorry blocks: apply-sum, fisher-inv, uniform-N≥3 (3), refinement, rational, theorem |
## Current Status
@ -119,7 +119,7 @@ Target: `formal/SilverSight/HachimojiN8.lean` — provable by `native_decide` on
| Bind.lean | Complete | 0 |
| PIST/Spectral.lean | Complete | 0 |
| PIST/FisherRigidity.lean | Complete | 0 |
| CoreFormalism/ChentsovFinite.lean | In Progress | 7 |
| CoreFormalism/ChentsovFinite.lean | In Progress | 8 |
## FisherRigidity — Parabola Focal-Chord to Fisher-Rao Bridge