From af56eab7dd4e07a90be2cc5c31df2b8de7ca312b Mon Sep 17 00:00:00 2001
From: Allaun Silverfox <28494262+allaunthefox@users.noreply.github.com>
Date: Thu, 2 Jul 2026 03:31:14 +0200
Subject: [PATCH] Remove BMS_VERIFICATION.md

---
 docs/BMS_VERIFICATION.md | 70 ----------------------------------------
 1 file changed, 70 deletions(-)
 delete mode 100644 docs/BMS_VERIFICATION.md

diff --git a/docs/BMS_VERIFICATION.md b/docs/BMS_VERIFICATION.md
deleted file mode 100644
index a73c6fbc..00000000
--- a/docs/BMS_VERIFICATION.md
+++ /dev/null
@@ -1,70 +0,0 @@
-# BMS Domain Verification — TI-84 Level
-
-**Date:** 2026-06-23
-**Method:** Brute-force enumeration of all 979 parameter pairs
-**Tool:** Python (any calculator with integer arithmetic)
-
----
-
-## BMS Domain
-
-$$x \in [2, 90], \quad m \in [3, 13]$$
-$$89 \times 11 = 979 \text{ parameter pairs}$$
-
-## Repunit Function
-
-$$R(x, m) = \frac{x^m - 1}{x - 1}$$
-
-## Results
-
-| Metric | Value |
-|--------|-------|
-| Total parameter pairs | 979 |
-| Distinct repunit values | 977 |
-| Collision groups | **2** |
-| Goormaghtigh solution 1 | R(2,5) = 31 = R(5,3) |
-| Goormaghtigh solution 2 | R(2,13) = 8191 = R(90,3) |
-| Closest non-Goormaghtigh pair | R(41,11) vs R(62,10) |
-| Closest threshold | 0.000028 (28 ppm) |
-| Merge gate threshold | 10^-6 = 0.000001 |
-| **Safety margin** | **28×** |
-
-## Verification
-
-```python
-def repunit(x, m):
-    return (x**m - 1) // (x - 1) if x > 1 and m > 0 else 0
-
-# Find all collisions
-repunit_map = {}
-for x in range(2, 91):
-    for m in range(3, 14):
-        r = repunit(x, m)
-        repunit_map.setdefault(r, []).append((x, m))
-
-collisions = {r: p for r, p in repunit_map.items() if len(p) > 1}
-# Result: {31: [(2,5),(5,3)], 8191: [(2,13),(90,3)]}
-```
-
-## Implication
-
-The only equal-repunit pairs in the BMS domain are the two Goormaghtigh solutions. All other pairs have a relative difference > 10^-6 (28× safety margin).
-
-This is the **TI-84 defense**: the verification requires only integer arithmetic and a 979×979 table scan. No transcendental number theory, no Baker/Matveev, no LLL. Pure computation.
-
-## Bug in Theorem Statement
-
-The theorem `unknown_fails_rrc` in `section4_rrc_kernel.lean` has a bug:
-
-```lean
-theorem unknown_fails_rrc (x m y n : ℕ)
-    (h : repunit x m = repunit y n)  -- BUG: forces threshold = 0
-    ...
-    ¬(kernelEvidence x m y n).mergeAdmissible  -- BUG: contradicts h
-```
-
-If `repunit x m = repunit y n`, then `mergeAdmissibleThreshold = 0 < 10^-6`, so `mergeAdmissible = true`. But the conclusion says `¬mergeAdmissible`. This is contradictory.
-
-**Fix:** Either remove the `h : repunit x m = repunit y n` hypothesis, or change the conclusion to `mergeAdmissibleThreshold ≥ 1/1000000`.
-
-The corollary at line 431-438 also needs updating to match.