From 44f8df9b4adc554fe46b26d9612bf90d7f4c2c4b Mon Sep 17 00:00:00 2001 From: allaun Date: Thu, 25 Jun 2026 21:22:11 -0500 Subject: [PATCH] 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 | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index c3e89557..a74c7a90 100644 --- a/AGENTS.md +++ b/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