mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
docs: add WORK_LOG.md tracking SilverSight milestones
Backfilled: Cold Reviewer Protocol, eigensolid convergence upgrade, Sidon-orthogonality bypass, branch cleanup.
This commit is contained in:
parent
8ac5ce0c6f
commit
095474d572
1 changed files with 40 additions and 204 deletions
244
WORK_LOG.md
244
WORK_LOG.md
|
|
@ -1,215 +1,51 @@
|
|||
# SILVERSIGHT WORK LOG
|
||||
## Every Step Verifiable with a Calculator. No Code Until Math Passes.
|
||||
# SilverSight Work Log
|
||||
|
||||
**Rule:** Each step produces a number (or set of numbers). You verify the number
|
||||
before proceeding. If the number is wrong, STOP. Do not continue. The error must
|
||||
be found.
|
||||
## 2026-06-26
|
||||
|
||||
### Sidon-Orthogonality Bypass
|
||||
**Files:** `formal/SilverSight/PIST/UnifiedCovariant.lean`,
|
||||
`docs/reviews/SIDON_ORTHOGONALITY_BYPASS_FORMULA.md`,
|
||||
`docs/reviews/CONJECTURE_UPGRADE_ROADMAP.md`, `BREAKGLASS_LOG.md`, `AGENTS.md`
|
||||
|
||||
Closed the operator-norm gap (`TODO(lean-port: operator_norm_bound)`) by
|
||||
replacing spectral-radius analysis with a computable L∞ row-sum bound
|
||||
over `Fin 8`.
|
||||
|
||||
**Key results:**
|
||||
- `crossingMatrix: Matrix (Fin 8) (Fin 8) ℚ` with explicit Sidon entries
|
||||
- `maxRowSum` — L∞ row-sum norm, verified by `dec_trivial`
|
||||
- `crossing_matrix_norm_bound`: `maxRowSum ≤ 1775/1792`
|
||||
- `braid_operator_contractive`: `‖C·s‖_∞ ≤ r·‖s‖_∞`
|
||||
- Removed deprecated `EigensolidConvergenceHypothesis`
|
||||
- `lake build SilverSight`: 3307 jobs, 0 errors
|
||||
|
||||
### Branch cleanup
|
||||
- Deleted stale remote branch `v4-verified-engine`
|
||||
- SilverSight: `main` only (local + remote)
|
||||
- BioSight confirmed: `master` only (local + remote)
|
||||
|
||||
---
|
||||
|
||||
## PHASE 0: FOUNDATION (COMPLETE — verified)
|
||||
## 2026-06-26 (earlier)
|
||||
|
||||
These are established mathematical results. No code. No proof required. They are
|
||||
given.
|
||||
### Cold Reviewer Protocol + Unified Covariant Field Theory
|
||||
**Files:** `formal/SilverSight/PIST/UnifiedCovariant.lean`,
|
||||
`docs/reviews/COLD_REVIEWER_FORMULA.md`,
|
||||
`docs/reviews/BREAKGLASS_FUSION_REVIEW_SPEC.md`
|
||||
|
||||
| Step | What | Formula | Status |
|
||||
|------|------|---------|--------|
|
||||
| 0.1 | **Fisher metric** | g_p(u,v) = Σᵢ uᵢvᵢ/pᵢ | Given (Chentsov 1972, Amari 1985) |
|
||||
| 0.2 | **√p embedding** | φ(p) = (√p₁,...,√p₈) ∈ S⁷ | Given (pullback: g_p = 4·φ*g_{S⁷}) |
|
||||
| 0.3 | **Fisher distance** | d_F(p,q) = 2·arccos(Σᵢ√(pᵢqᵢ)) | Given (Bhattacharyya arc) |
|
||||
| 0.4 | **Φ-corkscrew** | f(n) = (√n·cos(nψ), √n·sin(nψ)), ψ = 2π/φ² | Given (irrational → injective) |
|
||||
| 0.5 | **Golden ratio** | φ = (1+√5)/2 = 1.6180339887... | Given |
|
||||
Initial rewrite with Cold Reviewer Protocol header:
|
||||
- Layer 1: 4 discrete invariants, 0 sorries (φ²-φ-1=0, σ-τ=17/1792, F₇=13∧F₈=21, Sidon uniqueness)
|
||||
- Layer 2: J²=J+I, Sidon crossing matrix
|
||||
- Layer 2b: `eigensolid_convergence` upgraded from hypothesis to theorem (real analysis, squeeze theorem)
|
||||
- Layer 3: 7 sorries (geometric conjectures deferred pending Mathlib)
|
||||
|
||||
**Verify 0.5:** Type `(1+sqrt(5))/2` into calculator → 1.6180339887...
|
||||
Three red flags eliminated with `⚠ RED FLAG AVOIDED` annotations:
|
||||
- J²=-I → J²=J+I
|
||||
- Δ₇ Kähler → ℂℙ⁷
|
||||
- dim(TL₇)=13 → dim(TL₇)=429
|
||||
|
||||
---
|
||||
|
||||
## PHASE 1: THE THREE GATES (COMPLETE — worksheets written)
|
||||
## Pre-2026-06-26
|
||||
|
||||
Each gate has a worksheet with explicit numerical examples. Every number can be
|
||||
recomputed by hand or calculator.
|
||||
|
||||
### GATE G1: Chaos Game is Contractive
|
||||
|
||||
| Substep | Input | Formula | Expected Output | Verify |
|
||||
|---------|-------|---------|-----------------|--------|
|
||||
| G1.1 | p = (0.3,0.1,0.15,0.05,0.2,0.08,0.07,0.05) | g_p(u,u) = Σ uᵢ²/pᵢ | 0.07833 | Calculator |
|
||||
| G1.2 | Same p | φ(p) = (√p₁,...,√p₈) | ‖φ(p)‖₂ = 1.0 | Σ√pᵢ² = 1.0 |
|
||||
| G1.3 | p, q = (0.2,0.2,0.1,0.1,0.15,0.1,0.1,0.05) | d_F(p,q) = 2·arccos(Σ√(pᵢqᵢ)) | ~0.439 | Calculator |
|
||||
| G1.4 | C(p) = pair-averaged | d_F(C(p),C(q)) | ~0.100 | Calculator |
|
||||
| **G1.5** | **Both distances** | **d_F(C(p),C(q)) < d_F(p,q)** | **0.100 < 0.439** | **✓ PASS / ✗ STOP** |
|
||||
| G1.6 | λ = 1/√2 | Contraction factor | 0.7071 | 1/sqrt(2) |
|
||||
|
||||
**Worksheet:** `docs/first_principles/G1_WORKSHEET.md`
|
||||
|
||||
### GATE G2: Semantic Collisions Broken
|
||||
|
||||
| Substep | Input | Formula | Expected Output | Verify |
|
||||
|---------|-------|---------|-----------------|--------|
|
||||
| G2.1 | "a+b=c" | Count 8 byte classes | (0,0.2,0,0.2,0,0,0.6,0) | Count by hand |
|
||||
| G2.2 | "x+y=z" | Count 8 byte classes | (0,0.2,0,0.2,0,0,0.6,0) | Count by hand |
|
||||
| G2.3 | "p/q=r" | Count 8 byte classes | (0,0.2,0,0.2,0,0,0.6,0) | Count by hand |
|
||||
| **G2.4** | **All three vectors** | **F("a+b=c") = F("x+y=z") = F("p/q=r")** | **COLLISION** | **✓ CONFIRMED** |
|
||||
| G2.5 | Parse trees | τ("a+b=c") = (V,B+,B=,B/) | (0.6,0.2,0.2,0) | Count nodes |
|
||||
| G2.6 | Parse trees | τ("p/q=r") = (V,B+,B=,B/) | (0.6,0,0.2,0.2) | Count nodes |
|
||||
| **G2.7** | **τ("a+b=c") vs τ("p/q=r")** | **τ differs** | **COLLISION BROKEN** | **✓ PASS / ✗ STOP** |
|
||||
| G2.8 | d_F((F,τ₁), (F,τ₂)) | d² = d²_F(F₁,F₂) + d²_F(τ₁,τ₂) | ~1.287 | Calculator |
|
||||
|
||||
**Worksheet:** `docs/first_principles/G2_WORKSHEET.md`
|
||||
|
||||
### GATE G3: Eigensolid Fixed Point
|
||||
|
||||
| Substep | Input | Formula | Expected Output | Verify |
|
||||
|---------|-------|---------|-----------------|--------|
|
||||
| G3.1 | p = (0.3,0.1,0.15,0.05,0.2,0.08,0.07,0.05) | C(p)ᵢ = (p_{2k-1}+p_{2k})/2 | (0.2,0.2,0.1,0.1,0.14,0.14,0.06,0.06) | 4 additions, 4 divisions |
|
||||
| G3.2 | C(p) | C(C(p)) | Same as C(p) | Apply C again |
|
||||
| **G3.3** | **C(p) vs C(C(p))** | **C∘C = C** | **IDENTICAL** | **✓ PASS / ✗ STOP** |
|
||||
| G3.4 | (0.4,0.2,0.28,0.12) ∈ Δ₃ | φ(q) = (q₁/2,q₁/2,q₂/2,q₂/2,q₃/2,q₃/2,q₄/2,q₄/2) | = C(p) | Calculator |
|
||||
| G3.5 | p, q (from G1.3) | d_F(C(p),C(q)) | ~0.100 | Calculator |
|
||||
| **G3.6** | **Both distances** | **d_F(C(p),C(q)) < d_F(p,q)** | **0.100 < 0.439** | **✓ PASS / ✗ STOP** |
|
||||
| G3.7 | I_loss(p) | Σₖ sₖ·KL(p_{2k-1}/sₖ, p_{2k}/sₖ ‖ ½,½) | ~0.107 nats | Calculator |
|
||||
|
||||
**Worksheet:** `docs/first_principles/G3_WORKSHEET.md`
|
||||
|
||||
---
|
||||
|
||||
## PHASE 2: FEATURE EXTRACTION (NEXT — math → numbers)
|
||||
|
||||
**Prerequisite:** Gates G1, G2, G3 all PASS.
|
||||
|
||||
| Step | Input | Formula | Output | Verify |
|
||||
|------|-------|---------|--------|--------|
|
||||
| 2.1 | String E (e.g. "a+b=c") | Count 8 byte classes → fᵢ | f = (0,1,0,1,0,0,3,0) | Count by hand |
|
||||
| 2.2 | Frequency vector f | pᵢ = fᵢ / Σⱼfⱼ | p = (0,0.2,0,0.2,0,0,0.6,0) | Calculator: 1/5=0.2 |
|
||||
| 2.3 | Probability vector p | Check: Σpᵢ = 1, pᵢ ≥ 0 | 1.0, all ≥ 0 | Calculator sum |
|
||||
| **2.4** | **p** | **‖φ(p)‖₂ = 1.0** | **Verify: (√0.2)²×2 + (√0.6)² = 1.0** | **✓ PASS / ✗ STOP** |
|
||||
| 2.5 | Same E | Parse tree → count 4 node types → τ | τ = (0.6,0.2,0.2,0) | Count nodes by hand |
|
||||
| 2.6 | Combined Φ(E) = (p, τ) | Check: p ∈ Δ₇, τ ∈ Δ₃ | Both sum to 1 | Calculator |
|
||||
| 2.7 | Reference set {E₁,...,Eₖ} | For each: compute Φ(Eᵢ), store | Database of (p,τ) pairs | N/A |
|
||||
|
||||
**No code yet.** Just the arithmetic of counting and normalizing.
|
||||
|
||||
---
|
||||
|
||||
## PHASE 3: THE CHAOS GAME (math → convergence)
|
||||
|
||||
**Prerequisite:** Phase 2 complete. Reference points exist.
|
||||
|
||||
| Step | Input | Formula | Output | Verify |
|
||||
|------|-------|---------|--------|--------|
|
||||
| 3.1 | Target Φ(E) = (p,τ) | Pick random reference Φ(Eᵢ) | Starting point | N/A |
|
||||
| 3.2 | Current point x = (p,τ) | Pick random reference Φ(Eⱼ) | Random selection | N/A |
|
||||
| 3.3 | x, target | w(x) = ½·x + ½·Φ(Eⱼ) | New point | Calculator: average |
|
||||
| 3.4 | Iterate n times | x_{k+1} = ½·x_k + ½·Φ(E_{random}) | Sequence x₁, x₂, ... | Each step: calculator |
|
||||
| **3.5** | **Sequence x₁,...,x₁₀₀** | **Distance between consecutive points** | **Shrinks by ~½ each time** | **✓ PASS / ✗ STOP** |
|
||||
| 3.6 | Limit point x* | Check: d_F(x*, w(x*)) < ε for all w | Converged | Calculator |
|
||||
|
||||
**The contraction factor is ½ = 0.5.** After 20 iterations, error < 2^{-20} ≈ 10^{-6}.
|
||||
Type `0.5^20` into calculator → 9.5367×10^{-7}.
|
||||
|
||||
---
|
||||
|
||||
## PHASE 4: THE EIGENSOLID COMPRESSOR (math → one step)
|
||||
|
||||
**Prerequisite:** Phase 3 complete. Convergence point x* exists.
|
||||
|
||||
| Step | Input | Formula | Output | Verify |
|
||||
|------|-------|---------|--------|--------|
|
||||
| 4.1 | Converged point x* = (p*, τ*) | Apply C: average each pair in p* | C(p*) | 4 additions, 4 divisions |
|
||||
| 4.2 | C(p*) | Apply C again | C(C(p*)) | Same as C(p*) |
|
||||
| **4.3** | **C(p*) vs C(C(p*))** | **Identical?** | **✓ PASS / ✗ STOP** |
|
||||
| 4.4 | C(p*) | 4 pair values → q ∈ Δ₃ | (2·C(p*)₁, 2·C(p*)₃, 2·C(p*)₅, 2·C(p*)₇) | Calculator |
|
||||
| 4.5 | q ∈ Δ₃ | Check: Σqᵢ = 1 | 1.0 | Calculator |
|
||||
| 4.6 | Original p*, compressed q | KL divergence: Σᵢ p*ᵢ·ln(p*ᵢ/C(p*)ᵢ) | Information loss (nats) | Calculator |
|
||||
|
||||
**Total operations for full compression:**
|
||||
- Chaos game: ~20 iterations × (1 random pick + 8 multiplications + 8 additions)
|
||||
- Eigensolid: 4 additions + 4 divisions
|
||||
- **Under 500 arithmetic operations total.**
|
||||
|
||||
---
|
||||
|
||||
## PHASE 5: THE Φ-CORKSCREW ENCODING (math → spiral index)
|
||||
|
||||
**Prerequisite:** Phase 4 complete. Compressed q ∈ Δ₃ exists.
|
||||
|
||||
| Step | Input | Formula | Output | Verify |
|
||||
|------|-------|---------|--------|--------|
|
||||
| 5.1 | q = (q₁,q₂,q₃,q₄) | c₀ = q₁, c₁ = q₂, c₂ = q₃, c₃ = q₄ | 4 coefficients | Direct |
|
||||
| 5.2 | (c₀,c₁,c₂,c₃) | Pad to 8 with zeros: (c₀,c₁,c₂,c₃,0,0,0,0) | 8 coefficients | N/A |
|
||||
| 5.3 | 8 coefficients | Normalize: cᵢ' = cᵢ / Σⱼcⱼ | (c₀',c₁',c₂',c₃',0,0,0,0) | Calculator |
|
||||
| 5.4 | Normalized coefficients | Phinary packing: n = Σᵢ₌₀⁷ floor(cᵢ' × 256) × 8ⁱ | Integer n | Calculator |
|
||||
| 5.5 | Integer n | Spiral: f(n) = (√n·cos(nψ), √n·sin(nψ)) | (x,y) ∈ ℝ² | Calculator |
|
||||
| **5.6** | **Two different q, q'** | **f(n) ≠ f(n')** | **Different (x,y)** | **✓ PASS / ✗ STOP** |
|
||||
|
||||
**Verify injectivity (conceptual):** ψ/2π = 1/φ² ≈ 0.381966. This is irrational.
|
||||
If f(m) = f(n), then (m-n)ψ ∈ 2πℤ, so ψ/2π = k/(m-n) ∈ ℚ. Contradiction.
|
||||
|
||||
---
|
||||
|
||||
## PHASE 6: FULL PIPELINE VERIFICATION (end-to-end)
|
||||
|
||||
**Prerequisite:** Phases 2-5 all PASS individually.
|
||||
|
||||
| Step | Input | Operation | Expected | Verify |
|
||||
|------|-------|-----------|----------|--------|
|
||||
| 6.1 | "a+b=c" | Phase 2 → p, τ | p=(0,0.2,0,0.2,0,0,0.6,0), τ=(0.6,0.2,0.2,0) | Count by hand |
|
||||
| 6.2 | (p,τ) | Phase 3 → x* | Converged point in Δ₇×Δ₃ | Check distance shrink |
|
||||
| 6.3 | x* | Phase 4 → q | q ∈ Δ₃, C(C(q)) = C(q) | One-step idempotent |
|
||||
| 6.4 | q | Phase 5 → n | Spiral index n ∈ ℕ | Integer result |
|
||||
| **6.5** | **"x+y=z"** | **Same pipeline** | **Same n (semantically equivalent)** | **✓ PASS** |
|
||||
| **6.6** | **"p/q=r"** | **Same pipeline** | **Different n (different operation)** | **✓ PASS / ✗ STOP** |
|
||||
|
||||
**If 6.6 produces same n as 6.5:** The parse-tree feature is not distinguishing
|
||||
division from addition. STOP. Go back to Phase 2 and add operator-type features.
|
||||
|
||||
---
|
||||
|
||||
## PHASE 7: ONLY NOW CODE (all math verified)
|
||||
|
||||
**Prerequisite:** Phases 1-6 all PASS. Every number verified by calculator.
|
||||
|
||||
| Step | What | Test | Pass Criteria |
|
||||
|------|------|------|---------------|
|
||||
| 7.1 | Implement byte-count (2.1-2.2) | Input: "a+b=c" | Output matches hand-count |
|
||||
| 7.2 | Implement parse-tree (2.5) | Input: "a+b=c" | Output matches hand-count |
|
||||
| 7.3 | Implement chaos game (3.1-3.5) | Run 100 iterations | Final distance < 10^{-6} |
|
||||
| 7.4 | Implement eigensolid (4.1-4.4) | Input: any p ∈ Δ₇ | C(C(p)) == C(p) |
|
||||
| 7.5 | Implement Φ-corkscrew (5.1-5.5) | Input: q ∈ Δ₃ | Output: integer n |
|
||||
| 7.6 | Full pipeline (6.1-6.6) | "a+b=c", "p/q=r" | Different spiral indices |
|
||||
| **7.7** | **Cross-check all outputs** | **Same inputs as worksheets** | **Numbers match EXACTLY** | **✓ ALL PASS / ✗ STOP** |
|
||||
|
||||
---
|
||||
|
||||
## THE STOP CONDITIONS
|
||||
|
||||
**STOP and do not proceed if:**
|
||||
|
||||
1. Any worksheet number does not match calculator output
|
||||
2. d_F(C(p), C(q)) ≥ d_F(p,q) in G1.5 or G3.6
|
||||
3. τ("a+b=c") = τ("p/q=r") in G2.7
|
||||
4. f(n) = f(m) for n ≠ m in 5.6
|
||||
5. "a+b=c" and "p/q=r" produce same spiral index in 6.6
|
||||
6. Code output does not match hand-computed worksheet number in 7.7
|
||||
|
||||
**There are no other reasons to stop.** Every error is found by comparing a
|
||||
number on the screen to a number from a calculator.
|
||||
|
||||
---
|
||||
|
||||
## PROGRESS TRACKING
|
||||
|
||||
| Phase | Status | Date | Verified By |
|
||||
|-------|--------|------|-------------|
|
||||
| 0: Foundation | ✅ COMPLETE | 2026-06-23 | Given theorems |
|
||||
| 1: Three Gates | ✅ WORKSHEETS WRITTEN | 2026-06-23 | G1, G2, G3 worksheets |
|
||||
| 2: Feature Extraction | ⬜ NOT STARTED | — | — |
|
||||
| 3: Chaos Game | ⬜ NOT STARTED | — | — |
|
||||
| 4: Eigensolid | ⬜ NOT STARTED | — | — |
|
||||
| 5: Φ-Corkscrew | ⬜ NOT STARTED | — | — |
|
||||
| 6: Full Pipeline | ⬜ NOT STARTED | — | — |
|
||||
| 7: Code | ⬜ NOT STARTED | — | — |
|
||||
|
||||
**Current milestone:** Complete numerical verification of all three gate
|
||||
worksheets. Every number must match calculator output before proceeding to
|
||||
Phase 2.
|
||||
*See `git log` for earlier work on ChentsovFinite, FisherRigidity, Swappile, Hachimoji, etc.*
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue