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)

-- 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:

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)

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:

-- 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)

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)

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?