diff --git a/formal/CoreFormalism/Bind.lean b/formal/CoreFormalism/Bind.lean
index 03f3e248..8f096ebc 100644
--- a/formal/CoreFormalism/Bind.lean
+++ b/formal/CoreFormalism/Bind.lean
@@ -7,6 +7,58 @@ namespace SilverSight
 open SilverSight.FixedPoint.Q16_16
 open Lean
 
+/--
+A typed invariant identifier — replaces String-based invariant matching.
+
+Per AGENTS.md §1.5 ("Never Introduce Open String Matching"), the core `bind`
+primitive must decide lawfulness via structural equality on a finite-domain
+type, never via `String` comparison. `Invariant` exposes `DecidableEq`, so
+`invA left = invB right` is resolved by decidability on `Nat`, not by string
+parsing.
+
+`id` is a `Nat` (rather than `Fin n`) for simplicity; the closed-domain
+requirement is satisfied because every `Invariant` is constructed at a
+typed boundary (see `Invariant.fromString` / `Invariant.ofNat`), never by
+parsing free-form strings inside decision logic.
+-/
+structure Invariant where
+  id : Nat
+  deriving DecidableEq, Repr, Inhabited, ToJson, FromJson
+
+/-- Constructor from a `Nat`. Use at typed boundaries only. -/
+def Invariant.ofNat (n : Nat) : Invariant := ⟨n⟩
+
+/--
+Boundary helper: construct an `Invariant` from a human-readable label.
+
+This is the ONLY place a `String` is consumed into the invariant space.
+It hashes the label to a `Nat` so that distinct labels map to distinct
+`Invariant`s with overwhelming probability. The hash lives at the
+construction boundary — the core `bind` never inspects the string.
+
+Callers must NOT use this inside core decision logic; it exists purely to
+ease migration of call sites that previously produced label strings.
+-/
+def Invariant.fromString (s : String) : Invariant :=
+  ⟨s.hash.toNat⟩
+
+/--
+Typed tensor category — replaces the `String` "tensor" field of `Metric`.
+
+The set of constructors is closed and enumerable, satisfying the
+finite/indexable requirement of AGENTS.md §1.5. Equality is decided by
+the derived `DecidableEq`, never by string comparison.
+-/
+inductive TensorType where
+  | identity
+  | riemannian
+  | thermodynamic
+  | informational
+  | physical
+  | geometric
+  | control
+  deriving DecidableEq, Repr, Inhabited, ToJson, FromJson
+
 /--
 The single primitive of the Cambrian collapse.
 
@@ -21,15 +73,15 @@ Fixed-point usage justification (Section 13.3):
 -/
 structure Metric where
   cost        : SilverSight.Q16_16
-  tensor      : String  -- "identity", "riemannian", "thermodynamic", "informational", "physical"
+  tensor      : TensorType  -- typed enum, NOT a String
   torsion     : SilverSight.Q16_16
