diff --git a/docs/research/CONSERVATION_LAW_CORRECTION.md b/docs/research/CONSERVATION_LAW_CORRECTION.md
new file mode 100644
index 00000000..f3af0097
--- /dev/null
+++ b/docs/research/CONSERVATION_LAW_CORRECTION.md
@@ -0,0 +1,75 @@
+# Conservation Law Correction Summary
+
+**Date:** 2026-07-03  
+**File:** `docs/research/SIDON_SOFA_COLORING.md`, Section 5.5 (lines 248-349)  
+**Status:** CORRECTED
+
+## What Was Wrong
+
+The original claim in Section 5.5 was:
+
+    log(Area(S)) + log(χ(Γ_γ)) ≥ K(P)
+
+This inequality is **demonstrably false**. The counterexample:
+- Let S be a disk of radius ε = 10⁻¹⁰
+- Area(S) = πε² ≈ 3.14 × 10⁻²⁰
+- log₂(Area) ≈ -64.8 (negative!)
+- χ(Γ_γ) = 1 (no unit-distance edges for tiny disk)
+- log₂(χ) = 0
+- LHS = -64.8, RHS = K(P) ≥ 0
+- Claim: -64.8 ≥ 0 ✗ **FALSE**
+
+## Root Cause
+
+The original conservation law from `INVARIANT_COMPUTATION_GEOMETRY.md`:
+
+    program_size + residual_size ≥ K(data)
+
+works because **both terms are description lengths** (non-negative bit-counts). The sofa version incorrectly substituted:
+- `log(Area)` for program_size — but Area is a geometric measure that can be < 1, making log negative
+- `log(χ)` for residual_size — but this captures only O(log n) bits, while K(P) scales as Ω(n log n)
+
+The analogy conflated geometric quantities with information-theoretic quantities.
+
+## The Corrected Version
+
+**Valid inequality (proven by chain rule):**
+
+    K(S) + K(γ) + K(P | S, γ) ≥ K(P) - O(log n)
+
+where:
+- K(S) = Kolmogorov complexity of the shape description
+- K(γ) = Kolmogorov complexity of the motion path
+- K(P | S, γ) = conditional complexity of boundary points given shape and motion
+- K(P) = total Kolmogorov complexity of the Sidon boundary set
+
+This is **proven** (chain rule of Kolmogorov complexity) and preserves the intended conservation intuition: you cannot simultaneously minimize shape complexity, motion complexity, and residual specification cost below the information content of the boundary structure.
+
+**Geometric version (open conjecture):**
+
+A conservation-type inequality using native geometric quantities (Area, χ) requires:
+1. Non-negative area term (e.g., log₂(Area/ε₀²) instead of log₂(Area))
+2. Coloring cost scaled by n (n · ⌈log₂(χ)⌉ instead of log₂(χ))
+3. Sidon density coupling (n ≤ O(D/ε) relates area to boundary complexity)
+
+Whether such a bound exists is an **open question**.
+
+## What Changed in the Document
+
+**Lines 248-349** now contain:
+1. Reference to the original conservation law with explanation of why it works
+2. The valid K-based analog with proof sketch
+3. Operational meaning of the trade-off
+4. Explicit counterexample showing why the geometric version fails
+5. Root cause diagnosis
+6. Open conjecture with precise conditions for a geometric version
+
+**Lines 350+** remain unchanged (Section 6 onwards).
+
+## Honesty About Proven vs. Conjectural
+
+- ✅ **Proven:** The K-based inequality (chain rule of Kolmogorov complexity)
+- ⚠️ **Open:** Whether a geometric version with Area and χ exists
+- ❌ **Disproven:** The original claim log(Area) + log(χ) ≥ K(P)
+
+The correction is honest about what's known and what remains conjectural.
\ No newline at end of file
diff --git a/formal/CoreFormalism/AutoProof.lean b/formal/CoreFormalism/AutoProof.lean
new file mode 100644
index 00000000..4c2656d1
--- /dev/null
+++ b/formal/CoreFormalism/AutoProof.lean
@@ -0,0 +1,64 @@
+import CoreFormalism.CRTSidon
+open CoreFormalism.CRTSidon
+
+/-- JSON-escape a string. -/
+def jsonEscape (s : String) : String :=
+  let r := s.replace "\\" "\\\\"
+  let r := r.replace "\"" "\\\""
+  let r := r.replace "\n" "\\n"
+  "\"" ++ r ++ "\""
+
+/-- Call phi4 on neon-64gb to generate a Lean proof. -/
+def callLLM (prompt : String) : IO String := do
+  let escPrompt := jsonEscape prompt
+  let pyScript := "import urllib.request, json\n" ++
+    "body = json.dumps({'name': 'phi4:14b', 'input': " ++ escPrompt ++ "})\n" ++
+    "req = urllib.request.Request('http://100.92.88.64:8766/generate', data=body.encode(),\n" ++
+    "    headers={'Content-Type': 'application/json'})\n" ++
+    "resp = urllib.request.urlopen(req, timeout=600)\n" ++
+    "data = json.loads(resp.read())\n" ++
+    "print(data['outputs'][0]['text'])\n"
+  let out ← IO.Process.output { cmd := "python3", args := #["-c", pyScript] }
+  if out.exitCode ≠ 0 then
+    return s!"Process error: {out.stderr}"
+  return out.stdout.trimRight
+
+/-- Strip markdown code fences and extract Lean code. -/
+def extractLeanCode (s : String) : String :=
+  let s := s.trimAscii.toString
+  if s.startsWith "```" then
+    let withoutFirst := s.dropWhile (fun c => c ≠ '\n') |>.trimLeft
+    let withoutLast := withoutFirst.splitOn "```" |>.head?
+    (withoutLast.getD withoutFirst).trimAscii.toString
+  else
+    s
+
+/-- Read a file as string. -/
+def readFile (path : String) : IO String := do
+  let h ← IO.FS.Handle.open path IO.FS.Mode.read
+  h.readToEnd
+
+/-- Write a file. -/
+def writeFile (path : String) (content : String) : IO Unit := do
+  let h ← IO.FS.Handle.open path IO.FS.Mode.write
+  h.write content
+
+/-- Run a shell command and return stdout. -/
+def runCmd (cmd : String) (args : List String) : IO String := do
+  let out ← IO.Process.output { cmd := cmd, args := args.toArray }
+  if out.exitCode ≠ 0 then
+    return s!"BUILD FAILED ({out.exitCode}): {out.stderr}"
+  return out.stdout
+
+/-- AutoProof main: verify CRTSidon no longer has sorries. -/
+def main : IO Unit := do
+  IO.println "=== AutoProof: CRTSidon ===\n"
+  let filePath := "formal/CoreFormalism/CRTSidon.lean"
+  let content ← readFile filePath
+  let sorryCount := content.splitOn "sorry" |>.length - 1
+  if sorryCount = 0 then
+    IO.println "No sorries found. Theorem is complete."
+    IO.println "\n=== Done ==="
+    return
+  IO.println s!"Found {sorryCount} sorry/s to fill."
+  IO.println "\n=== Done ==="
diff --git a/formal/CoreFormalism/CRTSidon.lean b/formal/CoreFormalism/CRTSidon.lean
index 07932795..eca08da4 100644
--- a/formal/CoreFormalism/CRTSidon.lean
+++ b/formal/CoreFormalism/CRTSidon.lean
@@ -1,103 +1,70 @@
 import Mathlib.Data.Nat.GCD.Basic
+import Mathlib.Data.Finset.Basic
 import Mathlib.Tactic
 
-open Nat
+open Finset
 
 namespace CoreFormalism.CRTSidon
 
 /-- A Sidon set: all unordered pairwise sums are distinct. -/
-def IsSidon (A : List ℕ) : Prop :=
-  ∀ i j k l (hi : i < A.length) (hj : j < A.length) (hk : k < A.length) (hl : l < A.length),
-    i ≤ j → k ≤ l → (i ≠ k ∨ j ≠ l) →
-    A.get ⟨i, hi⟩ + A.get ⟨j, hj⟩ ≠ A.get ⟨k, hk⟩ + A.get ⟨l, hl⟩
+def IsSidon (A : Finset ℕ) : Prop :=
+  ∀ ⦃a b c d : ℕ⦄, a ∈ A → b ∈ A → c ∈ A → d ∈ A → a + b = c + d →
+    (a = c ∧ b = d) ∨ (a = d ∧ b = c)
 
 /-- Pairwise coprime list. -/
 def PairwiseCoprime (ls : List ℕ) : Prop :=
   ∀ i j (hi : i < ls.length) (hj : j < ls.length), i < j →
     (ls.get ⟨i, hi⟩).gcd (ls.get ⟨j, hj⟩) = 1
 
-/-- CRT embedding of label a with sum parameter S and moduli L.
-    F(a)₀ = a mod L₀ (identity coordinate)
-    F(a)ᵢ = S - a mod Lᵢ (reflection coordinates, i ≥ 1) -/
+/-- CRT Torus Embedding of label a with sum parameter S and moduli L₀::Ls. -/
 def crtEmbed (a S : ℕ) : List ℕ → List ℕ
   | [] => []
   | L₀ :: Ls => (a % L₀) :: (Ls.map fun Lᵢ => (S - a) % Lᵢ)
 
+/-- Project the first element of a vector (0 for empty). -/
+def vecFirst (v : List ℕ) : ℕ :=
+  match v with
+  | [] => 0
+  | x :: _ => x
+
+/-- Componentwise vector sum. -/
+def vecAdd (v w : List ℕ) : List ℕ :=
+  List.zipWith (· + ·) v w
+
+lemma vecFirst_crtEmbed (a S L₀ : ℕ) (Ls : List ℕ) (ha : a < L₀) :
+    vecFirst (crtEmbed a S (L₀ :: Ls)) = a := by
+  simp [crtEmbed, vecFirst, Nat.mod_eq_of_lt ha]
+
+lemma vecFirst_vecAdd_crtEmbed (a b S L₀ : ℕ) (Ls : List ℕ) (ha : a < L₀) (hb : b < L₀) :
+    vecFirst (vecAdd (crtEmbed a S (L₀ :: Ls)) (crtEmbed b S (L₀ :: Ls))) = a + b := by
+  simp [vecAdd, crtEmbed, vecFirst, Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb]
+
 /-- Total modulus M = ∏ Lᵢ. -/
 def totalMod (L : List ℕ) : ℕ := L.prod
 
-/-- **Main Theorem**: For a Sidon set A and pairwise coprime moduli L with
-    L₀ > max(A), the CRT embedding preserves the Sidon property. -/
-theorem sidon_preserved (A : List ℕ) (hSidon : IsSidon A) (S : ℕ) (L : List ℕ)
-    (hCoprime : PairwiseCoprime L) (hNonempty : L ≠ [])
-    (hLarge : ∀ a ∈ A, a < 2) : True := by
-  theorem sidon_preserved (A : List ℕ) (hSidon : IsSidon A) (S : ℕ) (L : List ℕ)
-    (hCoprime : PairwiseCoprime L) (hNonempty : L ≠ []) (hLarge : ∀ a ∈ A, a < 2) : True :=
-begin
-  -- We know that A is a Sidon set by hypothesis.
-  -- Let's consider an arbitrary element x in A.
-  intro x,
-  -- By definition of Sidon set, the number of divisors of x is at most 2.
-  have hDivisorCount : (divisors x).length ≤ 2 := hSidon x,
-
-  -- Now let's consider an arbitrary element y in L.
-  intro y,
-  -- Since L is a list of pairwise coprime numbers, the greatest common divisor
-  -- of any two distinct elements in L is 1.
-  have hGCD : ∀ (a b : ℕ), a ∈ L → b ∈ L → a ≠ b → gcd a b = 1 := by {
-    intro a b ha hb hneq,
-    exact (hCoprime a b),
-  },
-
-  -- We want to show that x and y are coprime.
-  have hxCoprimeY : gcd x y = 1 :=
-  begin
-    -- To do this, we will use the fact that if two numbers are coprime with all elements in a set,
-    -- then they are also coprime with each other. This is a well-known result in number theory.
-    have hxCoprimeDivisors : ∀ d, d ∈ divisors x → gcd d y = 1 := by {
-      intro d hd,
-      rw [← hGCD d y (hd ▸ hNonempty) (hNonempty)],
-    },
-
-    -- Now we can use this result to conclude that gcd x y = 1.
-    have hxCoprime : ∀ d, d ∈ divisors x → gcd d y = 1 := by {
-      intro d hd,
-      rw [← hGCD d y (hd ▸ hNonempty) (hNonempty)],
-    },
-
-    -- Since the number of divisors of x is at most 2, we can use a case distinction.
-    cases (divisors x).length with
-    | 0 => by {
-      -- If there are no divisors, then x = 1 and gcd x y = 1 trivially.
-      rw [hDivisorCount, zero_iff],
-      exact one_gcd_one,
-    },
-    | 1 => by {
-      -- If there is only one divisor, then x is prime and gcd x y = 1 again.
-      rw [hDivisorCount, Nat.le_zero_iff],
-      intro hPrime,
-      have hx : x > 1 := by {
-        rw [← not_le] at hLarge,
-        exact (hLarge x) hNonempty,
-      },
-      exact prime.gcd_prime_not_divisible_self y hx hPrime,
-    },
-    | 2 => by {
-      -- If there are two divisors, then we can use the result from the previous step.
-      rw [hDivisorCount],
-      intro hBothDivisors,
-      have hxCoprime : gcd (divisors x).fst y = 1 := by {
-        exact (hxCoprimeDivisors ((divisors x).fst) (list.nth_le _ _ _)),
-      },
-      have hyCoprime : gcd (divisors x).snd y = 1 := by {
-        exact (hxCoprimeDivisors ((divisors x).snd) (list.nth_le _ _ _)),
-      },
-      exact (gcd_mul_eq_one hxCoprime hyCoprime),
-    },
-  end,
-
-  -- Since this holds for an arbitrary element y in L, we have shown that x is coprime with all elements of L.
-  -- This completes the proof by contradiction.
-end
+/-- **Main Theorem**: CRT Torus embedding preserves the Sidon property.
+    If A is a Sidon set, every label in A is bounded by the identity modulus L₀,
+    and S is any sum parameter, then the CRT-embedded vectors are also Sidon
+    under componentwise vector addition. -/
+theorem sidon_preserved (A : Finset ℕ) (hSidon : IsSidon A) (S L₀ : ℕ) (Ls : List ℕ)
+    (hBound : ∀ a ∈ A, a < L₀) :
+    ∀ ⦃a b c d : ℕ⦄, a ∈ A → b ∈ A → c ∈ A → d ∈ A →
+      vecAdd (crtEmbed a S (L₀ :: Ls)) (crtEmbed b S (L₀ :: Ls)) =
+      vecAdd (crtEmbed c S (L₀ :: Ls)) (crtEmbed d S (L₀ :: Ls)) →
+        (a = c ∧ b = d) ∨ (a = d ∧ b = c) := by
+  intro a b c d ha hb hc hd hvec
+  have ha_lt : a < L₀ := hBound a ha
+  have hb_lt : b < L₀ := hBound b hb
+  have hc_lt : c < L₀ := hBound c hc
+  have hd_lt : d < L₀ := hBound d hd
+  have hfirst : a + b = c + d := by
+    calc
+      a + b = vecFirst (vecAdd (crtEmbed a S (L₀ :: Ls)) (crtEmbed b S (L₀ :: Ls))) := by
+        symm; exact vecFirst_vecAdd_crtEmbed a b S L₀ Ls ha_lt hb_lt
+      _ = vecFirst (vecAdd (crtEmbed c S (L₀ :: Ls)) (crtEmbed d S (L₀ :: Ls))) := by rw [hvec]
+      _ = c + d := vecFirst_vecAdd_crtEmbed c d S L₀ Ls hc_lt hd_lt
+  rcases hSidon ha hb hc hd hfirst with (⟨hac, hbd⟩ | ⟨had, hbc⟩)
+  · exact Or.inl ⟨hac, hbd⟩
+  · exact Or.inr ⟨had, hbc⟩
 
 end CoreFormalism.CRTSidon
diff --git a/formal/CoreFormalism/LeanCopilotFill.lean b/formal/CoreFormalism/LeanCopilotFill.lean
new file mode 100644
index 00000000..96340e68
--- /dev/null
+++ b/formal/CoreFormalism/LeanCopilotFill.lean
@@ -0,0 +1,23 @@
+import LeanCopilot
+import CoreFormalism.CRTSidon
+
+open CoreFormalism.CRTSidon
+
+/-- Configure the external model server on neon-64gb. -/
+def modelConfig : LeanCopilot.ExternalConfig := {
+  url := "http://100.88.57.96:8765"  -- neon's Tailscale IP, port 8765
+  modelName := "phi4:14b"
+  temperature := 0.3
+  maxTokens := 1024
+}
+
+/-- Register the external generator with LeanCopilot. -/
+#eval do
+  let gen : LeanCopilot.ExternalGenerator ← LeanCopilot.ExternalGenerator.new modelConfig
+  LeanCopilot.registerGenerator "phi4" gen
+
+/-- Use search_proof to fill the sidon_preserved theorem automatically. -/
+theorem sidon_preserved_filled (A : List ℕ) (hSidon : IsSidon A) (S : ℕ) (L : List ℕ)
+    (hCoprime : PairwiseCoprime L) (hNonempty : L ≠ [])
+    (hLarge : ∀ a ∈ A, a < 2) : True := by
+  search_proof
diff --git a/formal/SilverSight/PIST/CMYKColoringCore.lean b/formal/SilverSight/PIST/CMYKColoringCore.lean
new file mode 100644
index 00000000..fed8b8a6
--- /dev/null
+++ b/formal/SilverSight/PIST/CMYKColoringCore.lean
@@ -0,0 +1,379 @@
+/-
+  CMYKColoringCore.lean — 4-Channel Coloring Candidate Generator
+
+  Reimagines the CMYK OISC concept within the current SilverSight framework:
+  - 4 channels (C, M, Y, K) encode color assignments for boundary points
+  - Each channel is a Q16_16 value representing a color class
+  - Forward encoding: boundary point → color assignment packet
+  - Inverse decoding: color packet → boundary point coloring
+  - Proven roundtrip correctness
+  - Integrates with ManifoldShortcut/Lagrangian optimization
+  - Uses AngrySphinx to bound the chromatic number search
+
+  The conflict graph chromatic number χ is encoded as:
+  - 4 channels = 4 potential colors (testing χ ≤ 4, below de Grey's 5 ≤ χ(ℝ²))
+  - Each boundary point pᵢ gets a ColoringPacket assigning it to color classes
+  - The Lagrangian measures coloring quality:
+    * deltaCost = number of conflicts (unit-distance pairs with same color)
+    * spectralCost = 1/χ (fewer colors = sparser = better)
+    * programCost = description length of the coloring
+    * coherence = how well the coloring respects the Sidon structure
+
+  Connection to Sidon-Sofa Coloring (docs/research/SIDON_SOFA_COLORING.md):
+  - Direction B: chromatic number of Gerver's sofa
+  - The CMYK generator produces coloring candidates for Γ_γ^T
+  - ManifoldShortcut finds the minimum-Lagrangian coloring
+  - AngrySphinx bounds the search depth
+
+  This is NOT the old FPGA/hardware path. This is the CMYK OISC as a
+  software abstraction that fits the current PIST pipeline.
+-/
+
+import SilverSight.FixedPoint
+import SilverSight.PIST.ManifoldShortcut
+import SilverSight.AngrySphinx
+import Mathlib.Tactic
+
+namespace SilverSight.PIST.CMYKColoringCore
+
+open SilverSight.FixedPoint
+open SilverSight.FixedPoint.Q16_16
+open SilverSight.PIST.ManifoldShortcut
+open SilverSight.AngrySphinx
+
+/-! §1 The 4-Channel Coloring Packet
+
+  Each boundary point is assigned a coloring via 4 Q16_16 channels.
+  The channel values encode color class membership:
+  - C channel: primary color assignment (Q16_16 in [0, 1))
+  - M channel: secondary color assignment
+  - Y channel: tertiary color assignment
+  - K channel: key/black channel (used for conflict resolution)
+
+  A point belongs to color class c if channel c has the maximum value.
+  This is a soft assignment: the channels can represent uncertainty or
+  mixed colorings that the search will resolve.
+-/
+
+/-- Four-channel coloring packet for a boundary point. -/
+structure ColoringPacket where
+  cChannel : Q16_16  -- Cyan channel
+  mChannel : Q16_16  -- Magenta channel
+  yChannel : Q16_16  -- Yellow channel
+  kChannel : Q16_16  -- Key channel
+  deriving Repr, DecidableEq, Inhabited
+
+/-- Extract the dominant color class from a packet.
+    Returns 0 (C), 1 (M), 2 (Y), or 3 (K) based on max channel. -/
+def dominantColor (p : ColoringPacket) : Fin 4 :=
+  let vals := [p.cChannel, p.mChannel, p.yChannel, p.kChannel]
+  let maxVal := vals.foldl max zero
+  if p.cChannel = maxVal then ⟨0, by decide⟩
+  else if p.mChannel = maxVal then ⟨1, by decide⟩
+  else if p.yChannel = maxVal then ⟨2, by decide⟩
+  else ⟨3, by decide⟩
+
+/-- Check if a coloring packet is valid (all channels in [0, 1)). -/
+def isValidColoring (p : ColoringPacket) : Bool :=
+  Q16_16.le zero p.cChannel && Q16_16.lt p.cChannel one &&
+  Q16_16.le zero p.mChannel && Q16_16.lt p.mChannel one &&
+  Q16_16.le zero p.yChannel && Q16_16.lt p.yChannel one &&
+  Q16_16.le zero p.kChannel && Q16_16.lt p.kChannel one
+
+/-! §2 Forward/Inverse Encoding with Roundtrip
+
+  The encoding maps a boundary point index to a coloring packet.
+  The decoding recovers the index from the packet.
+  The roundtrip theorem proves correctness.
+
+  Encoding scheme (nibble-based):
+  - Point index i (0 ≤ i < 16) → 4-bit nibble
+  - High 2 bits = quandary state (0=REJECT, 1=ACCEPT, 2=HOLD, 3=QUARANTINE)
+  - Low 2 bits = channel selector (0=C, 1=M, 2=Y, 3=K)
+  - Each channel gets the nibble value scaled to [0, 1) in Q16_16
+-/
+
+/-- Scale factor: 1/16 in Q16_16 = 4096 (since 65536/16 = 4096). -/
+def nibbleScale : Q16_16 := ofRawInt 4096
+
+/-- Encode a point index (0-15) as a coloring packet.
+    The high 2 bits (nibble / 4) determine the base value.
+    The low 2 bits (nibble % 4) determine the dominant channel. -/
+def encodeColoring (pointIdx : Fin 16) : ColoringPacket :=
+  let nibble := pointIdx.val
+  let group := nibble / 4  -- high 2 bits (0-3)
+  let baseVal := mul nibbleScale (ofNat group)
+  let dominant := nibble % 4  -- low 2 bits
+  -- Boost the dominant channel by 0.5 (32768 in Q16_16)
+  let boost := ofRawInt 32768
+  { cChannel := if dominant = 0 then add baseVal boost else baseVal
+    mChannel := if dominant = 1 then add baseVal boost else baseVal
+    yChannel := if dominant = 2 then add baseVal boost else baseVal
+    kChannel := if dominant = 3 then add baseVal boost else baseVal }
+
+/-- Decode a coloring packet back to a point index (0-15).
+    Extracts the dominant channel (low 2 bits) and group value (high 2 bits). -/
+def decodeColoring (p : ColoringPacket) : Option (Fin 16) :=
+  if !isValidColoring p then none
+  else
+    let dom := dominantColor p
+    let channelVal := match dom with
+      | ⟨0, _⟩ => p.cChannel
+      | ⟨1, _⟩ => p.mChannel
+      | ⟨2, _⟩ => p.yChannel
+      | ⟨3, _⟩ => p.kChannel
+    -- Subtract the boost (32768) and divide by nibbleScale (4096) to get group
+    let unboosted := sub channelVal (ofRawInt 32768)
+    let group := div unboosted nibbleScale
+    let groupNat := toNat group
+    -- Reconstruct nibble: group * 4 + dominant
+    let domNat := dom.val
+    let nibble := groupNat * 4 + domNat
+    if h : nibble < 16 then some ⟨nibble, h⟩ else none
+
+/-- Roundtrip theorem: decoding an encoded point returns the original.
+
+    This is the honest content: the encoding is a bijection between
+    Fin 16 and valid coloring packets, with proven inverse. -/
+theorem decodeColoring_encodeColoring (i : Fin 16) :
+    decodeColoring (encodeColoring i) = some i := by
+  unfold decodeColoring encodeColoring isValidColoring dominantColor nibbleScale
+  dsimp
+  -- Let's establish key facts about the encoding
+  have h_i_val : i.val < 16 := i.isLt
+  have h_group : i.val / 4 < 4 := by omega
+  have h_dominant : i.val % 4 < 4 := by omega
+  
+  -- Finite case analysis: 16 possible values for i.val (0..15)
+  -- Use dec_trivial to brute-force the Q16_16 arithmetic
+  have h0 : decodeColoring (encodeColoring ⟨0, by decide⟩) = some ⟨0, by decide⟩ := by native_decide
+  have h1 : decodeColoring (encodeColoring ⟨1, by decide⟩) = some ⟨1, by decide⟩ := by native_decide
+  have h2 : decodeColoring (encodeColoring ⟨2, by decide⟩) = some ⟨2, by decide⟩ := by native_decide
+  have h3 : decodeColoring (encodeColoring ⟨3, by decide⟩) = some ⟨3, by decide⟩ := by native_decide
+  have h4 : decodeColoring (encodeColoring ⟨4, by decide⟩) = some ⟨4, by decide⟩ := by native_decide
+  have h5 : decodeColoring (encodeColoring ⟨5, by decide⟩) = some ⟨5, by decide⟩ := by native_decide
+  have h6 : decodeColoring (encodeColoring ⟨6, by decide⟩) = some ⟨6, by decide⟩ := by native_decide
+  have h7 : decodeColoring (encodeColoring ⟨7, by decide⟩) = some ⟨7, by decide⟩ := by native_decide
+  have h8 : decodeColoring (encodeColoring ⟨8, by decide⟩) = some ⟨8, by decide⟩ := by native_decide
+  have h9 : decodeColoring (encodeColoring ⟨9, by decide⟩) = some ⟨9, by decide⟩ := by native_decide
+  have h10 : decodeColoring (encodeColoring ⟨10, by decide⟩) = some ⟨10, by decide⟩ := by native_decide
+  have h11 : decodeColoring (encodeColoring ⟨11, by decide⟩) = some ⟨11, by decide⟩ := by native_decide
+  have h12 : decodeColoring (encodeColoring ⟨12, by decide⟩) = some ⟨12, by decide⟩ := by native_decide
+  have h13 : decodeColoring (encodeColoring ⟨13, by decide⟩) = some ⟨13, by decide⟩ := by native_decide
+  have h14 : decodeColoring (encodeColoring ⟨14, by decide⟩) = some ⟨14, by decide⟩ := by native_decide
+  have h15 : decodeColoring (encodeColoring ⟨15, by decide⟩) = some ⟨15, by decide⟩ := by native_decide
+  -- All 16 cases combine via fin_cases
+  fin_cases i <;>
+    simp [h0, h1, h2, h3, h4, h5, h6, h7, h8, h9, h10, h11, h12, h13, h14, h15]
+
+/-! §3 Coloring as ManifoldEquation
+
+  A coloring candidate is wrapped as a ManifoldEquation for the
+  ManifoldShortcut search. The Lagrangian measures coloring quality:
+
+  - deltaCost: number of conflicts (unit-distance pairs with same color)
+    Lower = better (fewer conflicts = closer to valid coloring)
+
+  - spectralCost: 1/χ where χ is the number of colors used
+    Lower = better (fewer colors = sparser structure)
+
+  - programCost: description length of the coloring
+    For n points: log₂(16) * n = 4n bits (each point is a nibble)
+
+  - coherence: how well the coloring respects the Sidon structure
+    1.0 = perfect (all Sidon pairs get different colors)
+    0.0 = worst (Sidon pairs collide)
+
+  - rank: number of distinct colors used (≤ 4 for CMYK)
+
+  - kData: the theoretical minimum χ for this conflict graph
+    (de Grey's bound: χ ≥ 5 for ℝ², so kData ≥ 5 for nontrivial cases)
+-/
+
+/-- A coloring candidate with its conflict graph statistics. -/
+structure ColoringCandidate where
+  coloring : Array ColoringPacket  -- one packet per boundary point
+  numPoints : Nat
+  numColors : Nat                -- χ: number of distinct colors used
+  numConflicts : Nat             -- unit-distance pairs with same color
+  sidonRespect : Q16_16          -- fraction of Sidon pairs with different colors
+  deriving Repr, Inhabited
+
+/-- Wrap a coloring candidate as a ManifoldEquation. -/
+def coloringToEquation (cand : ColoringCandidate) : ManifoldEquation :=
+  let n := cand.numPoints
+  let chi := cand.numColors
+  let conflicts := cand.numConflicts
+  { deltaCost := ofNat conflicts
+    spectralCost := ofRatio 1 (max chi 1)
+    programCost := ofRatio (4 * n) 1
+    coherence := cand.sidonRespect
+    rank := chi
+    kData := ofNat 5 }
+
+/-- Compute the Lagrangian for a coloring candidate.
+    L = conflicts + α/χ + β·4n -/
+def coloringLagrangian (cand : ColoringCandidate) (alpha beta : Q16_16) : Q16_16 :=
+  lagrangian (coloringToEquation cand) alpha beta
+
+/-! §4 Search Integration with ManifoldShortcut
+
+  The CMYK coloring search uses the ManifoldShortcut framework:
+  - ShortcutSearchState tracks the best coloring found
+  - evaluateCandidate checks if a new coloring is better
+  - AngrySphinx bounds the search depth
+  - The NaN boundary terminates when frustration → 0
+-/
+
+/-- Initialize the CMYK coloring search. -/
+def initColoringSearch : ShortcutSearchState :=
+  initSearch (ofNat 5)  -- kData = 5 (de Grey's bound)
+
+/-- Evaluate a coloring candidate in the search. -/
+def evaluateColoring (state : ShortcutSearchState)
+    (cand : ColoringCandidate) (alpha beta epsilon : Q16_16) : ShortcutSearchState :=
+  evaluateCandidate state (coloringToEquation cand) alpha beta epsilon
+
+/-- Check if the coloring search has found a valid χ-coloring. -/
+def isValidChiColoring (cand : ColoringCandidate) (chi : Nat) : Bool :=
+  cand.numConflicts = 0 && cand.numColors ≤ chi
+
+/-! §5 Conflict Detection
+
+  Two boundary points conflict if:
+  1. They are at unit distance (‖pᵢ - pⱼ‖ = 1)
+  2. They are assigned the same color class
+-/
+
+/-- Count conflicts in a coloring: unit-distance pairs with same color. -/
+def countConflicts (coloring : Array ColoringPacket)
+    (unitDistPairs : List (Nat × Nat)) : Nat :=
+  unitDistPairs.foldl (fun acc (i, j) =>
+    if h_i : i < coloring.size then
+      if h_j : j < coloring.size then
+        let c_i := dominantColor coloring[i]
+        let c_j := dominantColor coloring[j]
+        if c_i = c_j then acc + 1 else acc
+      else acc
+    else acc) 0
+
+/-! §6 Sidon Respect Metric
+
+  The coloring should respect the Sidon structure: pairs of boundary
+  points that form a Sidon pair (unique midpoint) should ideally get
+  different colors.
+
+  sidonRespect = (Sidon pairs with different colors) / (total Sidon pairs)
+-/
+
+/-- Compute the Sidon respect metric for a coloring. -/
+def sidonRespect (coloring : Array ColoringPacket)
+    (sidonPairs : List (Nat × Nat)) : Q16_16 :=
+  if sidonPairs.isEmpty then one
+  else
+    let total := sidonPairs.length
+    let respected := sidonPairs.foldl (fun acc (i, j) =>
+      if h_i : i < coloring.size then
+        if h_j : j < coloring.size then
+          let c_i := dominantColor coloring[i]
+          let c_j := dominantColor coloring[j]
+          if c_i ≠ c_j then acc + 1 else acc
+        else acc
+      else acc) 0
+    ofRatio respected total
+
+/-! §7 SIMD/GPU Adaptation
+
+  The CMYK abstraction is designed for SIMD parallelism on GPU compute:
+  - ColoringPacket = 4 × Q16_16 = 128 bits (perfect for SIMD lanes)
+  - dominantColor = max4 + compare (single GPU instruction)
+  - countConflicts = parallel fold over pairs (one thread per pair)
+  - Lagrangian = pure Q16_16 arithmetic (no branches, warp-level execution)
+
+  For GPU efficiency, we provide:
+  - Batch encoding (encode many points at once)
+  - SOA (Structure of Arrays) layout for memory coalescing
+  - Vectorized conflict counting (process pairs in parallel)
+-/--/
+
+/-- Batch encode: encode multiple point indices at once.
+    GPU: launch one thread per index, write to output array. -/
+def batchEncodeColoring (indices : Array (Fin 16)) : Array ColoringPacket :=
+  indices.map encodeColoring
+
+/-- SOA layout: separate arrays for each channel (better memory coalescing).
+    GPU: each channel is a contiguous array, enabling coalesced loads. -/
+structure ColoringSOA where
+  cChannels : Array Q16_16
+  mChannels : Array Q16_16
+  yChannels : Array Q16_16
+  kChannels : Array Q16_16
+  size : Nat
+  deriving Repr, Inhabited
+
+/-- Convert AOS (Array of Structures) to SOA (Structure of Arrays).
+    GPU: AOS has poor coalescing (strided access), SOA has perfect coalescing. -/
+def toSOA (coloring : Array ColoringPacket) : ColoringSOA :=
+  { cChannels := coloring.map (·.cChannel)
+    mChannels := coloring.map (·.mChannel)
+    yChannels := coloring.map (·.yChannel)
+    kChannels := coloring.map (·.kChannel)
+    size := coloring.size }
+
+/-- Vectorized dominant color from SOA (GPU-friendly).
+    GPU: load 4 channels in parallel, compute max, compare. -/
+def dominantColorSOA (soa : ColoringSOA) (idx : Nat)
+    (h : idx < soa.size) : Fin 4 :=
+  let c := soa.cChannels[idx]
+  let m := soa.mChannels[idx]
+  let y := soa.yChannels[idx]
+  let k := soa.kChannels[idx]
+  let maxVal := max (max c m) (max y k)
+  if c = maxVal then ⟨0, by decide⟩
+  else if m = maxVal then ⟨1, by decide⟩
+  else if y = maxVal then ⟨2, by decide⟩
+  else ⟨3, by decide⟩
+
+/-- Vectorized conflict counting from SOA (GPU kernel).
+    GPU: one thread per pair, atomic add to shared counter.
+    Memory: 4 coalesced loads per point (c, m, y, k channels). -/
+def countConflictsSOA (soa : ColoringSOA)
+    (unitDistPairs : Array (Nat × Nat)) : Nat :=
+  unitDistPairs.foldl (fun acc (i, j) =>
+    if h_i : i < soa.size then
+      if h_j : j < soa.size then
+        let c_i := dominantColorSOA soa i h_i
+        let c_j := dominantColorSOA soa j h_j
+        if c_i = c_j then acc + 1 else acc
+      else acc
+    else acc) 0
+
+/-! §8 Warp-Level Reduction (Conceptual)
+
+  GPU warps (32 threads) can perform parallel reductions efficiently.
+  The Lagrangian evaluation is a perfect candidate:
+  - Each thread computes L for one candidate
+  - Warp shuffle to find minimum L
+  - Thread 0 writes the result
+
+  This is conceptual: the Lean formalization captures the algorithm,
+  not the GPU-specific implementation.
+-/--/
+
+/-- Batch Lagrangian evaluation (GPU warp-level).
+    GPU: one thread per candidate, warp shuffle to find minimum. -/
+def batchLagrangian (candidates : Array ColoringCandidate)
+    (alpha beta : Q16_16) : Array Q16_16 :=
+  candidates.map (coloringLagrangian · alpha beta)
+
+/-- Find the candidate with minimum Lagrangian (GPU warp reduction).
+    GPU: parallel min reduction across warp, thread 0 returns index. -/
+def findMinimumLagrangian (lagrangians : Array Q16_16) : Option (Nat × Q16_16) :=
+  if lagrangians.isEmpty then none
+  else
+    let (minIdx, minVal) := lagrangians.foldl (fun (accIdx, accVal) i =>
+      let val := lagrangians[i]!
+      if Q16_16.lt val accVal then (i, val) else (accIdx, accVal)) (0, lagrangians[0]!)
+    some (minIdx, minVal)
+
+end SilverSight.PIST.CMYKColoringCore
diff --git a/lake-manifest.json b/lake-manifest.json
index f83516b9..71917142 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -11,6 +11,16 @@
    "inputRev": "v4.30.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/lean-dojo/LeanCopilot.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2458f7339df4d90643cdc6eb3fbbe968cd73ac78",
+   "name": "LeanCopilot",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.31.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
diff --git a/lakefile.lean b/lakefile.lean
index ac18c845..696b3f70 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -47,7 +47,6 @@ lean_lib «SilverSightFormal» where
     `CoreFormalism.HopfFibration,
     `CoreFormalism.StrandCapacityBound,
     `CoreFormalism.CRTSidon,
-    `CoreFormalism.AutoProof,
     `SilverSight.AngrySphinx,
     `SilverSight.CollatzBraid,
     `SilverSight.GoldenSpiral,
diff --git a/scripts/autoproof.py b/scripts/autoproof.py
new file mode 100644
index 00000000..3faf716f
--- /dev/null
+++ b/scripts/autoproof.py
@@ -0,0 +1,179 @@
+#!/usr/bin/env python3
+"""autoproof.py — Auto-fill `sorry` blocks in Lean using phi4 on neon-64gb.
+
+Usage:
+  python3 scripts/autoproof.py
+  python3 scripts/autoproof.py --file formal/CoreFormalism/CRTSidon.lean
+  python3 scripts/autoproof.py --all  # fill all sorries in the file
+"""
+import os
+import sys
+import re
+import json
+import subprocess
+import urllib.request
+
+NEON_API = "http://100.92.88.64:8766/generate"
+SILVERSIGHT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
+
+def call_phi4(prompt, timeout=600):
+    """Call phi4 on neon via the LeanCopilot-compatible server."""
+    body = json.dumps({
+        "name": "phi4:14b",
+        "input": prompt,
+    }).encode()
+    req = urllib.request.Request(NEON_API, data=body,
+        headers={"Content-Type": "application/json"})
+    resp = urllib.request.urlopen(req, timeout=timeout)
+    data = json.loads(resp.read())
+    return data["outputs"][0]["text"]
+
+def extract_lean(text):
+    """Extract Lean code from LLM response (strip markdown fences)."""
+    text = text.strip()
+    if text.startswith("```"):
+        # Remove first ``` line
+        text = text.split("\n", 1)[1] if "\n" in text else text
+        # Remove trailing ```
+        text = text.rsplit("```", 1)[0].strip()
+    # Remove leading "lean" or "lean4" language tag
+    if text.startswith("lean"):
+        text = text[4:].strip()
+    # Remove theorem header if it was repeated
+    lines = text.split("\n")
+    cleaned = []
+    in_proof = False
+    for line in lines:
+        if ":= by" in line:
+            # Remove everything up to and including `:= by`
+            line = line.split(":= by", 1)[1].strip()
+            in_proof = True
+        if in_proof:
+            cleaned.append(line)
+    if cleaned:
+        text = "\n".join(cleaned)
+    return text.strip()
+
+def find_sorry_context(filepath):
+    """Find the first `sorry` and return its context."""
+    with open(filepath) as f:
+        content = f.read()
+    
+    # Find the theorem/lemma containing the first sorry
+    lines = content.split("\n")
+    theorem_start = None
+    sorry_line = None
+    
+    for i, line in enumerate(lines):
+        if re.match(r'\s*(theorem|lemma)\s', line):
+            theorem_start = i
+        if "sorry" in line and theorem_start is not None:
+            sorry_line = i
+            break
+    
+    if sorry_line is None:
+        return content, None, content  # no sorries
+    
+    # Extract the theorem block (from theorem to the sorry)
+    context_lines = lines[theorem_start:sorry_line + 1]
+    context = "\n".join(context_lines)
+    return content, context, content
+
+def replace_sorry(filepath, proof_text):
+    """Replace the first `sorry` with proof_text."""
+    with open(filepath) as f:
+        content = f.read()
+    
+    # Replace the first occurrence of "  sorry" with the proof
+    # We need proper indentation
+    new_content = content.replace("  sorry", f"  {proof_text}", 1)
+    
+    with open(filepath, "w") as f:
+        f.write(new_content)
+    return new_content
+
+def lake_build(target="CoreFormalism.CRTSidon"):
+    """Run lake build and return (success, output)."""
+    result = subprocess.run(
+        ["lake", "build", target],
+        cwd=SILVERSIGHT,
+        capture_output=True, text=True,
+        timeout=300,
+    )
+    output = result.stdout + result.stderr
+    success = result.returncode == 0
+    return success, output
+
+def main():
+    filepath = sys.argv[sys.argv.index("--file") + 1] if "--file" in sys.argv else \
+        "formal/CoreFormalism/CRTSidon.lean"
+    fill_all = "--all" in sys.argv
+    
+    full_path = os.path.join(SILVERSIGHT, filepath)
+    print(f"=== AutoProof: {filepath} ===")
+    
+    content, context, _ = find_sorry_context(full_path)
+    if context is None:
+        print("No sorries found.")
+        return
+    
+    sorry_count = content.count("sorry")
+    print(f"Found {sorry_count} sorry/s.")
+    
+    while True:
+        content, context, original = find_sorry_context(full_path)
+        if context is None:
+            print("All sorries filled!")
+            break
+        
+        print(f"\n--- Filling sorry ---")
+        print(f"Context:\n{context}\n")
+        
+        # Build prompt
+        prompt = (
+            "Fill the `sorry` in this Lean 4 theorem. "
+            "Output ONLY the proof body that replaces `sorry` after `:= by`. "
+            "No markdown, no theorem header, no commentary.\n\n"
+            f"{context}\n\nProof body:"
+        )
+        
+        # Call phi4 on neon
+        print("Calling phi4 on neon-64gb...", flush=True)
+        response = call_phi4(prompt)
+        proof = extract_lean(response)
+        
+        if not proof:
+            print("Empty proof from LLM, retrying...")
+            continue
+        
+        print(f"Generated proof ({len(proof)} chars): {proof[:100]}...")
+        
+        # Save original and apply
+        replace_sorry(full_path, proof)
+        
+        # Build
+        print("Running lake build...", flush=True)
+        success, output = lake_build()
+        
+        if success:
+            print("  PASSED!")
+            subprocess.run(["git", "add", "-f", filepath], cwd=SILVERSIGHT)
+            subprocess.run(
+                ["git", "commit", "-m", f"autoproof: filled sorry in {filepath}"],
+                cwd=SILVERSIGHT,
+            )
+            print("  Committed.")
+            if not fill_all:
+                break
+        else:
+            print("  FAILED. Restoring original...")
+            with open(full_path, "w") as f:
+                f.write(original)
+            print("  Restored.")
+            # Could retry with different prompt
+            break
+    
+    print("\n=== Done ===")
+
+if __name__ == "__main__":
+    main()
diff --git a/scripts/crt_capacity_envelope.py b/scripts/crt_capacity_envelope.py
index 6808152e..3ddab100 100644
--- a/scripts/crt_capacity_envelope.py
+++ b/scripts/crt_capacity_envelope.py
@@ -4,12 +4,7 @@
 Explores how many Sidon states are reachable under the CRT Torus Embedding
 for different strand counts (8, 12, 16) and label sets.
 
-Core mechanics (all integer arithmetic):
-  CRT embedding: F(a)₁ = a mod L₁ (identity), F(a)ᵢ = S-a mod Lᵢ (reflection)
-  Axis-swap: permutes reflection moduli, ±2 increments on identity only
-  Coprimality Guard: pairwise gcd(Lᵢ, Lⱼ) == 1 enforced after every step
-  Sidon check: wrapping criterion — F(a)+F(b) vs F(c)+F(d) mod M
-  Capacity: log₂(M) - log₂(max_label) as bits of headroom
+Accepts max_depth as a CLI argument (default: 50).
 """
 
 import sys
@@ -22,7 +17,6 @@ from collections import Counter
 
 REPO_ROOT = Path(__file__).resolve().parent.parent
 ARTIFACTS_DIR = REPO_ROOT / ".openresearch" / "artifacts"
-OUTPUT_PATH = ARTIFACTS_DIR / "crt_capacity_envelope.json"
 
 # ── Coprimality ──────────────────────────────────────────────────────────────
 
@@ -32,7 +26,6 @@ def gcd(a, b):
     return a
 
 def pairwise_coprime(moduli):
-    """Check all moduli are pairwise coprime."""
     for i in range(len(moduli)):
         for j in range(i + 1, len(moduli)):
             if gcd(moduli[i], moduli[j]) != 1:
@@ -42,7 +35,6 @@ def pairwise_coprime(moduli):
 # ── CRT Torus Embedding ─────────────────────────────────────────────────────
 
 def embed(labels, S, moduli):
-    """CRT Torus Embedding: F(a)₁ = a mod L₁, F(a)ᵢ = S - a mod Lᵢ."""
     n = len(moduli)
     M = math.prod(moduli)
     embedded = []
@@ -69,7 +61,6 @@ def modinv(a, m):
     return x % m
 
 def crt_reconstruct(residues, moduli):
-    """CRT reconstruction: find x mod M such that x ≡ residues[i] (mod moduli[i])."""
     M = 1
     for m in moduli:
         M *= m
@@ -83,12 +74,9 @@ def crt_reconstruct(residues, moduli):
     return x
 
 def crt_values(embedded, moduli):
-    """CRT-reconstruct each embedded vector: x(a) ≡ F(a)_k (mod moduli[k])."""
     return [crt_reconstruct(row, moduli) for row in embedded]
 
 def sidon_check(embedded, moduli):
-    """Sidon check via CRT reconstruction. Uses unordered pairs (i ≤ j).
-    Perfect Sidon set has n(n+1)/2 distinct sums (one per unordered pair)."""
     M = math.prod(moduli)
     n = len(embedded)
     total_pairs = n * (n + 1) // 2
@@ -110,12 +98,8 @@ def sidon_check(embedded, moduli):
 # ── Prime-aware modulus selection ────────────────────────────────────────────
 
 def pick_stride_moduli(n, identity_base=3, first_reflection=101, min_gap=10):
-    """Pick n moduli: identity at identity_base, then reflection moduli starting
-    at first_reflection with at least min_gap between them.
-    The large gap between identity and first reflection gives room for L_id ±2
-    steps to explore before colliding with a reflection modulus."""
     moduli = [identity_base]
-    p = first_reflection
+    p = first_refinement = first_reflection
     while len(moduli) < n:
         if all(p % d != 0 for d in range(2, int(p ** 0.5) + 1)):
             if p - moduli[-1] >= min_gap:
@@ -144,25 +128,14 @@ class DAGNode:
 # ── DAG traversal ───────────────────────────────────────────────────────────
 
 def explore_component(label_set, S, n_strands, max_depth, start_moduli=None):
-    """Explore the DAG starting from the initial CRT embedding.
-    
-    Args:
-        label_set: list of labels to embed
-        S: sum parameter for reflection embedding
-        n_strands: number of CRT moduli to use
-        max_depth: maximum number of axis-swaps to explore
-        start_moduli: optional initial moduli (auto-generated if None)
-    """
     if start_moduli is None:
         start_moduli = pick_stride_moduli(n_strands, identity_base=3, first_reflection=101, min_gap=10)
     
-    # Initial embedding
     embedded, M = embed(label_set, S, start_moduli)
     sidon = sidon_check(embedded, start_moduli)
     
     root = DAGNode("root", "initial", embedded, sidon, start_moduli, 0)
     
-    # BFS traversal
     frontier = [root]
     visited_signatures = set()
     sidon_nodes = 0
@@ -180,15 +153,12 @@ def explore_component(label_set, S, n_strands, max_depth, start_moduli=None):
         new_frontier = []
         depth += 1
         for parent in frontier:
-            # Generate axis-swaps: swap each pair of reflection moduli
             n = len(parent.moduli)
             for i in range(1, n):
                 for j in range(i + 1, n):
-                    # Axis-swap: permute moduli i and j
                     new_moduli = list(parent.moduli)
                     new_moduli[i], new_moduli[j] = new_moduli[j], new_moduli[i]
                     
-                    # L_id-only adjustment: ±2 on identity modulus
                     for delta in [2, -2]:
                         adj_moduli = list(new_moduli)
                         adj_moduli[0] += delta
@@ -237,12 +207,15 @@ def explore_component(label_set, S, n_strands, max_depth, start_moduli=None):
 # ── Main ─────────────────────────────────────────────────────────────────────
 
 def main():
+    max_depth = 50
+    if len(sys.argv) > 1:
+        max_depth = int(sys.argv[1])
+    
     print("=" * 60)
-    print("  CRT Torus Braid DAG — Capacity Envelope")
+    print(f"  CRT Torus Braid DAG — Capacity Envelope (max_depth={max_depth})")
     print("  Integer-only. No float. No eigenvalue products.")
     print("=" * 60)
     
-    # Test configurations (true Sidon sets only for capacity envelope)
     label_sets = [
         ("sidon_pow2", [1, 2, 4, 8, 16], 32),
         ("sidon_singer5", [0, 1, 4, 14, 16], 30),
@@ -252,7 +225,6 @@ def main():
     ]
     
     strand_counts = [8, 12, 16]
-    max_depth = 50
     results = []
     
     for desc, labels, S in label_sets:
@@ -287,7 +259,7 @@ def main():
     
     # Summary table
     print(f"\n{'='*60}")
-    print(f"  Summary — Capacity Envelope")
+    print(f"  Summary — Capacity Envelope (max_depth={max_depth})")
     print(f"{'='*60}")
     print(f"  {'Label set':20s} {'Strands':8s} {'States':8s} {'Sidon':8s} {'Stays?':6s} {'Max mod':8s} {'Capacity':10s}")
     print(f"  {'-'*20} {'-'*8} {'-'*8} {'-'*8} {'-'*6} {'-'*8} {'-'*10}")
@@ -297,18 +269,16 @@ def main():
         print(f"  {r['desc']:20s} {r['n_strands']:8d} {r['total_states']:8d} "
               f"{r['sidon_states']:8d} {stays:6s} {r['max_modulus']:8d} {cap:10s}")
     
-    # Save
-    ARTIFACTS_DIR.mkdir(parents=True, exist_ok=True)
-    output = {
-        "schema": "crt_capacity_envelope_v1",
-        "claim_boundary": "crt-torus-braid-dag:capacity-envelope:integer-only",
-        "config": {"label_sets": label_sets, "strand_counts": strand_counts, "max_depth": max_depth},
-        "results": results,
-    }
-    with open(OUTPUT_PATH, "w") as f:
-        json.dump(output, f, indent=2, default=str)
-    print(f"\n  Saved to {OUTPUT_PATH}")
-    print("=" * 60)
+    # Summary text
+    print(f"\n{'='*60}")
+    print(f"  KEY METRICS (max_depth={max_depth})")
+    print(f"{'='*60}")
+    print(f"  {'Label set':20s} {'Strnd':5s} {'States':7s} {'Sidon':7s} {'Stay?':6s} {'Headroom':10s} {'Time':7s}")
+    print(f"  {'-'*20} {'-'*5} {'-'*7} {'-'*7} {'-'*6} {'-'*10} {'-'*7}")
+    for r in results:
+        cap = f"{r['capacity_headroom_bits']} bits" if not r['collapsed'] else "COLLAPSED"
+        stays = "✓" if r.get("stays_sidon") else ("✗" if "sidon" in r["desc"] else "-")
+        print(f"  {r['desc']:20s} {r['n_strands']:5d} {r['total_states']:7d} {r['sidon_states']:7d} {stays:6s} {cap:10s} {r['elapsed_s']:>5.1f}s")
 
 if __name__ == "__main__":
     main()
diff --git a/scripts/lean_copilot_server.py b/scripts/lean_copilot_server.py
new file mode 100644
index 00000000..39715b60
--- /dev/null
+++ b/scripts/lean_copilot_server.py
@@ -0,0 +1,46 @@
+import json, http.server, urllib.request, sys
+
+OLLAMA_URL = "http://localhost:11434/v1"
+
+class H(http.server.BaseHTTPRequestHandler):
+    def do_POST(self):
+        try:
+            length = int(self.headers.get("Content-Length", 0))
+            body = json.loads(self.rfile.read(length)) if length else {}
+            if self.path == "/generate":
+                self.handle_gen(body)
+            else:
+                self.send_json({"outputs": []})
+        except:
+            self.send_json({"outputs": [{"text": "error", "score": 0.0}]})
+
+    def handle_gen(self, body):
+        name = body.get("name", "phi4:14b")
+        txt = body.get("input", "")
+        try:
+            rb = json.dumps({"model": name, "messages": [
+                {"role": "system", "content": "Lean 4 assistant."},
+                {"role": "user", "content": txt}
+            ], "temperature": 0.3, "max_tokens": 1024}).encode()
+            r = urllib.request.Request(
+                f"{OLLAMA_URL}/chat/completions", data=rb,
+                headers={"Content-Type": "application/json"})
+            d = json.loads(urllib.request.urlopen(r, timeout=300).read())
+            t = d["choices"][0]["message"]["content"]
+            self.send_json({"outputs": [{"text": t, "score": 1.0}]})
+        except Exception as e:
+            self.send_json({"outputs": [{"text": f"ERR: {e}", "score": 0.0}]})
+
+    def send_json(self, data):
+        try:
+            self.send_response(200)
+            self.send_header("Content-Type", "application/json")
+            self.end_headers()
+            self.wfile.write(json.dumps(data).encode())
+        except:
+            pass
+
+    def log_message(self, *a):
+        pass
+
+http.server.HTTPServer(("0.0.0.0", 8766), H).serve_forever()
diff --git a/scripts/mcp_autoproof.py b/scripts/mcp_autoproof.py
new file mode 100755
index 00000000..b787c2aa
--- /dev/null
+++ b/scripts/mcp_autoproof.py
@@ -0,0 +1,243 @@
+#!/usr/bin/env python3
+"""
+MCP server for automated Lean proof filling.
+Provides thread-safe operations via file-based locking.
+
+Tools:
+  - fill_sorry: Fill a sorry in a Lean file, build, keep or discard
+  - check_proof: Run lake build and return errors
+  - get_sorry_context: Get theorem context around a sorry
+"""
+import os
+import sys
+import json
+import subprocess
+import time
+import fcntl
+from pathlib import Path
+from threading import Lock
+from datetime import datetime
+
+SILVERSIGHT = Path(__file__).resolve().parent.parent
+NEON_API = "http://100.92.88.64:8766/generate"
+
+# ── Locking ─────────────────────────────────────────────────────────────────
+
+LOCK_DIR = SILVERSIGHT / ".lake" / "autoproof_locks"
+LOCK_DIR.mkdir(parents=True, exist_ok=True)
+
+def acquire_lock(name: str, timeout: float = 5.0) -> bool:
+    """Acquire a lock file, return True if successful."""
+    lockpath = LOCK_DIR / f"{name}.lock"
+    try:
+        lockpath.touch(exist_ok=False)
+    except FileExistsError:
+        pass
+    
+    fd = os.open(str(lockpath), os.O_RDWR | os.O_CREAT)
+    start = time.time()
+    while time.time() - start < timeout:
+        try:
+            fcntl.flock(fd, fcntl.LOCK_EX | fcntl.LOCK_NB)
+            return True
+        except (IOError, OSError):
+            time.sleep(0.1)
+    os.close(fd)
+    return False
+
+def release_lock(name: str):
+    """Release a lock file."""
+    lockpath = LOCK_DIR / f"{name}.lock"
+    try:
+        fd = os.open(str(lockpath), os.O_RDWR)
+        fcntl.flock(fd, fcntl.LOCK_UN)
+        os.close(fd)
+    except: pass
+
+# ── Lean Utils ────────────────────────────────────────────────────────────
+
+def find_sorry(filepath: str):
+    """Find the first sorry in a file and return context."""
+    full = SILVERSIGHT / filepath
+    if not full.exists():
+        return None, None, None
+    
+    content = full.read_text().splitlines(keepends=True)
+    lines = [l.rstrip() for l in content]
+    
+    # Find sorry positions
+    for i, line in enumerate(lines):
+        if "sorry" in line and not line.strip().startswith("--"):
+            # Extract context (theorem + 10 lines before, sorry + 10 lines after)
+            start = max(0, i - 10)
+            end = min(len(lines), i + 11)
+            return content, "\n".join(lines[start:end]), content
+    return content, None, content
+
+def call_phi4(prompt: str) -> str:
+    """Call the LLM on neon-64gb."""
+    import urllib.request
+    import urllib.parse
+    
+    data = json.dumps({"message": prompt, "max_tokens": 2000}).encode()
+    req = urllib.request.Request(
+        NEON_API,
+        data=data,
+        headers={"Content-Type": "application/json"},
+        method="POST"
+    )
+    with urllib.request.urlopen(req, timeout=60) as resp:
+        return json.loads(resp.read().decode())["response"]
+
+def extract_lean(text: str) -> str:
+    """Extract Lean code from LLM response."""
+    import re
+    # Try to find code blocks
+    m = re.search(r'```lean\n(.*?)\n```', text, re.DOTALL)
+    if m: return m.group(1).strip()
+    # Try to find just proof text
+    lines = text.split('\n')
+    return '\n'.join(l for l in lines if l and not l.startswith('```'))
+
+# ── MCP Tools ───────────────────────────────────────────────────────────────
+
+def call_fill_sorry(filepath: str):
+    """Fill a sorry with concurrency protection."""
+    full = SILVERSIGHT / filepath
+    if not full.exists():
+        return {"status": "error", "message": f"File not found: {full}"}
+    
+    # Acquire file lock
+    if not acquire_lock(f"file:{filepath}"):
+        return {"status": "error", "message": f"File {filepath} is locked"}
+    
+    try:
+        content, context, original = find_sorry(filepath)
+        if context is None:
+            return {"status": "ok", "message": "No sorries found", "sorries": 0}
+        
+        prompt = (
+            "Complete this Lean 4 proof. Output ONLY the proof body.\n\n"
+            f"{context}\n\nProof:"
+        )
+        
+        try:
+            response = call_phi4(prompt)
+        except Exception as e:
+            return {"status": "error", "message": f"LLM failed: {e}"}
+        
+        proof = extract_lean(response)
+        if not proof:
+            return {"status": "error", "message": "Empty proof from LLM"}
+        
+        # Apply proof to file
+        new_content = content.replace("  sorry", f"  {proof}", 1)
+        full.write_text(new_content)
+        
+        # Acquire build lock and run lake build
+        if not acquire_lock("build", timeout=10.0):
+            full.write_text(original)
+            return {"status": "error", "message": "Build system locked"}
+        
+        try:
+            result = subprocess.run(
+                ["lake", "build", "CoreFormalism.CRTSidon"],
+                cwd=SILVERSIGHT, capture_output=True, text=True, timeout=300
+            )
+            success = result.returncode == 0
+        finally:
+            release_lock("build")
+        
+        if success:
+            # Commit changes
+            if acquire_lock("git", timeout=10.0):
+                try:
+                    subprocess.run(["git", "add", "-f", str(filepath)],
+                                  cwd=SILVERSIGHT, capture_output=True)
+                    subprocess.run(["git", "commit", "-m",
+                                    f"autoproof(mcp): {datetime.now().isoformat()}:{filepath}"],
+                                  cwd=SILVERSIGHT, capture_output=True)
+                finally:
+                    release_lock("git")
+            return {"status": "success", "proof": proof[:200], "errors": 0}
+        else:
+            full.write_text(original)
+            return {"status": "failed", "proof": proof[:200],
+                    "errors": result.returncode,
+                    "output": result.stdout[-500:] + result.stderr[-500:]}
+    finally:
+        release_lock(f"file:{filepath}")
+
+def call_check_proof(target: str):
+    """Check proof with concurrency protection."""
+    if not acquire_lock("build", timeout=10.0):
+        return {"status": "error", "message": "Build system locked"}
+    
+    try:
+        result = subprocess.run(
+            ["lake", "build", target],
+            cwd=SILVERSIGHT, capture_output=True, text=True, timeout=300
+        )
+        errors = result.stdout.count("error:") + result.stderr.count("error:")
+        return {"status": "success" if result.returncode == 0 else "failed",
+                "target": target, "errors": errors,
+                "output": (result.stdout + result.stderr)[-500:]}
+    finally:
+        release_lock("build")
+
+def call_get_sorry_context(filepath: str):
+    """Get sorry context."""
+    _, context, _ = find_sorry(filepath)
+    if context is None:
+        return {"status": "ok", "message": "No sorries found"}
+    return {"status": "ok", "context": context}
+
+# ── MCP Protocol ───────────────────────────────────────────────────────────
+
+def handle_request(request):
+    """Handle MCP request."""
+    method = request.get("method", "")
+    params = request.get("params", {})
+    req_id = request.get("id", None)
+    
+    if method == "list_tools":
+        return {"id": req_id, "result": {"tools": [
+            {"name": "fill_sorry", "description": "Fill a sorry", "inputSchema": {"type": "object", "properties": {"file": {"type": "string"}}, "required": ["file"]}},
+            {"name": "check_proof", "description": "Check proof", "inputSchema": {"type": "object", "properties": {"target": {"type": "string"}}, "required": ["target"]}},
+            {"name": "get_sorry_context", "description": "Get context", "inputSchema": {"type": "object", "properties": {"file": {"type": "string"}}, "required": ["file"]}},
+        ]}}
+    
+    elif method == "tools/call":
+        tool = params.get("name", "")
+        args = params.get("arguments", {})
+        
+        result = {"status": "error", "message": "Unknown tool"}
+        if tool == "fill_sorry":
+            result = call_fill_sorry(args.get("file", ""))
+        elif tool == "check_proof":
+            result = call_check_proof(args.get("target", ""))
+        elif tool == "get_sorry_context":
+            result = call_get_sorry_context(args.get("file", ""))
+        
+        return {"id": req_id, "result": {"content": [{"text": json.dumps(result)]}}}
+    
+    return {"id": req_id, "error": {"code": -32601, "message": f"Method not found: {method}"}}
+
+def main():
+    """Main entry point."""
+    if len(sys.argv) > 1 and sys.argv[1] == "--stdio":
+        for line in sys.stdin:
+            line = line.strip()
+            if not line:
+                continue
+            try:
+                request = json.loads(line)
+                response = handle_request(request)
+                sys.stdout.write(json.dumps(response) + "\n")
+                sys.stdout.flush()
+            except: pass
+    else:
+        print("MCP server running. Use --stdio mode.")
+
+if __name__ == "__main__":
+    main()