feat(lean): modular Sidon preservation theorem + meta-review fixes

- CRTSidon.lean: full proof of sidon_preserved_mod (matches Python CRT-reconstructed mod-M check). Uses Bezout via Nat.gcdA/Nat.gcdB for CRT injectivity. 0 sorries. - BraidEigensolid.lean/GoldenSpiral.lean: fix golden centering constant (40560->40504, 0.14% relative error) - AGENTS.md: flag StrandCapacityBound triviality, add CRTSidon status - CITATION.cff: add Elsasser(1946) toroidal/poloidal prior art - SLOS receipt: add classical-simulation disclaimer - sidon_preservation_creation.md: mark creation theorem unformalized - autoresearch: containerized via runpod/autoresearch base image (silver-autoproof:latest), systemd service created - LeanCopilotFill.lean: updated for new CRTSidon API Build: 3297 jobs, 0 errors (lake build CoreFormalism.CRTSidon)
2026-07-30 17:16:16 +00:00 · 2026-07-04 01:04:52 -05:00 · 2026-07-04 01:04:52 -05:00 · f9b3df0803
commit f9b3df0803
parent 50732eaf0b
9 changed files with 255 additions and 35 deletions
--- a/AGENTS.md
+++ b/AGENTS.md
@ -138,6 +138,8 @@ Target: `formal/SilverSight/HachimojiN8.lean` — provable by `native_decide` on
 | AVMIsa/TypeCheck.lean | Complete | 0 |
 | AVMIsa/TypeSafety.lean | Complete | 0 |
 | AVMIsa/Run.lean | Complete | 0 |
+| CoreFormalism/CRTSidon.lean | Complete (CRT Torus preserves Sidon under vecAdd) | 0 |
+| CoreFormalism/StrandCapacityBound.lean | Trivial (|F(A)| ≤ min(|A|, L₁·L₂) — cardinality only, no Sidon info) | 0 |
 | RRC/Emit.lean | Complete (Q16_16 ncDerived, alignment gate, 6 fixtures) | 0 |
 | RRC/Q16_16Manifold.lean | Complete (278 rows, Q16_16 manifold fields) | 0 |
 | RRC/ReceiptDensity.lean | Complete | 0 |
--- a/CITATION.cff
+++ b/CITATION.cff
@ -360,6 +360,39 @@ references:
      name: "University of Twente"
    notes: "Polydisperse hard-sphere EOS, moments, glassy regime."

+  - type: article
+    title: "Induction Effects in Terrestrial Magnetism, Part I. Theory"
+    authors:
+      - family-names: "Elsasser"
+        given-names: "Walter M."
+    date-published: "1946"
+    doi: "10.1103/PhysRev.69.106"
+    journal: "Physical Review"
+    notes: >
+      Introduced toroidal/poloidal decomposition of vector fields on a
+      torus (poloidal = short way, toroidal = long way). SilverSight's
+      CRT Torus Embedding F(a)₁ = a mod L₀ (identity, poloidal),
+      F(a)ᵢ = S-a mod Lᵢ (reflection, toroidal) is the discrete
+      additive analogue. The S-a reflection corresponds to poloidal
+      inversion s_θ = ±1 in the continuous case, encoding braid
+      crossing orientation (over vs. under). Source:
+      formal/CoreFormalism/CRTSidon.lean,
+      docs/research/sidon_preservation_creation.md.
+
+  - type: online
+    title: "Toroidal and Poloidal Coordinates"
+    authors:
+      - literal: "Wikipedia contributors"
+    date-published: "2025-05-26"
+    url: "https://en.wikipedia.org/wiki/Toroidal_and_poloidal_coordinates"
+    notes: >
+      Accessible reference for toroidal/poloidal coordinate system.
+      The poloidal θ coordinate (short way around the torus) maps to
+      SilverSight's identity axis; the toroidal ζ coordinate (long way)
+      maps to the reflection axes. Both are special cases of the same
+      topology: two orthogonal directions on a torus with orientation
+      sign s = ±1 encoding chirality.
+
  # ── 2026-07 Session Sources ──────────────────────────────────

  - type: article
