From 0ef6ddbc60c56b983e6a6c660ff44c4bcc371851 Mon Sep 17 00:00:00 2001
From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com>
Date: Mon, 15 Jun 2026 20:27:49 +0000
Subject: [PATCH] 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>
---
 .../Semantics/RRC/PolyFactorIdentity.lean     | 27 +++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

diff --git a/0-Core-Formalism/lean/Semantics/Semantics/RRC/PolyFactorIdentity.lean b/0-Core-Formalism/lean/Semantics/Semantics/RRC/PolyFactorIdentity.lean
index bddddb35..48e16684 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/RRC/PolyFactorIdentity.lean
+++ b/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)