docs: Update ChentsovFinite status - 7 sorries remaining

- CoreFormalism/ChentsovFinite.lean now tracked in module table
- Consolidated old sorry entries into single 'chentsov-core' entry
- Build verified: 3307 jobs, 0 errors

AGENTS.md

@@ -105,9 +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-h9` | `ChentsovFinite.lean:~608` | same file — `h9` in `hc_pos` | ⚠️ `sorry`; closable via `h_perm (Equiv.swap 1 2)` + `simp`; est. ~20 lines |
-| `chentsov-diagonal` | `ChentsovFinite.lean:~836` | same file — diagonal `h_agree` | ⚠️ `sorry`; needs Steps A–E: `h_inv` at `splitIdx=i` → `IsFunctionalEquation` → `functional_eq_unique` → `c_val/p_i`; est. ~100 lines |
-| `chentsov-offdiag` | `ChentsovFinite.lean:~862` | same file — off-diagonal `h_agree` | ⚠️ `sorry`; needs Steps A–C: `h_inv` at `splitIdx=0` → functional eq for cross term → `c_val/p_0`; est. ~80 lines |
+| `chentsov-core` | (ported) | `ChentsovFinite.lean` | ⚠️ 7 sorry blocks: apply-sum, fisher-inv, uniform-N≥3, refinement, rational, theorem |
 
 ## Current Status
 
@@ -121,6 +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 |
 
 ## FisherRigidity — Parabola Focal-Chord to Fisher-Rao Bridge