diff --git a/formal/SilverSight/PIST/CartanConnection.lean b/formal/SilverSight/PIST/CartanConnection.lean
index 18699d8e..4f539fb2 100644
--- a/formal/SilverSight/PIST/CartanConnection.lean
+++ b/formal/SilverSight/PIST/CartanConnection.lean
@@ -15,7 +15,11 @@
     PIST:                 Same Sidon support separation drives gates
     VCN:                  Vanishing terms = structural zero gaps
 
-  Gate C verification: `native_decide` on 7³ = 343 basis triples.
+  Proof strategy (integer bypass, replaces native_decide per AGENTS.md §5):
+    D = lcm(7, 256) = 1792.  C_weight i j = C_int i j / D (exact).
+    mu on ℤ-valued inputs scales by 1/D; Jacobiator scales by 1/D².
+    decide on ℤ (binary arithmetic, no GCD) verifies 7³×8 = 2744 cases.
+    Scaling then lifts the ℤ result to the ℚ theorem.
 -/
 
 import Mathlib.Data.Matrix.Basic
@@ -39,7 +43,7 @@ def C_weight (i j : Fin 8) : ℚ :=
     On basis vectors: μ(e_i, e_j) = C[i,j]·(e_i − e_j).
     This is alternating: μ(e_j,e_i) = −μ(e_i,e_j).
 
-    Explicit formula (for efficient native_decide evaluation):
+    Explicit formula:
       μ(X,Y)[k] = (C·X)[k]·Y[k] − X[k]·(C·Y)[k] -/
 def mu (X Y : Fin 8 → ℚ) : Fin 8 → ℚ :=
   λ k => (∑ i : Fin 8, X i * C_weight i k) * Y k - X k * (∑ j : Fin 8, Y j * C_weight k j)
@@ -58,27 +62,118 @@ def v (k : Fin 7) : Fin 8 → ℚ :=
     else if i = 7 then -1
     else 0
 
