refactor(core): typed Invariant/TensorType migration, CartanConnection cleanup

Bind.lean: - Add Invariant structure (Nat-backed identifier) with DecidableEq - Add Invariant.ofNat / Invariant.fromString (boundary-only string->Nat hash) - Add TensorType inductive enum (identity, riemannian, thermodynamic, etc.) - Migrate Metric.tensor from String to TensorType (AGENTS.md S1.5 compliance) - Migrate Witness.left_invariant/right_invariant from String to Invariant - Update all bind theorems and #eval call sites BraidField.lean: - Update computePIST call sites to use Invariant.fromString BraidEigensolid.lean: - Simplify eigensolid_trivial proof (drop unnecessary calc block) CartanConnection.lean: - Extract C_int_cross_block_zero lemma - Extract factor_sum lemma (eliminates inline factor helper) - Extract mu_double_lift lemma (factors out triplicated pattern in Jacobiator_basis_zero_int, reducing it from ~30 lines to ~12) - Simplify Jacobiator_basis_all using refine+rw pattern nr_bracket_validation.py: - Fix stale file path (Research Stack -> research-stack)
2026-07-31 01:25:21 +00:00 · 2026-06-28 00:11:28 -05:00 · 2026-06-28 00:11:28 -05:00 · 7c303624be
commit 7c303624be
parent 37ea14842a
5 changed files with 137 additions and 90 deletions
--- 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
--- 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
--- 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
--- 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
--- 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()