feat: pull research platform results — HN database + q-sweep + CRTSidonN

- HN spectral database: 6 graphs measured, de Grey 1581 shows gap=2
  (larger than Moser/Golomb gap=1 — spectral info degrades with size)
- CRT q-profile sweep: refutes toroidal/poloidal prediction — q>1 beats q<1.
  Mechanism: larger M = L₀·L₁ for q>1 gives more CRT headroom
- CRTSidonN.lean: n-moduli generalization (auto-generated, needs mathlib API fix)
- Gerver Sidon design: Direction B design document
- Lakefile: CRTSidonN registered but commented out (builds with 0 errors)

Build: lake build CoreFormalism.CRTSidon (3297 jobs, 0 errors)

.openresearch/artifacts/hn_spectral_database.json

@@ -1,7 +1,7 @@
 {
   "experiment": "hn_spectral_database",
-  "timestamp": "2026-07-04T08:50:51Z",
-  "include_degrey": false,
+  "timestamp": "2026-07-04T15:01:00Z",
+  "include_degrey": true,
   "graphs": [
     {
       "description": "Moser spindle",
@@ -11,8 +11,8 @@
       "lambda_min": -2.0,
       "hoffman_bound": 2.822875655532,
       "chi_hoffman": 3,
-      "welch_wynn": null,
-      "chi_welch_wynn": null,
+      "welch_wynn": 2.086905488878,
+      "chi_welch_wynn": 3,
       "best_spectral_lower_bound": 3,
       "chi_known": 4,
       "gap": "gap=1"
@@ -25,8 +25,8 @@
       "lambda_min": -2.323404276086,
       "hoffman_bound": 2.154052556071,
       "chi_hoffman": 3,
-      "welch_wynn": null,
-      "chi_welch_wynn": null,
+      "welch_wynn": 1.504135614368,
+      "chi_welch_wynn": 2,
       "best_spectral_lower_bound": 3,
       "chi_known": 4,
       "gap": "gap=1"
@@ -39,11 +39,11 @@
       "lambda_min": 0.0,
       "hoffman_bound": null,
       "chi_hoffman": null,
-      "welch_wynn": null,
-      "chi_welch_wynn": null,
-      "best_spectral_lower_bound": null,
+      "welch_wynn": 1.0,
+      "chi_welch_wynn": 1,
+      "best_spectral_lower_bound": 1,
       "chi_known": 1,
-      "gap": "?"
+      "gap": "tight"
     },
     {
       "description": "Path graph P10 (baseline)",
@@ -53,8 +53,8 @@
       "lambda_min": -1.918985947229,
       "hoffman_bound": 2.0,
       "chi_hoffman": 2,
-      "welch_wynn": null,
-      "chi_welch_wynn": null,
+      "welch_wynn": 1.237468458129,
+      "chi_welch_wynn": 2,
       "best_spectral_lower_bound": 2,
       "chi_known": 2,
       "gap": "tight"
@@ -67,8 +67,8 @@
       "lambda_min": -1.61803398875,
       "hoffman_bound": 2.2360679775,
       "chi_hoffman": 3,
-      "welch_wynn": null,
-      "chi_welch_wynn": null,
+      "welch_wynn": 1.666666666667,
+      "chi_welch_wynn": 2,
       "best_spectral_lower_bound": 3,
       "chi_known": 3,
       "gap": "tight"
@@ -81,12 +81,82 @@
       "lambda_min": -1.0,
       "hoffman_bound": 4.0,
       "chi_hoffman": 4,
-      "welch_wynn": null,
-      "chi_welch_wynn": null,
+      "welch_wynn": 4.0,
+      "chi_welch_wynn": 4,
       "best_spectral_lower_bound": 4,
       "chi_known": 4,
       "gap": "tight"
+    },
+    {
+      "description": "De Grey G (1581 vertices, 7877 edges)",
+      "n_vertices": 1581,
+      "n_edges": 7877,
+      "lambda_max": 12.091766719308,
+      "lambda_min": -7.73894638212,
+      "hoffman_bound": 2.562456453665,
+      "chi_hoffman": 3,
+      "welch_wynn": null,
+      "chi_welch_wynn": null,
+      "best_spectral_lower_bound": 3,
+      "chi_known": 5,
+      "gap": "gap=2"
+    },
+    {
+      "description": "de Grey subgraph (n=50, e=100)",
+      "n_vertices": 50,
+      "n_edges": 100,
+      "lambda_max": 5.866375245109,
+      "lambda_min": -4.056427910215,
+      "hoffman_bound": 2.446192407447,
+      "chi_hoffman": 3,
+      "welch_wynn": 1.132923032669,
+      "chi_welch_wynn": 2,
+      "best_spectral_lower_bound": 3,
+      "chi_known": null,
+      "gap": "?"
+    },
+    {
+      "description": "de Grey subgraph (n=100, e=266)",
+      "n_vertices": 100,
+      "n_edges": 266,
+      "lambda_max": 7.080506734483,
+      "lambda_min": -4.563418201316,
+      "hoffman_bound": 2.551579632224,
+      "chi_hoffman": 3,
+      "welch_wynn": null,
+      "chi_welch_wynn": null,
+      "best_spectral_lower_bound": 3,
+      "chi_known": null,
+      "gap": "?"
+    },
+    {
+      "description": "de Grey subgraph (n=200, e=747)",
+      "n_vertices": 200,
+      "n_edges": 747,
+      "lambda_max": 9.241919119832,
+      "lambda_min": -5.218824047335,
+      "hoffman_bound": 2.770881531166,
+      "chi_hoffman": 3,
+      "welch_wynn": null,
+      "chi_welch_wynn": null,
+      "best_spectral_lower_bound": 3,
+      "chi_known": null,
+      "gap": "?"
+    },
+    {
+      "description": "de Grey subgraph (n=500, e=2242)",
+      "n_vertices": 500,
+      "n_edges": 2242,
+      "lambda_max": 11.690329949761,
+      "lambda_min": -7.523976221726,
+      "hoffman_bound": 2.553743606473,
+      "chi_hoffman": 3,
+      "welch_wynn": null,
+      "chi_welch_wynn": null,
+      "best_spectral_lower_bound": 3,
+      "chi_known": null,
+      "gap": "?"
     }
   ],
-  "sha256": "6af248bdf51d4a90b6e286e4decc33f60b153b4b162c677ecfbaf9f12b20641c"
-}
+  "sha256": "2041b3ce8902f73ae8b92f1696b6badbd69718d30304c78dfa61ec67b5e270c1"
+}

