From 8738d9777702b6752d75d351ba08530a6bb5df08 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Thu, 25 Jun 2026 22:03:00 -0500
Subject: [PATCH] docs: Update ChentsovFinite sorry count to 5
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Verified sorry count: apply-sum (110), uniform-N≥3 (511), refinement (535), rational (559), theorem (586)
- Build: 3307 jobs, 0 errors
---
 AGENTS.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/AGENTS.md b/AGENTS.md
index 7a4eaf60..db7dcf64 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -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 | 8 |
+| CoreFormalism/ChentsovFinite.lean | In Progress | 5 |
 
 ## FisherRigidity — Parabola Focal-Chord to Fisher-Rao Bridge