From 1bd5e557293e10a1cefd21eccf5e8560efbb5d59 Mon Sep 17 00:00:00 2001 From: allaun Date: Sat, 4 Jul 2026 10:06:17 -0500 Subject: [PATCH] =?UTF-8?q?feat:=20pull=20research=20platform=20results=20?= =?UTF-8?q?=E2=80=94=20HN=20database=20+=20q-sweep=20+=20CRTSidonN?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 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) --- .../artifacts/hn_spectral_database.json | 106 +++++++++++++++--- formal/CoreFormalism/CRTSidonN.lean | 16 +-- lakefile.lean | 1 + 3 files changed, 94 insertions(+), 29 deletions(-) diff --git a/.openresearch/artifacts/hn_spectral_database.json b/.openresearch/artifacts/hn_spectral_database.json index ccb004fe..eb5a74cb 100644 --- a/.openresearch/artifacts/hn_spectral_database.json +++ b/.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" +} \ No newline at end of file diff --git a/formal/CoreFormalism/CRTSidonN.lean b/formal/CoreFormalism/CRTSidonN.lean index efe5b3b4..6552a977 100644 --- a/formal/CoreFormalism/CRTSidonN.lean +++ b/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 diff --git a/lakefile.lean b/lakefile.lean index 696b3f70..023b9b44 100644 --- a/lakefile.lean +++ b/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,