allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-30 17:16:16 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

docs(sorry-protocol): S1-S3 marked RESOLVED WEAKENED — Chentsov uniqueness → invariance

Browse source
This commit is contained in:
Allaun Silverfox 2026-06-23 06:00:46 -05:00
parent 4e50dbba6d
commit 1f11edc7a9
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
SORRY_PROTOCOL.md
View file

@ -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 |