+-- ─── Integer bypass ──────────────────────────────────────────────────────────
+-- D = lcm(7, 256) = 1792.  Exact: C_weight i j = C_int i j / 1792.
+-- ─────────────────────────────────────────────────────────────────────────────
+
+private def C_int (i j : Fin 8) : ℤ :=
+  if i = j then 273                       -- 1792 × (39/256) = 7 × 39
+  else if i.val / 2 = j.val / 2 then 256  -- 1792 × (1/7)
+  else 0
+
+private lemma C_weight_scale (i j : Fin 8) : C_weight i j = (C_int i j : ℚ) / 1792 := by
+  simp only [C_weight, C_int]; split_ifs <;> norm_num
+
+private def mu_int (X Y : Fin 8 → ℤ) (k : Fin 8) : ℤ :=
+  (∑ i : Fin 8, X i * C_int i k) * Y k - X k * (∑ j : Fin 8, Y j * C_int k j)
+
+private def v_int (k : Fin 7) (i : Fin 8) : ℤ :=
+  if i = k.castSucc then 1 else if i = (7 : Fin 8) then -1 else 0
+
+private lemma v_eq_cast (k : Fin 7) (i : Fin 8) : v k i = (v_int k i : ℚ) := by
+  simp only [v, v_int]; split_ifs <;> norm_num
+
+-- mu is linear in its first argument: mu(c·X, Y) = c·mu(X, Y)
+private lemma mu_linear_first (c : ℚ) (X Y : Fin 8 → ℚ) (k : Fin 8) :
+    mu (fun i => c * X i) Y k = c * mu X Y k := by
+  simp only [mu]
+  have h : ∑ i : Fin 8, c * X i * C_weight i k = c * ∑ i : Fin 8, X i * C_weight i k := by
+    rw [Finset.mul_sum]; congr 1; ext i; ring
+  rw [h]; ring
+
+-- mu on ℤ-cast inputs = mu_int / 1792 (exact).
+-- ring cannot handle Finset.sum directly; we factor 1/1792 from each sum first.
+private lemma mu_scale (X Y : Fin 8 → ℤ) (k : Fin 8) :
+    mu (fun i => (X i : ℚ)) (fun i => (Y i : ℚ)) k = (mu_int X Y k : ℚ) / 1792 := by
+  simp only [mu, mu_int, C_weight_scale]
+  -- Factor 1/1792 from each weighted sum: ∑ f*(c/D) = (∑ f*c)/D
+  have factor : ∀ (f : Fin 8 → ℤ) (j : Fin 8),
+      ∑ i : Fin 8, (f i : ℚ) * ((C_int i j : ℚ) / 1792) =
+      (∑ i : Fin 8, (f i : ℚ) * (C_int i j : ℚ)) / 1792 := fun f j => by
+    rw [Finset.sum_div]; congr 1; ext i; ring
+  rw [factor X k, factor Y k]
+  push_cast
+  ring
+
+-- 7³ × 8 = 2744 ℤ arithmetic cases.
+-- Binary-integer kernel evaluation: no GCD chains, completes in < 1s.
+-- Per AGENTS.md §5: decide is preferred over native_decide when feasible.
+private lemma Jacobiator_int_zero : ∀ a b c : Fin 7, ∀ ℓ : Fin 8,
+    mu_int (mu_int (v_int a) (v_int b)) (v_int c) ℓ +
+    mu_int (mu_int (v_int b) (v_int c)) (v_int a) ℓ +
+    mu_int (mu_int (v_int c) (v_int a)) (v_int b) ℓ = 0 := by decide
+
+-- Jacobiator vanishes on every basis triple (ℚ, lifted from the ℤ computation).
+private lemma Jacobiator_basis_zero_int (a b c : Fin 7) :
+    Jacobiator mu (v a) (v b) (v c) = 0 := by
+  funext ℓ
+  simp only [Jacobiator, Pi.add_apply, Pi.zero_apply]
+  -- Rewrite each v k as a cast of v_int k
+  have hva : v a = fun i => (v_int a i : ℚ) := funext (v_eq_cast a)
+  have hvb : v b = fun i => (v_int b i : ℚ) := funext (v_eq_cast b)
+  have hvc : v c = fun i => (v_int c i : ℚ) := funext (v_eq_cast c)
+  -- Inner mu: mu(cast X)(cast Y) k = cast(mu_int X Y k) / 1792
+  have hab : mu (v a) (v b) = fun k => (mu_int (v_int a) (v_int b) k : ℚ) / 1792 :=
+    funext fun k => by rw [hva, hvb]; exact mu_scale _ _ k
+  have hbc : mu (v b) (v c) = fun k => (mu_int (v_int b) (v_int c) k : ℚ) / 1792 :=
+    funext fun k => by rw [hvb, hvc]; exact mu_scale _ _ k
+  have hca : mu (v c) (v a) = fun k => (mu_int (v_int c) (v_int a) k : ℚ) / 1792 :=
+    funext fun k => by rw [hvc, hva]; exact mu_scale _ _ k
+  -- Outer mu: mu((cast Z)/1792)(cast W) = cast(mu_int Z W) / 1792²
+  -- Step: rewrite first arg as (1/1792)·cast Z, apply linearity, then mu_scale.
+  have habc : mu (mu (v a) (v b)) (v c) ℓ =
+      (mu_int (mu_int (v_int a) (v_int b)) (v_int c) ℓ : ℚ) / 1792 ^ 2 := by
+    rw [hab, hvc]
+    have heq : (fun k => (mu_int (v_int a) (v_int b) k : ℚ) / 1792) =
+               fun k => (1 / 1792 : ℚ) * (mu_int (v_int a) (v_int b) k : ℚ) := by
+      ext; ring
+    rw [heq, mu_linear_first (1 / 1792), mu_scale]; ring
+  have hbca : mu (mu (v b) (v c)) (v a) ℓ =
+      (mu_int (mu_int (v_int b) (v_int c)) (v_int a) ℓ : ℚ) / 1792 ^ 2 := by
+    rw [hbc, hva]
+    have heq : (fun k => (mu_int (v_int b) (v_int c) k : ℚ) / 1792) =
+               fun k => (1 / 1792 : ℚ) * (mu_int (v_int b) (v_int c) k : ℚ) := by
+      ext; ring
+    rw [heq, mu_linear_first (1 / 1792), mu_scale]; ring
+  have hcab : mu (mu (v c) (v a)) (v b) ℓ =
+      (mu_int (mu_int (v_int c) (v_int a)) (v_int b) ℓ : ℚ) / 1792 ^ 2 := by
+    rw [hca, hvb]
+    have heq : (fun k => (mu_int (v_int c) (v_int a) k : ℚ) / 1792) =
+               fun k => (1 / 1792 : ℚ) * (mu_int (v_int c) (v_int a) k : ℚ) := by
+      ext; ring
+    rw [heq, mu_linear_first (1 / 1792), mu_scale]; ring
+  rw [habc, hbca, hcab]
+  -- Integer sum = 0 (by decide), cast to ℚ, clear 1792² denominator
+  have hint := Jacobiator_int_zero a b c ℓ
+  have hq : (mu_int (mu_int (v_int a) (v_int b)) (v_int c) ℓ : ℚ) +
+            (mu_int (mu_int (v_int b) (v_int c)) (v_int a) ℓ : ℚ) +
+            (mu_int (mu_int (v_int c) (v_int a)) (v_int b) ℓ : ℚ) = 0 := by exact_mod_cast hint
+  field_simp
+  linarith
+
 /-- Theorem (Gate C): The Jacobiator of μ vanishes on all 7³ = 343 basis
