From ee7544dc0c82c39e48df6d6ad6caef1e0ad2747a Mon Sep 17 00:00:00 2001 From: Allaun Silverfox <28494262+allaunthefox@users.noreply.github.com> Date: Tue, 23 Jun 2026 05:34:23 -0500 Subject: [PATCH] docs(sorry-protocol): sorry = STOP. No exceptions. No smuggling. --- SORRY_PROTOCOL.md | 293 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 293 insertions(+) create mode 100644 SORRY_PROTOCOL.md diff --git a/SORRY_PROTOCOL.md b/SORRY_PROTOCOL.md new file mode 100644 index 00000000..758ceb16 --- /dev/null +++ b/SORRY_PROTOCOL.md @@ -0,0 +1,293 @@ +# THE SORRY PROTOCOL +## A sorry is a STOP sign. Not a TODO. Not a placeholder. A full project halt. + +**Definition:** A `sorry` is any gap between what is claimed and what is proven. +This includes Lean's `sorry`, unproven lemmas, unstated hypotheses, hand-waving, +"obviously", "it follows that", and any step where the reader must trust the +author rather than verify the arithmetic. + +**The rule:** Encounter a sorry → STOP → Assess → Decide → Only then proceed. + +--- + +## THE STOP PROTOCOL + +``` +SORRY DETECTED + │ + ▼ +┌─────────────┐ +│ 1. STOP │ Halt all work on this path immediately. +│ │ No code. No lemmas. No further steps. +└──────┬───────┘ + │ + ▼ +┌─────────────┐ +│ 2. DOCUMENT │ Write down exactly what is missing: +│ │ - The exact statement that needs proof +│ │ - What was assumed instead of proven +│ │ - Why the original author thought it worked +└──────┬───────┘ + │ + ▼ +┌─────────────┐ +│ 3. ASSESS │ Three options only: +│ │ +│ (A) CAN PROVE NOW +│ ↓ The statement is true and you can prove it +│ ↓ Write the proof. No shortcuts. Every step verifiable. +│ ↓ Only then proceed. +│ +│ (B) CAN PROVE LESS +│ ↓ The full statement is too strong +│ ↓ Weaken it to what IS provable +│ ↓ Change the theorem, not the proof attempt +│ ↓ Example: "unique" → "invariant" if uniqueness needs more +│ +│ (C) CANNOT PROVE — ABANDON PATH +│ ↓ The statement may be false or requires unknown math +│ ↓ Mark the path as UNPROVEN +│ ↓ Do not build code on this path +│ ↓ Do not cite this result +│ ↓ Find a different path that bypasses this result +└──────┬───────┘ + │ + ▼ +┌─────────────┐ +│ 4. VERIFY │ The chosen resolution must itself be verified: +│ │ - Proof: checkable by independent reader +│ │ - Weakened theorem: calculator-verified example +│ │ - Abandoned: documented with reason +└──────┬───────┘ + │ + ▼ +┌─────────────┐ +│ 5. PROCEED │ Only after step 4 passes. +│ │ The sorry is resolved. Log the resolution. +└─────────────┘ +``` + +--- + +## WHAT COUNTS AS A SORRY + +### Explicit sorries (Lean) +- `sorry` — tactic that fills any proof obligation +- `admit` — same as sorry +- `stop` — abandoned proof + +### Implicit sorries (text) +- "It is clear that..." — if it needs saying, it needs proving +- "By standard arguments..." — which arguments? write them down +- "One can show..." — either show it or don't claim it +- "The proof is analogous to..." — analogy is not proof +- "Numerical evidence suggests..." — evidence is not proof +- Any step where a calculator cannot verify the number + +### Structural sorries (design) +- Axiom used where theorem needed +- `native_decide` where proof needed +- `partial` definition where totality needed +- Unstated hypothesis in theorem statement +- Type that is too permissive (allows invalid states) + +--- + +## RESOLUTION OPTIONS — DETAILED + +### OPTION A: PROVE IT + +**When:** The statement is true and within current capability. + +**Requirements:** +1. Every step is a formula or a reference to a proven result +2. No English where a formula suffices +3. Every number can be verified on a calculator +4. The proof is complete — no nested sorries +5. An independent reader can verify without asking questions + +**Log entry:** +``` +SORRY RESOLVED: PROVEN +Location: [file, line number] +Original: [statement with sorry] +Proof: [complete proof text] +Verified by: [name, date, method] +``` + +--- + +### OPTION B: WEAKEN THE THEOREM + +**When:** The statement is too strong but a weaker version is provable. + +**Method:** +1. State the strongest version you CAN prove +2. Remove adjectives: "unique" → "exists", "all" → "some", "for every" → "for this class" +3. Add hypotheses that make it provable +4. Never keep the strong statement with a weak proof + +**Example — Chentsov:** +``` +ORIGINAL (UNPROVEN): The Fisher metric is the UNIQUE Chentsov-invariant metric. + +WEAKENED (PROVEN): The Fisher metric is invariant under sufficient-statistic + coarse-graining (Chentsov condition). + + Uniqueness requires additional proof that any invariant + metric satisfies the functional equation H(t) = c/t. + This is OPEN. +``` + +**Log entry:** +``` +SORRY RESOLVED: WEAKENED +Location: [file, line number] +Original: [full statement] +Weakened to: [new statement] +Proof: [complete proof of weakened version] +What remains open: [exact gap] +``` + +--- + +### OPTION C: ABANDON THE PATH + +**When:** The statement requires math that does not exist, is likely false, +or is beyond current capability. + +**Method:** +1. Clearly mark the path as UNPROVEN +2. Document what was tried and why it failed +3. Do not write code that depends on this result +4. Find an alternative path that achieves the goal without this result + +**Example — NP-hard smuggling:** +``` +ORIGINAL CLAIM: NP-hard problems can be solved via DNA sort. + +STATUS: ABANDONED +Reason: The reduction requires exponential preprocessing. The total work + (preprocessing + sort) exceeds brute force. This is a lower bound + result, not an algorithm. + +ALTERNATIVE PATH: Resumable chunked computation for tensor network + contraction. This is a heuristic, not a complexity result. + It does not claim to solve NP-hard problems. +``` + +**Log entry:** +``` +SORRY RESOLVED: ABANDONED +Location: [file, line number] +Original claim: [full statement] +Reason: [why it cannot be proven now] +Attempted: [what was tried] +Alternative: [different path to the goal] +``` + +--- + +## SORRY INVENTORY + +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 | +| 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 | +| S7 | BraidSpherionBridge | Receipt bijection claim | STOP | Tautology — WEAKEN or ABANDON | +| S8 | finsler_metric.py | F is a Finsler metric | STOP | FALSE — RENAME or PROVE it is not | +| S9 | RESUMABLE_DAG_MODEL.md | Solves NP-hard problems | STOP | FALSE — ABANDON claim | +| S10 | spectral_profile.py | Semantically collision-free | STOP | FALSE — ADD features (G2) | + +**Rule:** A sorry stays in this table until resolved. No code is written for +paths that depend on unresolved sorries. + +--- + +## THE CLEAN BOUNDARY + +**PROVEN TERRITORY (code allowed):** +- Fisher metric formula and S⁷ embedding +- Φ-corkscrew injectivity +- Chaos game contraction (for specific IFS) +- Eigensolid projection (idempotent, one-step) +- Byte-frequency map E → Δ₇ (well-defined, not injective) +- Parse-tree map E → Δ₃ (well-defined, breaks some collisions) +- Product Fisher metric on Δ₇ × Δ₃ + +**UNPROVEN TERRITORY (no code):** +- Fisher metric uniqueness (S1-S3) +- Full chaos game convergence proof (needs IFS contraction proof) +- Complete collision-freedom (needs more features) +- Eigensolid convergence characterization (native_decide used) +- Finsler structure of distance function +- Any complexity claims +- Any cryptographic security claims without proofs + +**THE WALL:** Nothing crosses from UNPROVEN to PROVEN without: +1. A complete proof with no sorries +2. Verification by calculator or independent reader +3. Log entry documenting the resolution + +--- + +## CURRENT STATUS + +``` +PROVEN: UNPROVEN: +├── Fisher metric ├── Chentsov uniqueness (S1-S3) +├── S⁷ embedding ├── 7 axioms (S4) +├── Fisher distance ├── Hermite sieve (S5) +├── Φ-corkscrew injectivity├── Eigensolid convergence (S6) +├── Contraction (G1) ├── Receipt bijection (S7) +├── Collision break (G2) ├── Finsler claim (S8) +├── Eigensolid fixed (G3) ├── NP-hard claim (S9) +└── Product metric └── Spectral collisions (S10) + +The wall: +┌──────────────────────────────────────┐ +│ NO CODE for anything depending on │ +│ S1-S10 until they are resolved. │ +│ │ +│ Current code in UNPROVEN territory │ +│ must be flagged or removed. │ +└──────────────────────────────────────┘ +``` + +--- + +## NEXT ACTIONS + +1. **Resolve S1-S3 (Chentsov):** WEAKEN theorem to invariance only. Write the + weakened proof. Log as resolved. + +2. **Resolve S4 (7 axioms):** MARK each as `conjecture` not `axiom`. Remove + any code that assumes them as true. Log as resolved (weakened). + +3. **Resolve S5 (14 sorries):** ASSESS each individually. Some may be provable + (Option A), some need weakening (Option B), some need abandoning (Option C). + +4. **Resolve S6 (native_decide):** STATE clearly: "verified by computation for + 8 cases, not proven for all cases." This is honest. Log as resolved (weakened). + +5. **Resolve S7 (receipt bijection):** The statement is a tautology. WEAKEN to + "receipt encodes specific fields, injectivity on those fields." Log as resolved. + +6. **Resolve S8 (Finsler):** RENAME to "distance-like function." The code + computes a distance, not a Finsler metric. Log as resolved (weakened). + +7. **Resolve S9 (NP-hard):** ABANDON. Replace with "heuristic chunking." Log + as resolved. + +8. **Resolve S10 (collisions):** PROVEN that G2 breaks operator-type collisions. + Variable-name collisions are semantically equivalent — this is correct behavior. + Log as resolved (the feature is sufficient). + +**After all 10 resolved:** The wall moves. Code can be written for newly proven +theorems. The work log (WORK_LOG.md) governs which phase to enter next.