SilverSight/docs/FIX_DESIGN.md

# Fix Design: Exact Arithmetic & Codebook Corrections

**Date:** 2026-07-01
**Status:** Design + partial implementation
**Context:** Fixes for bugs found in independent review (Claude Fable)

## Problem Summary

The spectral codebook analysis had 3 classes of bugs:

1. **Power iteration non-convergence** — 22/250 matrices produce wrong eigenvalues
2. **Phinary packing not injective** — float accumulation loses precision
3. **Torus winding saturation** — Q16.16 clamps at n ≥ 65536

Plus 2 architectural improvements:

4. **Characteristic polynomial > spectral radius** as codebook key (192 vs 180 unique)
5. **Cartan gap Δ = 17/1792** as principled distinguishability floor (replaces 3× median heuristic)

## Fix 1: Exact Eigenvalue via Characteristic Polynomial (Lean)

### Approach

For an 8×8 integer matrix A, compute the characteristic polynomial:

    p(λ) = det(λI - A) = λ⁸ + c₇λ⁷ + ... + c₁λ + c₀

The coefficients cᵢ are integers (since A has integer entries). The spectral radius is the largest real root of p(λ).

### Implementation Plan

**File:** `formal/SilverSight/PIST/CharPoly.lean` (new)

```lean
-- Characteristic polynomial of an n×n integer matrix
-- Uses the Faddeev–LeVerrier algorithm: trace(A^k) → Newton identities → coefficients
-- All integer arithmetic, no floats.

def charPoly (n : Nat) (mat : Array (Array Int)) : Array Int :=
  -- Faddeev-LeVerrier: p_k = -(1/k) * (trace(A^k) + sum_{i=1}^{k-1} c_{k-i} * trace(A^i))
  -- Since we work in integers, multiply through by k! to avoid division
  sorry -- TODO: implement

-- Spectral radius from characteristic polynomial
-- Uses Newton's method on integer polynomial
def spectralRadiusFromCharPoly (coeffs : Array Int) : Q16_16 :=
  sorry -- TODO: implement

-- Cayley-Hamilton theorem: every matrix satisfies its own characteristic polynomial
theorem cayley_hamilton (n : Nat) (mat : Array (Array Int)) :
    -- p(A) = 0 (matrix polynomial evaluates to zero matrix)
    sorry -- TODO: prove
```

### Key Decision: Faddeev–LeVerrier vs Bareiss

- **Faddeev–LeVerrier:** Computes traces of powers (A, A², ..., Aⁿ), then uses Newton identities. Requires O(n⁴) integer operations. Natural for the existing `matVecMul`/`powerIteration` infrastructure.
- **Bareiss algorithm:** Fraction-free Gaussian elimination. O(n³) but requires careful pivot management.

**Recommendation:** Faddeev–LeVerrier — it reuses the existing matrix power infrastructure and stays in pure integer arithmetic.

### Integration

Replace `powerIteration` calls in `SpectralN.lean` with `spectralRadiusFromCharPoly ∘ charPoly`:

```lean
def computeSpectralExact (n : Nat) (mat : Array (Array Int)) : SpectralProfile n :=
  let coeffs := charPoly n mat
  let evMax := spectralRadiusFromCharPoly coeffs
  -- ... rest of profile from exact eigenvalue
```

Keep `powerIteration` for backward compatibility with existing proofs.

## Fix 2: Characteristic Polynomial as Codebook Key (Python)

### Current State

- `spectral_codebook_raw.json` uses float ρ from power iteration (180 unique, 22 wrong)
- `ClassifyN.hashTable8` uses base-5 matrix hash (proxy classifier)

### Proposed

**File:** `python/charpoly_codebook.py` (new)

