allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
SilverSight/SORRY_PROTOCOL.md

13 KiB
Raw Permalink Blame History

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 3-agent rule: Every formula must be verified by 3 independent agents. All 3 must agree on every intermediate term and the final result to 6 decimal places. If any agent disagrees, the formula is a SORRY. STOP. Investigate. All 3 must agree before the formula is accepted.

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 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
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.         │
└──────────────────────────────────────┘

THE 3-AGENT VERIFICATION PROCESS

FORMULA CLAIMED
      │
      ▼
┌─────────────────────┐
│ Agent Alpha computes │  Independent. Shows all steps.
│ from scratch         │  Reports to 6 decimal places.
└──────────┬──────────┘
           │
      ┌────┴────┐
      ▼         ▼
┌─────────┐ ┌─────────┐
│ Agent   │ │ Agent   │  Independent. No sharing.
│ Beta    │ │ Gamma   │  Same formula, same inputs.
│ computes│ │ computes│  All steps shown.
│ scratch │ │ scratch │
└────┬────┘ └────┬────┘
     │            │
     └─────┬──────┘
           ▼
┌─────────────────────┐
│ Orchestrator compares│
│ all 3 results        │
└──────────┬──────────┘
           │
     ┌─────┴─────┐
     ▼           ▼
┌─────────┐ ┌─────────┐
│ ALL 3   │ │ ANY 2   │
│ AGREE   │ │ DISAGREE│
│         │ │         │
│ ✓ Log   │ │ ✗ STOP  │
│ ✓ Accept│ │ ✗ Find  │
│ ✓ Proceed│ │   error │
│         │ │ ✗ Recomp│
└─────────┘ └─────────┘

Agreement means: Every intermediate term matches to 6 decimal places. The final result matches to 6 decimal places. No rounding differences. No off-by-one in indices. Exact match.

Disagreement means: Any intermediate term or final result differs by more than 10^{-6}. STOP. All 3 agents recompute. If disagreement persists, the formula is a SORRY. Apply the STOP protocol.

VERIFICATION LOG (formulas verified)

# Formula Inputs Consensus Value Date Status
001 d_F(p,q) = 2·arccos(Σ√(pᵢqᵢ)) p=(0.3,0.1,0.15,0.05,0.2,0.08,0.07,0.05), q=(0.2,0.2,0.1,0.1,0.15,0.1,0.1,0.05) 0.440258 2026-06-23 ✅ VERIFIED

See VERIFICATION_LOG.md for full details.

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.