From d408aa6c733ff3ab9f4b2f11c839fc1192b78069 Mon Sep 17 00:00:00 2001 From: allaun Date: Thu, 25 Jun 2026 21:46:42 -0500 Subject: [PATCH] docs: Update ChentsovFinite sorry count to 8 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 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 --- AGENTS.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index a74c7a90..7a4eaf60 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -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