```python
def charpoly_fingerprint(mat: list[list[int]]) -> tuple[int, ...]:
    """Exact characteristic polynomial coefficients as a hashable key.
    
    Uses numpy for computation, but the result is exact integer
    (characteristic polynomial of integer matrix has integer coefficients).
    """
    np_mat = np.array(mat, dtype=float)
    coeffs = np.poly(np_mat)  # Highest degree first
    # Round to integers (exact for integer matrices)
    return tuple(int(round(c)) for c in coeffs)

def build_codebook(matrices: dict[str, list[list[int]]]) -> dict:
    """Build spectral codebook from matrices.
    
    Key: characteristic polynomial (exact, integer)
    Value: list of equation IDs with that polynomial
    """
    codebook = defaultdict(list)
    for eid, mat in matrices.items():
        key = charpoly_fingerprint(mat)
        codebook[key].append(eid)
    return codebook
```

### Integration with ClassifyN

The Lean `hashTable8` should be extended to use charpoly-based classification:

```lean
-- In ClassifyN.lean
def classifyByCharPoly (n : Nat) (mat : Array (Array Int)) : Option String :=
  let coeffs := charPoly n mat
  charPolyTable coeffs  -- lookup table: charpoly → shape name
```

## Fix 3: Cartan Gap as Distinguishability Floor

### Current State

The `determineAlignment` function uses binary thresholds (0.5, 1.0) for classification. The codebook analysis uses "3× median gap" as cluster boundary.

### Proposed

The Cartan gap Δ = 17/1792 ≈ 0.00949 (proven in `CartanConnection.lean:70`) is the minimum eigenvalue of the crossing blocks. Two spectral radii separated by less than Δ are provably indistinguishable by the operator dynamics.

**File:** `formal/SilverSight/PIST/CodebookFloor.lean` (new)

```lean
import SilverSight.PIST.CartanConnection

-- The Cartan distinguishability floor
def cartanFloor : Q16_16 := Q16_16.ofRatio 17 1792

-- Two spectral radii are distinguishable iff their difference exceeds the Cartan floor
def distinguishable (lam1 lam2 : Q16_16) : Bool :=
  Q16_16.toInt (Q16_16.abs (Q16_16.sub lam1 lam2)) > cartanFloor.toInt

-- The codebook quantization rule: snap to nearest Cartan-multiple
def snapToCartanGrid (lam : Q16_16) : Q16_16 :=
  let grid := cartanFloor.toInt
  let raw := lam.toInt
  let snapped := ((raw + grid / 2) / grid) * grid
  Q16_16.ofRawInt snapped
```

**File:** `python/cartan_floor.py` (new)

```python
CARTAN_FLOOR = 17 / 1792  # ≈ 0.00949

def distinguishable(lam1: float, lam2: float) -> bool:
    return abs(lam1 - lam2) > CARTAN_FLOOR

def snap_to_cartan_grid(lam: float) -> float:
    return round(lam / CARTAN_FLOOR) * CARTAN_FLOOR
```

## Fix 4: Integer Spiral-Index Packing (Lean + Python)

### Current State

- Python `phi_corkscrew_index` uses float phinary packing (FIXED in cd91eca)
- Lean side uses `corkscrew_index` in `silversight_engine.py` (Python only)

### Proposed

The Lean side doesn't directly use phinary packing — it's in the Python engine. The fix in cd91eca (integer positional packing) is sufficient.

For the Lean side, the `HachimojiN8Bridge.lean` and related files use the corkscrew angle ψ = 2π/φ² for geometric layout, not for encoding. These don't need fixing.

## Implementation Order

1. **Fix 2 (Python charpoly codebook)** — quickest win, 192 unique keys immediately
2. **Fix 3 (Cartan floor)** — add as alternative to 3× median heuristic
3. **Fix 1 (Lean charpoly)** — substantial, but unlocks exact classification
4. **Fix 4 (already done)** — integer packing in cd91eca

## Open Questions

1. Should `ClassifyN.classifyExact` switch from `powerIteration` to `charPoly`? This would change all the `#eval` witnesses.
2. Should the Cartan floor replace the binary thresholds (0.5, 1.0) entirely, or run alongside them?
3. How to handle the 120 stale DB rows on neon-64gb? Reclassify with exact eigenvalues or mark as stale?