mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
docs(sorry-protocol): sorry = STOP. No exceptions. No smuggling.
This commit is contained in:
Allaun Silverfox
parent
ef9285f90a
commit
ee7544dc0c
1 changed files with 293 additions and 0 deletions
293
SORRY_PROTOCOL.md
Normal file
293
SORRY_PROTOCOL.md
Normal file
|
|
@ -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.
|
||||
Loading…
Add table
Reference in a new issue