-    triples of V.  Verified by `native_decide`.  By trilinearity this
-    extends to all of V, proving d_CE μ = 0. -/
+    triples of V.  Proof: integer bypass (decide on ℤ, D=1792 scaling).
+    By trilinearity this extends to all of V, proving d_CE μ = 0. -/
 theorem Jacobiator_basis_all : ((Finset.univ : Finset (Fin 7)).product
     ((Finset.univ : Finset (Fin 7)).product (Finset.univ : Finset (Fin 7)))).filter
     (λ (ijk : Fin 7 × Fin 7 × Fin 7) => Jacobiator mu (v ijk.1) (v ijk.2.1) (v ijk.2.2) ≠ 0) = ∅ := by
-  native_decide
+  ext ⟨a, b, c⟩
+  simp only [Finset.mem_filter, Finset.mem_product, Finset.mem_univ, true_and,
+             Finset.not_mem_empty, iff_false, ne_eq, not_not]
+  exact Jacobiator_basis_zero_int a b c
 
 /-- Convenience: the Jacobiator vanishes for any single basis triple. -/
-lemma Jacobiator_basis_zero (i j k : Fin 7) : Jacobiator mu (v i) (v j) (v k) = 0 := by
-  have h_all := Jacobiator_basis_all
-  have mem : (i, (j, k)) ∈ (Finset.univ : Finset (Fin 7)).product
-    ((Finset.univ : Finset (Fin 7)).product (Finset.univ : Finset (Fin 7))) := by
-    simp
-  by_contra hne
-  have hmem_filter : (i, (j, k)) ∈ ((Finset.univ : Finset (Fin 7)).product
-    ((Finset.univ : Finset (Fin 7)).product (Finset.univ : Finset (Fin 7)))).filter
-    (λ (ijk : Fin 7 × Fin 7 × Fin 7) => Jacobiator mu (v ijk.1) (v ijk.2.1) (v ijk.2.2) ≠ 0) := by
-    apply Finset.mem_filter.mpr
-    exact ⟨mem, hne⟩
-  rw [h_all] at hmem_filter
-  simp at hmem_filter
+lemma Jacobiator_basis_zero (i j k : Fin 7) : Jacobiator mu (v i) (v j) (v k) = 0 :=
+  Jacobiator_basis_zero_int i j k
 
 end SilverSight.PIST.CartanConnection