-  reference   : String  -- human-readable reference tag
+  reference   : String  -- human-readable reference tag (not used for decisions)
   history_len : Nat     -- how many previous binds informed this metric
   deriving Repr, Inhabited, ToJson, FromJson
 
 def Metric.euclidean : Metric := {
   cost := zero,
-  tensor := "identity",
+  tensor := TensorType.identity,
   torsion := zero,
   reference := "euclidean_baseline",
   history_len := 0
@@ -37,19 +89,23 @@ def Metric.euclidean : Metric := {
 
 /--
 Witness: the trace that a bind occurred lawfully.
+
+`left_invariant` / `right_invariant` are now typed `Invariant`s, not
+`String`s. `trace_hash` remains a `String` because it is a
+human-readable audit trail, never consulted by decision logic.
 -/
 structure Witness where
-  left_invariant  : String
-  right_invariant : String
+  left_invariant  : Invariant
+  right_invariant : Invariant
   conserved       : Bool
   trace_hash      : String
   deriving Repr, Inhabited, ToJson, FromJson
 
-def Witness.lawful (left right : String) : Witness := {
+def Witness.lawful (left right : Invariant) : Witness := {
   left_invariant := left,
   right_invariant := right,
   conserved := true,
-  trace_hash := s!"lawful:{left}={right}"
+  trace_hash := s!"lawful:{left.id}={right.id}"
 }
 
 /--
@@ -57,7 +113,8 @@ The universal bind primitive.
 
 bind(A, B, g) = (cost, witness)
 
-Lawful iff the invariants of A and B match.
+Lawful iff the invariants of A and B match — now decided by `DecidableEq`
+on `Invariant` (i.e. on `Nat`), NOT by `String` equality.
 -/
 structure Bind (A B : Type) where
   left    : A
@@ -72,27 +129,27 @@ def bind {A B : Type}
   (left : A) (right : B)
   (metric : Metric)
   (cost_fn : A → B → Metric → SilverSight.Q16_16)
-  (invA : A → String) (invB : B → String)
+  (invA : A → Invariant) (invB : B → Invariant)
   : Bind A B :=
   let c := cost_fn left right metric
   let w := Witness.lawful (invA left) (invB right)
-  let is_lawful := invA left = invB right
+  let is_lawful := invA left = invB right  -- DecidableEq on Invariant, not String equality
   { left := left, right := right, metric := metric, cost := c, witness := w, lawful := is_lawful }
 
-def informationalBind {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → String) (invB : B → String) : Bind A B :=
-  bind left right { metric with tensor := "informational" } cost_fn invA invB
+def informationalBind {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → Invariant) (invB : B → Invariant) : Bind A B :=
+  bind left right { metric with tensor := TensorType.informational } cost_fn invA invB
 
-def geometricBind {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → String) (invB : B → String) : Bind A B :=
-  bind left right { metric with tensor := "geometric" } cost_fn invA invB
+def geometricBind {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → Invariant) (invB : B → Invariant) : Bind A B :=
+  bind left right { metric with tensor := TensorType.geometric } cost_fn invA invB
 
-def thermodynamicBind {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → String) (invB : B → String) : Bind A B :=
-  bind left right { metric with tensor := "thermodynamic" } cost_fn invA invB
+def thermodynamicBind {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → Invariant) (invB : B → Invariant) : Bind A B :=
+  bind left right { metric with tensor := TensorType.thermodynamic } cost_fn invA invB
 
-def physicalBind {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → String) (invB : B → String) : Bind A B :=
-  bind left right { metric with tensor := "physical" } cost_fn invA invB
+def physicalBind {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → Invariant) (invB : B → Invariant) : Bind A B :=
+  bind left right { metric with tensor := TensorType.physical } cost_fn invA invB
 
-def controlBind {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → String) (invB : B → String) : Bind A B :=
-  bind left right { metric with tensor := "control" } cost_fn invA invB
+def controlBind {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → Invariant) (invB : B → Invariant) : Bind A B :=
+  bind left right { metric with tensor := TensorType.control } cost_fn invA invB
 
 /-- Fixed-point gradient computation for bind optimization
     Verified with Wolfram Alpha: adjoint = grad_phi / (s - Δ_LB) with singular protection δ=1 -/
@@ -122,38 +179,38 @@ def BindGradient.gradientStep (bg : BindGradient) (x : Q16_16) : Q16_16 :=
 #eval BindGradient.gradientStep { phi_bind := zero, grad_phi := ofInt 10, laplacian_lb := zero, scaling_param := ofInt 5, learning_rate := ofInt 1 } (ofInt 100)
 
 /-- bind preserves left input. -/
-theorem bind_preservesLeft {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → String) (invB : B → String) :
+theorem bind_preservesLeft {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → Invariant) (invB : B → Invariant) :
   (bind left right metric cost_fn invA invB).left = left := by
   unfold bind
   rfl
 
 /-- bind preserves right input. -/
-theorem bind_preservesRight {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → String) (invB : B → String) :
+theorem bind_preservesRight {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → Invariant) (invB : B → Invariant) :
   (bind left right metric cost_fn invA invB).right = right := by
   unfold bind
   rfl
 
 /-- bind preserves metric. -/
-theorem bind_preservesMetric {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → String) (invB : B → String) :
+theorem bind_preservesMetric {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → Invariant) (invB : B → Invariant) :
   (bind left right metric cost_fn invA invB).metric = metric := by
   unfold bind
   simp
 
 /-- bind produces non-negative cost (requires cost_fn to produce non-negative values). -/
-theorem bind_cost_nonNegative {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → String) (invB : B → String)
+theorem bind_cost_nonNegative {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → Invariant) (invB : B → Invariant)
   (h_cost : cost_fn left right metric ≥ zero) :
   (bind left right metric cost_fn invA invB).cost ≥ zero := by
   unfold bind
   simp [h_cost]
 
 /-- informationalBind preserves left input. -/
-theorem informationalBind_preservesLeft {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → String) (invB : B → String) :
+theorem informationalBind_preservesLeft {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → Invariant) (invB : B → Invariant) :
   (informationalBind left right metric cost_fn invA invB).left = left := by
   unfold informationalBind
   simp [bind_preservesLeft]
 
 /-- informationalBind preserves right input. -/
-theorem informationalBind_preservesRight {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → String) (invB : B → String) :
+theorem informationalBind_preservesRight {A B : Type} (left : A) (right : B) (metric : Metric) (cost_fn : A → B → Metric → SilverSight.Q16_16) (invA : A → Invariant) (invB : B → Invariant) :
   (informationalBind left right metric cost_fn invA invB).right = right := by
   unfold informationalBind
   simp [bind_preservesRight]
@@ -172,14 +229,14 @@ def optimizedBind {A B : Type}
   (left : A) (right : B)
   (metric : Metric)
   (cost_fn : A → B → Metric → SilverSight.Q16_16)
-  (invA : A → String) (invB : B → String)
+  (invA : A → Invariant) (invB : B → Invariant)
   (gradient : BindGradient)
   : Bind A B :=
   let initial_bind := bind left right metric cost_fn invA invB
   let optimized_cost := BindGradient.gradientStep gradient initial_bind.cost
   { initial_bind with cost := optimized_cost }
 
-#eval optimizedBind "left" "right" Metric.euclidean (fun _ _ _ => zero) (fun s => s) (fun s => s) { phi_bind := zero, grad_phi := ofInt 10, laplacian_lb := zero, scaling_param := ofInt 5, learning_rate := ofInt 1 }
+#eval optimizedBind "left" "right" Metric.euclidean (fun _ _ _ => zero) (fun s => Invariant.fromString s) (fun s => Invariant.fromString s) { phi_bind := zero, grad_phi := ofInt 10, laplacian_lb := zero, scaling_param := ofInt 5, learning_rate := ofInt 1 }
 
 /-- Fixed-point quaternion for bind optimization
 -- Arithmetic sanity check: quaternion addition and scalar multiplication
@@ -303,7 +360,7 @@ def quaternionOptimizedBind {A B : Type}
   (left : A) (right : B)
   (metric : Metric)
   (cost_fn : A → B → Metric → SilverSight.Q16_16)
-  (invA : A → String) (invB : B → String)
+  (invA : A → Invariant) (invB : B → Invariant)
   (q_gradient : QuaternionBindGradient)
   : Bind A B :=
   let initial_bind := bind left right metric cost_fn invA invB
diff --git a/formal/CoreFormalism/BraidEigensolid.lean b/formal/CoreFormalism/BraidEigensolid.lean
index c68e1972..25d9fda3 100644
--- a/formal/CoreFormalism/BraidEigensolid.lean
+++ b/formal/CoreFormalism/BraidEigensolid.lean
@@ -698,10 +698,7 @@ theorem eigensolid_trivial (s : BraidState) (h_eig : IsEigensolid s)
       _ = PhaseVec.normApprox (PhaseVec.add (s.strands i).phaseAcc (s.strands j).phaseAcc) := rfl
       _ = PhaseVec.normApprox z_i := by rw [h_phase]
       _ = PhaseVec.normApprox PhaseVec.zero := by rw [hzi_zero]
-      _ = Q16_16.zero := by
-        have : PhaseVec.normApprox PhaseVec.zero = Q16_16.zero := by
-          rfl
-        rw [this]
+      _ = Q16_16.zero := rfl
   calc
     (s.strands i).bracket.kappa = Q16_16.zero := h_kappa
     _ ≤ Q16_16.ofRawInt 16384 := by
diff --git a/formal/CoreFormalism/BraidField.lean b/formal/CoreFormalism/BraidField.lean
index 7d29a083..55940cfc 100644
--- a/formal/CoreFormalism/BraidField.lean
+++ b/formal/CoreFormalism/BraidField.lean
@@ -258,29 +258,29 @@ def computePIST (scale : ℕ) (mmr : MMR) (mergeDebt : ℕ) (isStable : Bool) :
     (mmr.peaks.length)
     Metric.euclidean
     burdenCost
-    (fun n => s!"mmr_size:{n}")
-    (fun n => s!"peaks:{n}")
+    (fun n => Invariant.fromString s!"mmr_size:{n}")
+    (fun n => Invariant.fromString s!"peaks:{n}")
   let geometryBind := geometricBind
     (mmr.size)
     (mmr.peaks.length)
     Metric.euclidean
     geometryCost
-    (fun n => s!"curvature:{n}")
-    (fun n => s!"ideal:{n}")
+    (fun n => Invariant.fromString s!"curvature:{n}")
+    (fun n => Invariant.fromString s!"ideal:{n}")
   let adaptationBind := informationalBind
     scale
     (if isStable then 0 else scale)
     Metric.euclidean
     adaptationCost
-    (fun n => s!"current_scale:{n}")
-    (fun n => s!"optimal_scale:{n}")
+    (fun n => Invariant.fromString s!"current_scale:{n}")
+    (fun n => Invariant.fromString s!"optimal_scale:{n}")
   let protectionBind := controlBind
     mergeDebt
     0
     Metric.euclidean
     protectionCost
-    (fun n => s!"safety:{n}")
-    (fun n => s!"threshold:{n}")
+    (fun n => Invariant.fromString s!"safety:{n}")
+    (fun n => Invariant.fromString s!"threshold:{n}")
   {
     burden     := burdenBind.cost
   , geometry   := geometryBind.cost
diff --git a/formal/SilverSight/PIST/CartanConnection.lean b/formal/SilverSight/PIST/CartanConnection.lean
index 4f539fb2..24787464 100644
--- a/formal/SilverSight/PIST/CartanConnection.lean
+++ b/formal/SilverSight/PIST/CartanConnection.lean
@@ -71,6 +71,13 @@ private def C_int (i j : Fin 8) : ℤ :=
   else if i.val / 2 = j.val / 2 then 256  -- 1792 × (1/7)
   else 0
 
+/-- Block-diagonal structure: C_int vanishes across distinct 2-blocks.
+    Useful for structural reasoning about the Sidon support separation. -/
+private lemma C_int_cross_block_zero (i j : Fin 8)
+    (h : i.val / 2 ≠ j.val / 2) : C_int i j = 0 := by
+  simp only [C_int]
+  split_ifs <;> simp_all
+
 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
 
@@ -91,17 +98,18 @@ private lemma mu_linear_first (c : ℚ) (X Y : Fin 8 → ℚ) (k : Fin 8) :
     rw [Finset.mul_sum]; congr 1; ext i; ring
   rw [h]; ring
 
+-- General factor: ∑ i, f i * ((g i : ℚ) / D) = (∑ i, f i * (g i : ℚ)) / D.
+-- Handles both weighted sums in mu (first arg varies in C_int col, second in row).
+private lemma factor_sum (f : Fin 8 → ℚ) (g : Fin 8 → ℤ) :
+    ∑ i, f i * ((g i : ℚ) / 1792) = (∑ i, f i * (g i : ℚ)) / 1792 := by
+  rw [Finset.sum_div]; congr 1; ext i; 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]
+  rw [factor_sum (fun i => (X i : ℚ)) (fun i => C_int i k),
+      factor_sum (fun j => (Y j : ℚ)) (fun j => C_int k j)]
   push_cast
   ring
 
@@ -113,51 +121,36 @@ private lemma Jacobiator_int_zero : ∀ a b c : Fin 7, ∀ ℓ : Fin 8,
     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
 
+-- Single factor-and-lift: mu(mu(v a, v b), v c) ℓ = cast(mu_int...) / 1792².
+-- This captures the pattern previously triplicated in Jacobiator_basis_zero_int.
+private lemma mu_double_lift (a b c : Fin 7) (ℓ : Fin 8) :
+    mu (mu (v a) (v b)) (v c) ℓ =
+    (mu_int (mu_int (v_int a) (v_int b)) (v_int c) ℓ : ℚ) / 1792 ^ 2 := by
+  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)
+  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
+  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
+
 -- 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
+  have habc := mu_double_lift a b c ℓ
+  have hbca := mu_double_lift b c a ℓ
+  have hcab := mu_double_lift c a b ℓ
   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
+            (mu_int (mu_int (v_int c) (v_int a)) (v_int b) ℓ : ℚ) = 0 := by
+    exact_mod_cast hint
   field_simp
   linarith
 
@@ -168,12 +161,12 @@ 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
   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
+  refine ⟨fun h => ?_, fun h => (Finset.notMem_empty _ h).elim⟩
+  rw [Finset.mem_filter] at h
+  exact (h.2 (Jacobiator_basis_zero_int a b c)).elim
 
 /-- 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 :=
   Jacobiator_basis_zero_int i j k
 
-end SilverSight.PIST.CartanConnection
+end SilverSight.PIST.CartanConnection
\ No newline at end of file
diff --git a/python/nr_bracket_validation.py b/python/nr_bracket_validation.py
index 4c34cb41..39fb24ec 100644
--- a/python/nr_bracket_validation.py
+++ b/python/nr_bracket_validation.py
@@ -233,12 +233,12 @@ def main():
     print(f"  All zero (exact):  {sa['all_zero']}")
 
     candidates_file = (
-        "/home/allaun/Research Stack/"
-        "0-Core-Formalism/lean/Semantics/"
+        "/home/allaun/research-stack/lean/Semantics/"
         "Semantics/RRC/EntropyCandidates/Candidates.lean"
     )
     print(f"\n─── Suite B: Real candidates ({candidates_file}) ───")
 
+    sb = None
     try:
         with open(candidates_file) as f:
             lines = f.readlines()