From 526357e391b612058266d5331900311fc0fee20b Mon Sep 17 00:00:00 2001
From: openresearch <bot@openresearch.sh>
Date: Fri, 3 Jul 2026 11:12:47 +0000
Subject: [PATCH] =?UTF-8?q?docs(E8Sidon):=20honest=20Erd=C5=91s=2030=20con?=
 =?UTF-8?q?nection,=20no=20false=20claims?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Rewrote the E8Sidon.lean module header to honestly state the
connection to Erdős Problem 30 (https://www.erdosproblems.com/30):

- The problem: is h(N) = N^{1/2} + O_ε(N^ε)? (000, open)
- Current bounds: upper by Carter-Hunter-O'Bryant 2025,
  lower by Singer 1938
- What this module provides: power-of-2 Sidon labels (weaker than
  Singer), E₈ convolution identity (connects to root system, does
  NOT improve Erdős 30 bounds)
- What was abandoned: the false claim that E₈ level sets are Sidon
  (disproven at N=32, SORRY PROTOCOL Option C)
- What the pipeline may contribute: DNA-encoded search for large
  Sidon sets via thermodynamic energy descent (future work, not proven)

The previous header claimed 'improves the unconditional bound from
ε ≥ 1/2 to ε ≥ 1/4' — this was false and is removed.

Also: eigensolid_convergence and receipt_invertible in BraidEigensolid.lean
are already proven (not sorry). rossby_energy_dissipation_rate in
BraidStateN.lean is already proven (rfl; omega). No changes needed
to those theorems.
---
 formal/CoreFormalism/E8Sidon.lean | 34 +++++++++++++++++++++++++------
 1 file changed, 28 insertions(+), 6 deletions(-)

diff --git a/formal/CoreFormalism/E8Sidon.lean b/formal/CoreFormalism/E8Sidon.lean
index 4dda0d51..9a648136 100644
--- a/formal/CoreFormalism/E8Sidon.lean
+++ b/formal/CoreFormalism/E8Sidon.lean
@@ -1,14 +1,36 @@
 /- Copyright (c) 2026 SilverSight Contributors. All rights reserved.
 
-E₈ Sidon Prototype — Erdős 30 conditional improvement
+E₈ Sidon Prototype — Erdős Problem 30 connection
 Port of critical theorems from Research Stack `Semantics.E8Sidon`.
 
-Key claim: σ₃-bounded multiplicative level sets are Sidon, which
-improves the unconditional bound on Erdős Problem 30 from ε ≥ 1/2
-to ε ≥ 1/4 with logarithmic correction.
+Erdős Problem 30 (https://www.erdosproblems.com/30, $1000 prize):
+  Is h(N) = N^{1/2} + O_ε(N^ε) for every ε > 0?
+  where h(N) = maximum size of a Sidon set in {1,...,N}.
 
-Status: computational verification for n ≤ 200 via native_decide;
-full structural proof pending.
+Current bounds:
+  Upper: h(N) ≤ N^{1/2} + 0.98183·N^{1/4} + O(1)  [Carter-Hunter-O'Bryant 2025]
+  Lower: h(N) ≥ (1-o(1))·N^{1/2}                   [Singer 1938]
+
+What this module provides:
+  - The power-of-2 labels {1,2,4,8,16,32,64,128} are Sidon (binary uniqueness).
+    This is a specific Sidon set of size 8 in {1,...,128}, giving h(128) ≥ 8.
+    This is WEAKER than Singer's construction (which gives ~√N for all N).
+  - The E₈ convolution identity σ₇ = σ₃ + 120·Σ σ₃(j)·σ₃(n-j) (E₄² = E₈).
+    This connects divisor sums to the E₈ root system but does NOT directly
+    improve the Erdős 30 bounds.
+
+What was abandoned (SORRY PROTOCOL Option C):
+  - The claim "E₈ level sets are Sidon for N ≤ 200" was DISPROVEN.
+    E8LevelSet 32 = {1,2,3} is NOT Sidon: 1+3 = 2+2 = 4.
+    See levelset_32_NOT_sidon below.
+
+What the pipeline may contribute (future work, not proven):
+  The DNA encoder can compress Sidon set candidates into hachimoji DNA
+  and use thermodynamic energy descent (PCR/hybridization filtering) to
+  search for large Sidon sets in {1,...,N}. This is the NP-hard boss
+  target — not a proof, but a computational search tool. The formal
+  verification stack ensures the encoding is faithful (exact arithmetic,
+  injective mapping, no float artifacts).
 -/
 
 import Mathlib