--- a/docs/research/SLOS_SIDON_VERIFICATION_RECEIPT.md
+++ b/docs/research/SLOS_SIDON_VERIFICATION_RECEIPT.md
@ -62,3 +62,5 @@ slos-sidon-verification:spearman-correlation-cross-method
 ```

 This receipt is bounded to the claim that eigenvalue product distinct_ratio predicts SLOS concentration ordering across the tested label sets and photon numbers. It does not claim universality beyond the 12 test cases, nor does it claim physical realizability on quantum hardware.
+
+**Important caveat:** SLOS (Strong Linear Optical Simulation) is Perceval's **classical** simulator of a photonic quantum system. The "cross-method validation" (ρ = -0.979) compares two classical computations (SLOS sampling and exact tensor network entropy), not theory vs. physical experiment. This receipt verifies computational consistency, not physical correctness.
--- a/docs/research/sidon_preservation_creation.md
+++ b/docs/research/sidon_preservation_creation.md
@ -111,6 +111,15 @@ The case 0 is the existing collision (T₁ = T₂). The case M is the new collis

 ### 6.3 Complete Sidon Creation Theorem

+**Status: Mathematically argued, formalized in Lean only for the preservation direction.**
+
+The Lean theorem (`CRTSidon.lean`) now formalizes both:
+- `sidon_preserved` — **preservation** under componentwise vector addition (stronger property)
+- `sidon_preserved_mod` — **preservation** under CRT-reconstructed modular sums (matches Python)
+  
+The **creation** direction (non-Sidon → Sidon under conditions (a)+(b)) is still unformalized.
+Empirical verification (500/500 tests, 416 collisions across 5000 trials) is not a proof.
+
 **Theorem.** For a finite A ⊂ ℤ with reflection closure a ↦ S−a,
 moduli L₁,…,Lₖ coprime, L₁,L₂ ≥ 2, and M = ∏ Lᵢ > max(A):

--- a/formal/CoreFormalism/BraidEigensolid.lean
+++ b/formal/CoreFormalism/BraidEigensolid.lean
@ -40,9 +40,10 @@ open SilverSight.BraidBracket
 open SilverSight.BraidCross
 open SilverSight.FixedPoint.Q16_16

-/-- Golden centering constant: phi^-1 = sqrt(5)-1/2 approx 0.61803398.
-    Represented in Q16_16 as 40560 (since 40560/65536 = 0.618896). -/
-def goldenCentering : Q16_16 := Q16_16.ofRawInt 40560
+/-- Golden centering constant: phi^-1 = (sqrt(5)-1)/2 approx 0.61803399.
+    Represented in Q16_16 as 40504 (since 40504/65536 = 0.6180344).
+    Corrected from 40560 (0.618896) which had 0.14% relative error. -/
+def goldenCentering : Q16_16 := Q16_16.ofRawInt 40504

 -- ============================================================
 -- §1. CORE TYPES
@ -454,10 +455,10 @@ theorem IsTopologicallyTrivial_iff (s : BraidState) :
    gives `kappa_i = kappa_j = normApprox(z_i) = 16N`, which exceeds 16384
    for N > 1024.  This *apparent counterexample* is resolved by the
    **golden centering contraction**: in the full compressor dynamics,
-    `crossStep` applies `goldenCentering` (φ⁻¹ ≈ 0.6189) as a multiplicative
+    `crossStep` applies `goldenCentering` (φ⁻¹ ≈ 0.6180) as a multiplicative
    contraction, which forces all crossing weights into the Q0_2 range
    [0, 16384] after finite iteration.  The constant `goldenCentering` at
-    line 44 has raw value 40560, which satisfies 40560 < 2·16384 = 32768,
+    line 44 has raw value 40504, which satisfies 40504 < 2·16384 = 32768,
    providing the contraction envelope.

    **Current status.**  The theorem is proven under a non-saturation hypothesis
--- a/formal/CoreFormalism/CRTSidon.lean
+++ b/formal/CoreFormalism/CRTSidon.lean
@ -1,3 +1,4 @@
+import Mathlib.Data.Int.ModEq
 import Mathlib.Data.Nat.GCD.Basic
 import Mathlib.Data.Finset.Basic
 import Mathlib.Tactic
@ -42,9 +43,7 @@ lemma vecFirst_vecAdd_crtEmbed (a b S L₀ : ℕ) (Ls : List ℕ) (ha : a < L₀
 /-- Total modulus M = ∏ Lᵢ. -/
 def totalMod (L : List ℕ) : ℕ := L.prod

-/-- **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
+/-- **Main Theorem (Componentwise)**: CRT Torus embedding preserves the Sidon property
    under componentwise vector addition. -/
 theorem sidon_preserved (A : Finset ℕ) (hSidon : IsSidon A) (S L₀ : ℕ) (Ls : List ℕ)
    (hBound : ∀ a ∈ A, a < L₀) :
@ -67,4 +66,154 @@ theorem sidon_preserved (A : Finset ℕ) (hSidon : IsSidon A) (S L₀ : ℕ) (Ls
  · exact Or.inl ⟨hac, hbd⟩
  · exact Or.inr ⟨had, hbc⟩

+/-- Convert ℕ modular equality to ℤ divisibility: a%n = b%n → n ∣ (a-b) in ℤ. -/
+lemma mod_eq_dvd (a b n : ℕ) (h : a % n = b % n) : (n : ℤ) ∣ ((a : ℤ) - (b : ℤ)) := by
+  have hz : (a : ℤ) % n = (b : ℤ) % n := by exact_mod_cast h
+  have h_eq : (a : ℤ) ≡ (b : ℤ) [ZMOD n] := hz
+  have h_sub : (a : ℤ) - (b : ℤ) ≡ 0 [ZMOD n] := by
+    calc
+      (a : ℤ) - (b : ℤ) ≡ (b : ℤ) - (b : ℤ) [ZMOD n] := Int.ModEq.sub h_eq (Int.ModEq.refl _)
+      _ = 0 := by ring
+  exact (Int.modEq_zero_iff_dvd.mp h_sub)
+
+/-- Convert ℤ divisibility to ℕ modular equality: n ∣ (a-b) in ℤ → a%n = b%n in ℕ. -/
+lemma dvd_mod_eq (a b n : ℕ) (h : (n : ℤ) ∣ ((a : ℤ) - (b : ℤ))) : a % n = b % n := by
+  have h_sub : ((a : ℤ) - (b : ℤ)) ≡ 0 [ZMOD n] := by
+    rw [Int.modEq_zero_iff_dvd]
+    exact h
+  have h_mod : (a : ℤ) ≡ (b : ℤ) [ZMOD n] := by
+    calc
+      (a : ℤ) = ((a : ℤ) - (b : ℤ)) + (b : ℤ) := by ring
+      _ ≡ 0 + (b : ℤ) [ZMOD n] := Int.ModEq.add h_sub (Int.ModEq.refl _)
+      _ = (b : ℤ) := by ring
+  exact_mod_cast h_mod
+
+/-- Two-modulus CRT injectivity: if a ≡ b (mod m) and a ≡ b (mod n) and
+    gcd(m,n) = 1, and a,b < m*n, then a = b.
+    
+    Uses Bezout's identity via Nat.gcdA/Nat.gcdB to prove m*n ∣ (a-b) in ℤ,
+    then the bound |a-b| < m*n forces a = b. -/
+lemma mod_eq_of_coprime {a b m n : ℕ} (hmn : Nat.Coprime m n) (hm : 0 < m) (hn : 0 < n)
+    (ham : a % m = b % m) (han : a % n = b % n) (ha : a < m * n) (hb : b < m * n) :
+    a = b := by
+  have hm_dvd : (m : ℤ) ∣ ((a : ℤ) - (b : ℤ)) := mod_eq_dvd a b m ham
+  have hn_dvd : (n : ℤ) ∣ ((a : ℤ) - (b : ℤ)) := mod_eq_dvd a b n han
+  -- Bezout: gcd(m,n)=1 → (Nat.gcdA m n) * m + (Nat.gcdB m n) * n = 1 in ℤ
+  have h_gcd_one : Nat.gcd m n = 1 := hmn
+  have hbez : (m : ℤ) * Nat.gcdA m n + (n : ℤ) * Nat.gcdB m n = (1 : ℤ) := by
+    calc
+      (m : ℤ) * Nat.gcdA m n + (n : ℤ) * Nat.gcdB m n = (Nat.gcd m n : ℤ) :=
+        (Nat.gcd_eq_gcd_ab m n).symm
+      _ = (1 : ℤ) := by exact_mod_cast h_gcd_one
+  set d := (a : ℤ) - (b : ℤ) with hd
+  -- Show m*n ∣ s*(m*d) (since n ∣ d) and m*n ∣ t*(n*d) (since m ∣ d)
+  have h_mn_dvd_md : (m * n : ℤ) ∣ (m : ℤ) * d := by
+    obtain ⟨q, hq⟩ := hn_dvd
+    refine ⟨q, ?_⟩
+    calc
+      (m : ℤ) * d = (m : ℤ) * ((n : ℤ) * q) := by rw [hq]
+      _ = (m * n : ℤ) * q := by ring
+  have h_mn_dvd_nd : (m * n : ℤ) ∣ (n : ℤ) * d := by
+    obtain ⟨q, hq⟩ := hm_dvd
+    refine ⟨q, ?_⟩
+    calc
+      (n : ℤ) * d = (n : ℤ) * ((m : ℤ) * q) := by rw [hq]
+      _ = (m * n : ℤ) * q := by ring
+  -- d = s*(m*d) + t*(n*d), so m*n ∣ d
+  have h_d_eq : d = (Nat.gcdA m n : ℤ) * ((m : ℤ) * d) + (Nat.gcdB m n : ℤ) * ((n : ℤ) * d) := by
+    calc
+      d = (1 : ℤ) * d := by ring
+      _ = ((m : ℤ) * Nat.gcdA m n + (n : ℤ) * Nat.gcdB m n) * d := by rw [hbez]
+      _ = (Nat.gcdA m n : ℤ) * ((m : ℤ) * d) + (Nat.gcdB m n : ℤ) * ((n : ℤ) * d) := by ring
+  have h_mn_dvd_d : (m * n : ℤ) ∣ d := by
+    rw [h_d_eq]
+    exact dvd_add (dvd_mul_of_dvd_right h_mn_dvd_md _) (dvd_mul_of_dvd_right h_mn_dvd_nd _)
+  -- |d| < m*n (since 0 ≤ a,b < m*n), so d = 0
+  have ha_z : (a : ℤ) < (m * n : ℤ) := by exact_mod_cast ha
+  have hb_z : (b : ℤ) < (m * n : ℤ) := by exact_mod_cast hb
+  have ha_nonneg : 0 ≤ (a : ℤ) := by exact_mod_cast (Nat.zero_le _)
+  have hb_nonneg : 0 ≤ (b : ℤ) := by exact_mod_cast (Nat.zero_le _)
+  have hd_upper : d < (m * n : ℤ) := by
+    dsimp [d]
+    omega
+  have hd_lower : -(m * n : ℤ) < d := by
+    dsimp [d]
+    omega
+  have hd_abs : |d| < (m * n : ℤ) :=
+    abs_lt.mpr ⟨hd_lower, hd_upper⟩
+  obtain ⟨k, hk⟩ := h_mn_dvd_d
+  have h_abs_mul : |(m * n : ℤ) * k| = (m * n : ℤ) * |k| := by simp
+  by_cases hk0 : k = 0
+  · dsimp [d] at hk
+    rw [hk0, mul_zero] at hk
+    omega
+  · have hk_abs_ge_one : 1 ≤ |k| := by
+      have hk_pos : 0 < |k| := abs_pos.mpr hk0
+      omega
+    have h_abs_ge_mn : |(m * n : ℤ) * k| ≥ (m * n : ℤ) := by
+      rw [h_abs_mul]
+      have h_nonneg_mn : 0 ≤ (m * n : ℤ) := by positivity
+      nlinarith
+    have h_abs_d : |d| = |(m * n : ℤ) * k| := by rw [hk]
+    rw [h_abs_d] at hd_abs
+    omega
+
+/-- **Modular Sidon Preservation Theorem (two-modulus CRT)**.
+    If A is a Sidon set, L₀ and L₁ are coprime, all pairwise sums < L₀·L₁,
+    S ≥ all labels, and the componentwise modular sums are congruent:
+      (a%L₀ + b%L₀) % L₀ = (c%L₀ + d%L₀) % L₀
+      ((S-a)%L₁ + (S-b)%L₁) % L₁ = ((S-c)%L₁ + (S-d)%L₁) % L₁
+    then {a,b} = {c,d}.
+
+    This matches the `crt_capacity_envelope.py` verification, which checks
+    CRT-reconstructed mod-M sums via componentwise congruences.
+    The componentwise `sidon_preserved` theorem proves a stronger property. -/
+theorem sidon_preserved_mod (A : Finset ℕ) (hSidon : IsSidon A) (S L₀ L₁ : ℕ)
+    (hCoprime : Nat.Coprime L₀ L₁) (hL₀ : 0 < L₀) (hL₁ : 0 < L₁)
+    (hS : ∀ a ∈ A, a ≤ S)
+    (hBound : ∀ a ∈ A, ∀ b ∈ A, a + b < L₀ * L₁) :
+    ∀ ⦃a b c d : ℕ⦄, a ∈ A → b ∈ A → c ∈ A → d ∈ A →
+      (a % L₀ + b % L₀) % L₀ = (c % L₀ + d % L₀) % L₀ →
+      ((S - a) % L₁ + (S - b) % L₁) % L₁ = ((S - c) % L₁ + (S - d) % L₁) % L₁ →
+        (a = c ∧ b = d) ∨ (a = d ∧ b = c) := by
+  intro a b c d ha hb hc hd h0 h1
+  -- Step 1: identity component → (a+b) % L₀ = (c+d) % L₀
+  have habL₀ : (a + b) % L₀ = (c + d) % L₀ := by
+    rw [Nat.add_mod a b L₀, Nat.add_mod c d L₀]
+    exact h0
+  -- Step 2: reflection component → (a+b) % L₁ = (c+d) % L₁
+  have habL₁ : (a + b) % L₁ = (c + d) % L₁ := by
+    have haS : a ≤ S := hS a ha
+    have hbS : b ≤ S := hS b hb
+    have hcS : c ≤ S := hS c hc
+    have hdS : d ≤ S := hS d hd
+    rw [← Nat.add_mod (S-a) (S-b) L₁, ← Nat.add_mod (S-c) (S-d) L₁] at h1
+    rw [show (S - a) + (S - b) = 2 * S - (a + b) from by omega,
+        show (S - c) + (S - d) = 2 * S - (c + d) from by omega] at h1
+    -- h1: (2*S - (a+b)) % L₁ = (2*S - (c+d)) % L₁
+    -- In ℤ: 2S-(a+b) ≡ 2S-(c+d) (ZMOD L₁) → (a+b) ≡ (c+d) (ZMOD L₁)
+    have hz : ((2 * S - (a + b) : ℕ) : ℤ) % L₁ = ((2 * S - (c + d) : ℕ) : ℤ) % L₁ :=
+      by exact_mod_cast h1
+    have h_dvd : (L₁ : ℤ) ∣ ((a + b : ℤ) - (c + d : ℤ)) := by
+      have h_eq : ((2 * S - (a + b) : ℕ) : ℤ) ≡ ((2 * S - (c + d) : ℕ) : ℤ) [ZMOD L₁] := hz
+      have h_sub : ((2 * S - (c + d) : ℕ) : ℤ) - ((2 * S - (a + b) : ℕ) : ℤ) ≡ 0 [ZMOD L₁] := by
+        have h_sub_eq : ((2 * S - (c + d) : ℕ) : ℤ) - ((2 * S - (a + b) : ℕ) : ℤ) ≡
+          ((2 * S - (c + d) : ℕ) : ℤ) - ((2 * S - (c + d) : ℕ) : ℤ) [ZMOD L₁] :=
+          Int.ModEq.sub (Int.ModEq.refl _) h_eq
+        have hzero : ((2 * S - (c + d) : ℕ) : ℤ) - ((2 * S - (c + d) : ℕ) : ℤ) = 0 := by ring
+        simpa [hzero] using h_sub_eq
+      have h_sub_simp : ((2 * S - (c + d) : ℕ) : ℤ) - ((2 * S - (a + b) : ℕ) : ℤ) = 
+          ((a + b : ℤ) - (c + d : ℤ)) := by
+        omega
+      rw [h_sub_simp] at h_sub
+      exact (Int.modEq_zero_iff_dvd.mp h_sub)
+    exact dvd_mod_eq (a + b) (c + d) L₁ h_dvd
+  -- Step 3: By CRT, a+b = c+d (since both < L₀*L₁)
+  have heq : a + b = c + d :=
+    mod_eq_of_coprime hCoprime hL₀ hL₁ habL₀ habL₁ (hBound a ha b hb) (hBound c hc d hd)
+  -- Step 4: By Sidon
+  rcases hSidon ha hb hc hd heq with (⟨hac, hbd⟩ | ⟨had, hbc⟩)
+  · exact Or.inl ⟨hac, hbd⟩
+  · exact Or.inr ⟨had, hbc⟩
+
 end CoreFormalism.CRTSidon
--- a/formal/CoreFormalism/LeanCopilotFill.lean
+++ b/formal/CoreFormalism/LeanCopilotFill.lean
@ -1,23 +1,7 @@
-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
+/-- The sidon_preserved theorem is now proven in CRTSidon.lean.
+    This file is a placeholder for future LeanCopilot-powered proof filling. -/
+#check sidon_preserved
--- a/formal/SilverSight/GoldenSpiral.lean
+++ b/formal/SilverSight/GoldenSpiral.lean
@ -66,15 +66,16 @@ noncomputable def goldenAngle : ℝ := 2 * Real.pi / phi ^ 2

 /-! §2 Q16_16 Fixed-Point Constants -/

-/-- φ⁻¹ in Q16_16: round(65536 × 0.6180340) = 40560. -/
-def phiInvQ16 : Q16_16 := ofRawInt 40560
+/-- φ⁻¹ in Q16_16: round(65536 × 0.6180340) = 40504.
+    Corrected from 40560 (0.14% relative error). -/
+def phiInvQ16 : Q16_16 := ofRawInt 40504

-/-- φ⁻¹·cos(θ_g) in Q16_16: round(65536 × 0.6180340 × 0.7373699) ≈ 29866.
+/-- φ⁻¹·cos(θ_g) in Q16_16: round(65536 × 0.6180340 × (-0.7373699)) ≈ -29860.
    Actually negative: the cosine of the golden angle is negative. -/
-def goldenSpiralCos : Q16_16 := ofRawInt (-29866)
+def goldenSpiralCos : Q16_16 := ofRawInt (-29860)

-/-- φ⁻¹·sin(θ_g) in Q16_16: round(65536 × 0.6180340 × 0.6754903) ≈ 27360. -/
-def goldenSpiralSin : Q16_16 := ofRawInt 27360
+/-- φ⁻¹·sin(θ_g) in Q16_16: round(65536 × 0.6180340 × 0.6754903) ≈ 27357. -/
+def goldenSpiralSin : Q16_16 := ofRawInt 27357

 /-! §3 The 16×16 Golden Spiral Matrix

@ -232,7 +233,7 @@ theorem cost_outpaces_convergence (k : Nat) (hk : k ≥ 1) :

 /-! §7 Evaluation Witnesses -/

-#eval phiInvQ16  -- 40560 (≈ 0.618)
+#eval phiInvQ16  -- 40504 (≈ 0.618)
 #eval goldenSpiralCos  -- -29866
 #eval goldenSpiralSin  -- 27360

--- a/scripts/mcp_autoproof.py
+++ b/scripts/mcp_autoproof.py
@ -54,6 +54,45 @@ def release_lock(name: str):
        os.close(fd)
    except: pass

+# ── Worker Pool ─────────────────────────────────────────────────────────────
+
+WORKER_DIR = SILVERSIGHT / ".lake" / "autoproof_workers"
+WORKER_DIR.mkdir(parents=True, exist_ok=True)
+MAX_WORKERS = 4
+ACTIVE_WORKERS = []
+
+def spawn_worker(worker_id: int):
+    """Spawn a background worker process for handling proofs."""
+    cmd = [
+        sys.executable,
+        str(SILVERSIGHT / "scripts" / "mcp_worker.py"),
+        "--worker-id", str(worker_id),
+        "--stdio"
+    ]
+    proc = subprocess.Popen(
+        cmd,
+        stdin=subprocess.PIPE,
+        stdout=subprocess.PIPE,
+        stderr=subprocess.PIPE,
+        cwd=SILVERSIGHT
+    )
+    ACTIVE_WORKERS.append(proc)
+    return proc
+
+def get_worker_count() -> int:
+    """Count active workers."""
+    return len([p for p in ACTIVE_WORKERS if p.poll() is None])
+
+def maybe_spawn_workers():
+    """Spawn more workers if under load (queue depth > available workers)."""
+    queue_depth = len(ACTIVE_WORKERS)
+    if queue_depth < MAX_WORKERS:
+        # Check if we have high concurrency demand
+        if queue_depth > 1:
+            for i in range(MAX_WORKERS - queue_depth):
+                spawn_worker(queue_depth + i)
+                time.sleep(0.1)
+
 # ── Lean Utils ────────────────────────────────────────────────────────────

 def find_sorry(filepath: str):
@ -219,7 +258,7 @@ def handle_request(request):
        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, "result": {"content": [{"text": json.dumps(result)}]}}
    
    return {"id": req_id, "error": {"code": -32601, "message": f"Method not found: {method}"}}