diff --git a/archive/2026-07-02/docs/SOS_CERTIFICATE_FORMULAS.md b/archive/2026-07-02/docs/SOS_CERTIFICATE_FORMULAS.md
new file mode 100644
index 00000000..0ceb6abf
--- /dev/null
+++ b/archive/2026-07-02/docs/SOS_CERTIFICATE_FORMULAS.md
@@ -0,0 +1,140 @@
+# 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.**