diff --git a/formal/CoreFormalism/CharacterTransform.lean b/formal/CoreFormalism/CharacterTransform.lean
index e997952c..f164df10 100644
--- a/formal/CoreFormalism/CharacterTransform.lean
+++ b/formal/CoreFormalism/CharacterTransform.lean
@@ -1,96 +1,74 @@
 /- SilverSight: Character Transform — Complete Proof Chain
    Connects Sidon labels → Z₂⁴ character group → Cartan matrix → spectral gap.
-   All integer arithmetic, zero floats. -/
+   All integer arithmetic, zero floats. 0 sorries, 0 axioms. -/
 
 import Formal.CoreFormalism.SidonSets
-import Formal.CoreFormalism.BraidStateN
+import Mathlib.Tactic
 
 namespace SilverSight.CharacterTransform
 
-open SilverSight.BraidStateN
+open Finset
 
 -- ── §1: Sidon Labels ──────────────────────────────────────────────
 
-/-- The canonical Sidon set for n=8: powers of 2. All pairwise sums unique. -/
 def sidonLabels8 : Finset ℤ := {1, 2, 4, 8, 16, 32, 64, 128}
 
 theorem sidonLabels8_is_sidon : IsSidon sidonLabels8 := by
-  -- 8 elements → 8⁴ = 4096 quadruples → native_decide handles this
-  native_decide
+  unfold IsSidon sidonLabels8
+  decide
 
 -- ── §2: Z₂⁴ Character Matrix ────────────────────────────────────
 
-/-- Character vector for strand i. Maps each of the 4 crossing pairs to ±1. -/
 def charVec (i : Fin 8) (k : Fin 4) : ℤ :=
-  let pairIdx := i.val / 2
-  if pairIdx = k.val then
-    if i.val % 2 = 0 then 1 else -1
-  else 0
+  if i.val / 2 = k.val then (if i.val % 2 = 0 then 1 else -1) else 0
 
-/-- The character matrix: 8 strands × 4 crossing pairs, all entries in {-1, 0, 1}. -/
 theorem charVec_range (i : Fin 8) (k : Fin 4) : charVec i k ≥ -1 ∧ charVec i k ≤ 1 := by
-  unfold charVec
-  split <;> split <;> norm_num
+  unfold charVec; split <;> split <;> omega
 
 -- ── §3: Cartan Gram Matrix ────────────────────────────────────────
 
-/-- Gram product of character vectors: G[i][j] = Σₖ charVec(i,k) × charVec(j,k). -/
 def cartanGram (i j : Fin 8) : ℤ :=
-  Finset.sum Finset.univ (λ k => charVec i k * charVec j k)
+  ∑ k : Fin 4, charVec i k * charVec j k
 
-/-- Self-inner product: G[i][i] = 4 (each strand is in exactly one pair, norm = 1). -/
 theorem gram_self (i : Fin 8) : cartanGram i i = 1 := by
-  unfold cartanGram charVec
-  -- Sum over 4 crossing pairs; only the pair containing i contributes
-  have h : (Finset.filter (λ k => (i.val / 2 = k.val)) Finset.univ).card = 1 := by
-    decide
-  native_decide
+  unfold cartanGram charVec; fin_cases i <;> decide
 
-/-- Adjacent inner product: G[i][j] = -1 when i,j are in the same crossing pair. -/
-theorem gram_adjacent (i j : Fin 8) (h_same_pair : i.val / 2 = j.val / 2) (h_ne : i ≠ j) :
+theorem gram_adjacent (i j : Fin 8) (h_same : i.val / 2 = j.val / 2) (h_ne : i ≠ j) :
     cartanGram i j = -1 := by
-  unfold cartanGram charVec
-  native_decide
+  unfold cartanGram charVec; fin_cases i <;> fin_cases j <;> simp at h_ne h_same <;> omega
 
-/-- Cross-pair inner product: G[i][j] = 0 when i,j are in different pairs. -/
-theorem gram_cross_pair (i j : Fin 8) (h_diff_pair : i.val / 2 ≠ j.val / 2) :
+theorem gram_cross_pair (i j : Fin 8) (h_diff : i.val / 2 ≠ j.val / 2) :
     cartanGram i j = 0 := by
-  unfold cartanGram charVec
-  native_decide
+  unfold cartanGram charVec; fin_cases i <;> fin_cases j <;> simp at h_diff <;> omega
 
 -- ── §4: Cartan Weight Matrix ──────────────────────────────────────
 
-/-- The Cartan weight matrix C[i][j] = 273 for self, 256 for adjacent, 0 otherwise.
-    This is the scaled Gram matrix: C = G × scale_factor + constant_shift. -/
 def cartanWeight (i j : Fin 8) : ℤ :=
   if i = j then 273
   else if i.val / 2 = j.val / 2 then 256
   else 0
 
-/-- Cartan weights are related to character Gram by scaling and shifting.
-    C[i][j] = 256 + 17 × G[i][j] when adjusted for sign convention. -/
-theorem cartan_gram_relation (i j : Fin 8) :
-    (cartanWeight i j : ℚ) = if i=j then 273 else if i.val/2=j.val/2 then 256 else 0 := rfl
+theorem weight_diag (i : Fin 8) : cartanWeight i i = 273 := rfl
+
+theorem weight_adjacent (i j : Fin 8) (h_same : i.val / 2 = j.val / 2) (h_ne : i ≠ j) :
+    cartanWeight i j = 256 := by
+  unfold cartanWeight; simp [h_ne, h_same]
+
+theorem weight_cross_pair (i j : Fin 8) (h_diff : i.val / 2 ≠ j.val / 2) :
+    cartanWeight i j = 0 := by
+  unfold cartanWeight; simp [h_diff]
 
 -- ── §5: Block Eigenvalues ─────────────────────────────────────────
 
-/-- Each 2×2 block of the Cartan matrix has structure [[273, 256], [256, 273]]. -/
-/-- Eigenvalues: λ₁ = 273 + 256 = 529, λ₂ = 273 - 256 = 17. -/
 theorem block_eigenvalues :
-    (273 : ℤ) + 256 = 529 ∧ (273 : ℤ) - 256 = 17 := by
-  norm_num
+    (273 : ℤ) + 256 = 529 ∧ (273 : ℤ) - 256 = 17 := by norm_num
 
 -- ── §6: Spectral Gap ──────────────────────────────────────────────
 
-/-- The minimum eigenvalue λ_min = 17, normalized by D = 1792, gives ∆ = 17/1792. -/
 theorem spectral_gap_chain :
     (273 : ℚ) / 1792 = (39 : ℚ) / 256 ∧
     (256 : ℚ) / 1792 = (1 : ℚ) / 7 ∧
-    ((273 : ℚ) - 256) / 1792 = (17 : ℚ) / 1792 := by
+    (273 - 256 : ℚ) / 1792 = (17 : ℚ) / 1792 := by
   norm_num
 
-/-- The spectral gap in Q16_16 representation. -/
-theorem gap_q16 : ((17 : ℚ) / 1792) * 65536 = (17 * 65536 / 1792 : ℚ) := by
-  ring
-
 end SilverSight.CharacterTransform