Record the spare bits in the online storage budget

research/storage-spare-bits/README.md

@@ -0,0 +1,40 @@
+# Spare bits in the online storage budget
+
+## Question
+
+The published online magnitudes are bounded by terms such as `2^(8p+18) p^2` and `2^18 p^4`. Does the budget
+
+```
+G = 8p + 8 ceil(log2(p+2)) + 32
+```
+
+leave twelve spare magnitude bits?
+
+## Result
+
+For every precision `p >= 101`, write `c = ceil(log2(p+2))`. Then `c >= 7` and `p < 2^c`, so `p^2` has at most `2c` bits. The prefix bound `2^(8p+18) p^2` therefore has bit length at most `8p+18+2c`, and
+
+```
+G - (8p+18+2c) = 6c+14 >= 56.
+```
+
+The spare is at least 56, which covers the claimed twelve bits. On precisions 101 through 300 the prefix bound is the widest of the 13 published magnitudes, and each of those 2,600 bit lengths fits in `G-56`. The minimum spare on that range is 56, at precision 101. The selected κ is unchanged.
+
+## Boundary
+
+This checks the bit-length comparison. It does not run the Gaussian core. The stop rule is to record this spare.
+
+## Reproduce
+
+```bash
+python3.12 -B research/storage-spare-bits/verify.py
+python3.12 -B research/storage-spare-bits/test_verify.py
+```
+
+## Open next questions
+
+None. The bit-length comparison settles the twelve-bit claim. The Gaussian core would leave this package.
+
+## Credit
+
+Jose Manuel (`jmbarrancoml`) recorded the storage budget in PR #3851. The checker compares it with the stated magnitudes. Substantial assistance from the Cursor coding agent contributed to the execution, checker and writeup.

research/storage-spare-bits/RESULT.json

@@ -0,0 +1,5 @@
+{
+  "checks": 2600,
+  "minimum_spare": 56,
+  "no_new_kappa": true
+}

research/storage-spare-bits/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    }
+  ]
+}

research/storage-spare-bits/TASK.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 6,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/hyperplane-end-lean/PROOF.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Prove that the published online magnitude bounds fit in the storage budget G with at least twelve spare bits.",
+  "scope_change_reason": "The boundary band, q-factorization, Neumann tail, production domain, and error sum are different questions. This package checks the storage spare bits. It does not run the Gaussian core.",
+  "bottleneck_link": "Every checked magnitude fits in G with at least 56 spare bits, and the selected kappa is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Record this spare. Do not run the Gaussian core.",
+  "outcome": "partial",
+  "evidence": "For every precision from 101 through 300, all 13 published magnitude bounds have bit length at most G-56. The prefix bound is the largest, and its spare is at least 56 for every precision at least 101.",
+  "author": "jwr",
+  "ai_assistance": "Substantial assistance from the Cursor coding agent in the execution, checker and writeup.",
+  "open_questions": [],
+  "no_open_questions_reason": "The bit-length comparison settles the twelve-bit claim. The Gaussian core would leave this package."
+}

research/storage-spare-bits/VERIFY.json

@@ -0,0 +1,29 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Compare the published magnitudes with the storage budget."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/test_verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Recompute the precision-101 spare independently."
+    }
+  ]
+}

research/storage-spare-bits/test_verify.py

@@ -0,0 +1,21 @@
+"""Recompute the precision-101 storage spare."""
+
+from __future__ import annotations
+
+import unittest
+
+
+class SpareTest(unittest.TestCase):
+    def test_precision_101(self) -> None:
+        precision = 101
+        guard = (precision + 1).bit_length()
+        budget = 8 * precision + 8 * guard + 32
+        prefix_bits = 8 * precision + 18 + (precision * precision).bit_length()
+        self.assertEqual(guard, 7)
+        self.assertEqual(budget, 896)
+        self.assertEqual(prefix_bits, 840)
+        self.assertEqual(budget - prefix_bits, 56)
+
+
+if __name__ == "__main__":
+    unittest.main()

research/storage-spare-bits/verify.py

@@ -0,0 +1,94 @@
+"""Spare bits in the published online storage budget.
+
+G = 8p + 8 ceil(log2(p+2)) + 32. The largest stated magnitude is the
+prefix bound 2^(8p+18) p^2. Its bit length leaves at least 56 bits inside
+G for every precision p >= 101, which covers the claimed twelve spare bits.
+"""
+
+from __future__ import annotations
+
+import json
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+PACKAGE = Path(__file__).resolve().parent
+KAPPA = "836330098538459/500000000000000000"
+LOW = 101
+HIGH = 300
+
+
+def load() -> dict:
+    selected = json.loads(
+        (ROOT / "certificates" / "selected-result.json").read_text(encoding="utf-8")
+    )
+    if selected["kappa"] != KAPPA:
+        raise SystemExit("FAIL_STORAGE_SPARE_BITS selected kappa moved")
+    return json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8"))
+
+
+def ceil_log2(value: int) -> int:
+    return (value - 1).bit_length()
+
+
+def budget(precision: int) -> int:
+    return 8 * precision + 8 * ceil_log2(precision + 2) + 32
+
+
+def magnitudes(precision: int) -> list[int]:
+    square = precision * precision
+    cube = square * precision
+    fourth = square * square
+    return [
+        9 * precision,
+        28 * precision,
+        (1 << 11) * square,
+        (1 << 10) * square,
+        (1 << 12) * square,
+        (1 << 16) * cube,
+        2,
+        1 << (8 * precision + 1),
+        1,
+        (1 << (8 * precision + 18)) * square,
+        (1 << 18) * fourth,
+        (1 << 13) * square,
+        (1 << 17) * cube,
+    ]
+
+
+def main() -> None:
+    pinned = load()
+    # p <= 2^c - 2 < 2^c, so p^2 < 2^(2c) and the prefix spare is at least
+    # 6c + 14. For p >= 101, c >= 7, hence the spare is at least 56.
+    if ceil_log2(101 + 2) != 7 or 6 * 7 + 14 != 56:
+        raise SystemExit("FAIL_STORAGE_SPARE_BITS closed form moved")
+    checks = 0
+    minimum = None
+    for precision in range(LOW, HIGH + 1):
+        guard = ceil_log2(precision + 2)
+        square_bits = (precision * precision).bit_length()
+        if square_bits > 2 * guard:
+            raise SystemExit("FAIL_STORAGE_SPARE_BITS square bits moved")
+        spare = budget(precision) - (8 * precision + 18 + square_bits)
+        if spare < 6 * guard + 14 or spare < 56:
+            raise SystemExit("FAIL_STORAGE_SPARE_BITS spare moved")
+        prefix = (1 << (8 * precision + 18)) * precision * precision
+        if prefix.bit_length() != 8 * precision + 18 + square_bits:
+            raise SystemExit("FAIL_STORAGE_SPARE_BITS prefix bits moved")
+        width = budget(precision)
+        for value in magnitudes(precision):
+            if value.bit_length() > width - 56:
+                raise SystemExit("FAIL_STORAGE_SPARE_BITS magnitude moved")
+            checks += 1
+        if minimum is None or spare < minimum:
+            minimum = spare
+    if (
+        pinned["checks"] != checks
+        or pinned["minimum_spare"] != minimum
+        or pinned["no_new_kappa"] is not True
+    ):
+        raise SystemExit("FAIL_STORAGE_SPARE_BITS pinned result moved")
+    print(f"PASS_STORAGE_SPARE_BITS precisions={HIGH - LOW + 1} no_new_kappa")
+
+
+if __name__ == "__main__":
+    main()