From bba1fed2199090a3fbb5dce7456f2869119e1a37 Mon Sep 17 00:00:00 2001 From: Allaun Silverfox <28494262+allaunthefox@users.noreply.github.com> Date: Thu, 2 Jul 2026 03:34:57 +0200 Subject: [PATCH] Remove SOS_CERTIFICATE_FORMULAS.md --- docs/SOS_CERTIFICATE_FORMULAS.md | 140 ------------------------------- 1 file changed, 140 deletions(-) delete mode 100644 docs/SOS_CERTIFICATE_FORMULAS.md diff --git a/docs/SOS_CERTIFICATE_FORMULAS.md b/docs/SOS_CERTIFICATE_FORMULAS.md deleted file mode 100644 index 0ceb6abf..00000000 --- a/docs/SOS_CERTIFICATE_FORMULAS.md +++ /dev/null @@ -1,140 +0,0 @@ -# SOS Certificate — Replaces Baker's Application in the Merge Gate - -No English. Pure math. Graph-calculator verifiable. - ---- - -## The Problem - -$$\Lambda = \sum_{i=0}^{n} \beta_i \log \alpha_i \neq 0 \implies |\Lambda| > e^{-C \cdot \prod A_i \cdot \log B}$$ - -**Wall:** Requires Matveev's theorem (transcendence theory, ~1000 lines not in Lean). - -## The Replacement - -$$p(x) \geq 0 \text{ on } K \implies p(x) = \sum_{i} q_i(x)^2$$ - -**No wall:** Requires polynomial arithmetic only. Computationally verifiable. - ---- - -## 1. SOS Certificate - -$$p(x) = \sum_{i=0}^{k} q_i(x)^2$$ - -$$q_i(x) = \sum_{j} c_{ij} x^{e_j}$$ - -**Verification:** -``` -p(x) = x² + 2x + 1 -q₀(x) = x + 1 -q₀(x)² = (x+1)² = x² + 2x + 1 = p(x) ✓ -``` - -## 2. Semialgebraic Set - -$$K = \{x : g_1(x) \geq 0, \ldots, g_m(x) \geq 0\}$$ - -**Verification:** -``` -K = {x : x ≥ 0, x ≤ 1} -g₁(x) = x, g₂(x) = 1 - x -K = [0, 1] ✓ -``` - -## 3. Putinar's Positivstellensatz - -$$p(x) \geq 0 \text{ on } K \implies p(x) = s_0(x) + \sum_{i} s_i(x) \cdot g_i(x)$$ - -**Requires Archimedean condition:** the quadratic module generated by $\{g_i\}$ must be Archimedean (i.e., $N - \sum x_i^2$ lies in the quadratic module for some $N$). For bounded domains like the BMS box $[2,90] \times [3,13]$, this condition holds. - -$$s_0(x) = \sum_j q_j(x)^2 \quad (\text{SOS})$$ - -$$s_i(x) = \sum_j r_{ij}(x)^2 \quad (\text{SOS for each } i)$$ - -**Verification:** -``` -p(x) = x² on K = [0,1] -g₁(x) = x, g₂(x) = 1-x -s₀(x) = x² = (x)² (SOS: perfect square) -s₁(x) = 0, s₂(x) = 0 -p(x) = s₀(x) + s₁(x)·g₁(x) + s₂(x)·g₂(x) = x² ✓ -``` - -## 4. Gap Polynomial - -$$\text{gap}(x, m) = \text{sieve}(x, m) - \text{threshold}$$ - -$$\text{sieve}(x, m) = H_{m,m}(x, -1, x, -1, \tfrac{1}{2})$$ - -$$\text{threshold} = 10^{-6}$$ - -**Claim:** `gap(x, m) ≥ 0` on BMS domain $K = \{x \in [2,90], m \in [3,13]\}$. - -**Proof:** SOS certificate showing `gap(x, m)` is a sum of squares on $K$. - -## 5. SOS Certificate for Gap - -$$\text{gap}(x, m) = s_0(x, m) + s_1(x, m) \cdot (x - 2) + s_2(x, m) \cdot (90 - x) + s_3(x, m) \cdot (m - 3) + s_4(x, m) \cdot (13 - m)$$ - -$$s_i(x, m) = \sum_j q_{ij}(x, m)^2$$ - -**Verification:** -``` -For each (x, m) in BMS domain: - gap(x, m) = s₀ + s₁·(x-2) + s₂·(90-x) + s₃·(m-3) + s₄·(13-m) - All sᵢ ≥ 0 (SOS) - All gᵢ ≥ 0 on K - ∴ gap(x, m) ≥ 0 ✓ -``` - -## 6. Connection to Baker - -**Baker's theorem (transcendence theory):** - -$$\Lambda = \sum_{i=0}^{n} \beta_i \log \alpha_i \neq 0 \implies |\Lambda| > e^{-C}$$ - -This is a lower bound on a **non-vanishing transcendental expression**. Baker is needed when the statement of interest is "this linear form in logarithms is non-zero and I need an explicit quantitative bound." - -**SOS certificate (polynomial non-negativity):** - -$$\text{gap}(x,m) \geq 0 \text{ on } K$$ - -This is a **non-negativity certificate for a specific polynomial on a compact semialgebraic domain**. It has nothing to do with logarithms or transcendence. - -**Are they equivalent? No.** They prove different types of statements about different objects. Baker bounds a transcendental expression away from zero. SOS certifies that a polynomial stays non-negative on a domain. The two are incommensurable. - -**Why the merge gate does not need Baker:** The gate condition is: - -$$\text{gap}(x,m) \geq 0 \quad \forall (x,m) \in [2,90] \times [3,13]$$ - -This is a pure polynomial non-negativity condition. Historically, one might have attempted to prove this via: - -1. Express `gap` in terms of a linear form in logarithms. -2. Apply Baker/Matveev to bound the form away from zero. -3. Conclude `gap ≥ 0` by converting the Baker bound. - -Step 1 requires expressing the gap — a polynomial — in terms of transcendental functions, which is circuitous and fragile. The SOS approach skips all three steps and proves `gap ≥ 0` directly. - -**What SOS replaces:** The *application* of Baker as the proof strategy for this specific gate — not Baker's theorem itself. The SOS certificate is an independent, self-contained proof of `gap ≥ 0` that avoids the transcendence wall entirely. - -**Correct flow:** - -$$\text{build SOS certificate with SDP solver}$$ -$$\implies \text{verify Putinar representation in Lean}$$ -$$\implies \text{gap}(x,m) \geq 0 \text{ on } K$$ -$$\implies \text{merge gate holds}$$ - -**No Baker arrow exists in either direction.** Baker does not imply an SOS certificate exists (transcendence theory has no bearing on SOS representability). An SOS certificate does not imply anything about Baker's theorem. - -## 7. Verification Protocol - -``` -1. Define gap(x, m) as polynomial -2. Define K = BMS domain -3. Compute SOS certificate via SDP solver -4. Verify certificate in Lean (expand and compare) -5. ∴ gap ≥ 0 on K ✓ -``` - -**No Baker. No Matveev. No transcendence theory applied here. Pure polynomial arithmetic.**