formal/CoreFormalism/CRTSidonN.lean

@@ -1,4 +1,3 @@
-/-
 import Mathlib.Data.Int.ModEq
 import Mathlib.Data.Nat.GCD.Basic
 import Mathlib.Data.Finset.Basic
@@ -7,7 +6,7 @@ import Mathlib.Tactic
 
 open Finset
 
-namespace CoreFormalism.CRTSidon
+namespace CoreFormalism.CRTSidonN
 
 /-!
 # CRT Sidon Preservation: n-moduli generalization
@@ -30,13 +29,8 @@ the 2-moduli case (`mod_eq_of_coprime`) as the inductive step.
 The reflection components (i ≥ 1) all reduce to (a+b) ≡ (c+d) (mod Lᵢ)
 via the same algebraic manipulation as the 2-moduli case:
   (S-a) + (S-b) = 2S - (a+b), so
-  (2S - (a+b)) % Lᵢ = (2S - (c+d)) % Lᵢ implies (a+b) ≡ (c+d) (mod Lᵢ).
+  (2S - (a+b)) % Lᵢ = (2S - (c+d)) % Lᵢ implies (a+b) ≡ (c+d) (mod Lᵢ). -/
 
-This module provides:
-1. `mod_eq_of_coprime_list` — generalized CRT uniqueness (n moduli)
-2. `reflection_implies_sum_cong` — reflection component → sum congruence
-3. `sidon_preserved_mod_n` — main theorem (n-moduli version)
--/
 
 /-- A Sidon set: all unordered pairwise sums are distinct. -/
 def IsSidon (A : Finset ℕ) : Prop :=
@@ -88,8 +82,8 @@ If L is a pairwise coprime list, and each Lᵢ divides d, then
 ∏Lᵢ divides d. This is the heart of the generalized CRT.
 
 We prove this by strong induction on the list length.
--/
 
+-/
 /-- Product of a list of ℕ. -/
 def listProd (ls : List ℕ) : ℕ := ls.prod
 
@@ -103,8 +97,8 @@ def listProd (ls : List ℕ) : ℕ := ls.prod
       Since L₀ is coprime to each element of tail, L₀ is coprime to ∏tail
       (coprime to product = coprime to each factor)
       Since L₀ ∣ d and (∏tail) ∣ d and gcd(L₀, ∏tail) = 1:
-      L₀ * (∏tail) ∣ d  (i.e., (∏(L₀ :: tail)) ∣ d)
 -/
+      L₀ * (∏tail) ∣ d  (i.e., (∏(L₀ :: tail)) ∣ d)
 theorem pairwise_coprime_product_dvd (L : List ℕ) (hCoprime : PairwiseCoprime L)
     (hDiv : ∀ i (hi : i < L.length), (L.get ⟨i, hi⟩) ∣ d) :
     L.prod ∣ d := by
@@ -329,4 +323,4 @@ theorem sidon_preserved_mod_n (A : Finset ℕ) (hSidon : IsSidon A) (S : ℕ)
   · exact Or.inl ⟨hac, hbd⟩
   · exact Or.inr ⟨had, hbc⟩
 
-end CoreFormalism.CRTSidon
+end CoreFormalism.CRTSidonN

lakefile.lean

@@ -47,6 +47,7 @@ lean_lib «SilverSightFormal» where
     `CoreFormalism.HopfFibration,
     `CoreFormalism.StrandCapacityBound,
     `CoreFormalism.CRTSidon,
+    -- `CoreFormalism.CRTSidonN,  -- TODO(lean-port): auto-generated, targets different mathlib API
     `SilverSight.AngrySphinx,
     `SilverSight.CollatzBraid,
     `SilverSight.GoldenSpiral,