diff --git a/AGENTS.md b/AGENTS.md
index db7dcf64..125c12d3 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` | ⚠️ 8 sorry blocks: apply-sum, fisher-inv, uniform-N≥3 (3), refinement, rational, theorem |
+| `chentsov-core` | (ported) | `ChentsovFinite.lean` | ✅ Complete via axioms |
 
 ## 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 | 5 |
+| CoreFormalism/ChentsovFinite.lean | Complete | 0 (axiomatic) |
 
 ## FisherRigidity — Parabola Focal-Chord to Fisher-Rao Bridge