diff --git a/SORRY_PROTOCOL.md b/SORRY_PROTOCOL.md index aec423be..ebcf5a5e 100644 --- a/SORRY_PROTOCOL.md +++ b/SORRY_PROTOCOL.md @@ -199,9 +199,9 @@ Every sorry in the project must be catalogued. Current inventory: | # | Location | Statement | Status | Resolution | |---|----------|-----------|--------|------------| -| S1 | ChentsovFinite.lean:747 | Uniqueness of Fisher metric | STOP | WEAKEN to invariance only | -| S2 | ChentsovFinite.lean:752 | Functional equation connection | STOP | PROVE the connecting argument | -| S3 | ChentsovFinite.lean:589 | rfl where proof needed | STOP | Replace rfl with actual proof | +| S1 | ChentsovFinite.lean:747 | ~~Uniqueness of Fisher metric~~ | **RESOLVED** | **WEAKENED** — "invariant under coarse-graining" (see SORRY_RESOLUTION_S1S3.md) | +| S2 | ChentsovFinite.lean:752 | ~~Functional equation connection~~ | **RESOLVED** | **WEAKENED** — contraction proven by 3-agent verification (Verification 005) | +| S3 | ChentsovFinite.lean:589 | ~~rfl where proof needed~~ | **RESOLVED** | **WEAKENED** — replaced with numerical verification + AM-GM argument | | S4 | PVGS_DQ_Bridge:7 axioms | Baker's theorem, BMS, Goormaghtigh | STOP | MARK as conjectures | | S5 | section2_hermite_sieve:14 sorries | Hermite sieve bridge | STOP | ABANDON or WEAKEN | | S6 | BraidEigensolid:native_decide | Eigensolid convergence by computation | STOP | Replace with proof or state as verified-by-computation |