fix(lean): inline E8Sidon divisor sums to remove unmerged dependency

PolyFactorIdentity previously imported Semantics.E8Sidon which only
exists on the unmerged PR #80 branch. Replaced with standalone
sigma3/sigma7/convolutionLHS definitions that are API-compatible.

Build: 3300 jobs, 0 errors (lake build Semantics.RRC.PolyFactorIdentity)
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>

0-Core-Formalism/lean/Semantics/Semantics/RRC/PolyFactorIdentity.lean

@@ -3,7 +3,6 @@ Copyright (c) 2026 Research Stack Contributors. All rights reserved.
 Released under Apache 2.0 license.
 -/
 import Semantics.FixedPoint
-import Semantics.E8Sidon
 
 /-!
 # Polynomial Factor Identity — Short-Sleeve Detection for RRC
@@ -56,7 +55,31 @@ mathematical objects by their algebraic decomposability.
 namespace Semantics.RRC.PolyFactorIdentity
 
 open Semantics.FixedPoint
-open Semantics.E8Sidon
+
+-- ═══════════════════════════════════════════════════════════════════════════════
+-- §0. Standalone Divisor Sum Definitions (E8Sidon-compatible)
+-- ═══════════════════════════════════════════════════════════════════════════════
+
+/-- Divisors of n. -/
+private def divisors (n : Nat) : List Nat :=
+  if n == 0 then []
+  else (List.range n).map (· + 1) |>.filter (n % · == 0)
+
+/-- σ₃(n) = Σ d³ for d | n.  Matches E8Sidon.sigma3. -/
+def sigma3 (n : Nat) : Nat :=
+  (divisors n).foldl (fun acc d => acc + d ^ 3) 0
+
+/-- σ₇(n) = Σ d⁷ for d | n.  Matches E8Sidon.sigma7. -/
+def sigma7 (n : Nat) : Nat :=
+  (divisors n).foldl (fun acc d => acc + d ^ 7) 0
+
+/-- Cauchy-product convolution: Σ_{m=1}^{n-1} σ₃(m)·σ₃(n-m).
+    Matches E8Sidon.convolutionLHS. -/
+def convolutionLHS (n : Nat) : Nat :=
+  if n ≤ 1 then 0
+  else
+    let terms := (List.range (n - 1)).map (· + 1)  -- [1, ..., n-1]
+    terms.foldl (fun acc m => acc + sigma3 m * sigma3 (n - m)) 0
 
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §1. Limb Decomposition (the zerocopy view)