diff --git a/AGENTS.md b/AGENTS.md index da53053f..bd20e062 100644 --- 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 | diff --git a/CITATION.cff b/CITATION.cff index 6b916329..51f8cf3b 100644 --- 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 diff --git a/docs/research/SLOS_SIDON_VERIFICATION_RECEIPT.md b/docs/research/SLOS_SIDON_VERIFICATION_RECEIPT.md index 99cd906b..359a29fa 100644 --- 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. diff --git a/docs/research/sidon_preservation_creation.md b/docs/research/sidon_preservation_creation.md index 7dfa50a1..b2e4a648 100644 --- 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): diff --git a/formal/CoreFormalism/BraidEigensolid.lean b/formal/CoreFormalism/BraidEigensolid.lean index 25d9fda3..970345fb 100644 --- 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 diff --git a/formal/CoreFormalism/CRTSidon.lean b/formal/CoreFormalism/CRTSidon.lean index eca08da4..50cb77b1 100644 --- 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 diff --git a/formal/CoreFormalism/LeanCopilotFill.lean b/formal/CoreFormalism/LeanCopilotFill.lean index 96340e68..a75b1000 100644 --- 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 diff --git a/formal/SilverSight/GoldenSpiral.lean b/formal/SilverSight/GoldenSpiral.lean index c3399fad..bf26fc60 100644 --- 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 diff --git a/scripts/mcp_autoproof.py b/scripts/mcp_autoproof.py index b787c2aa..53e1afcd 100755 --- 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}"}}