Record the production envelope ratio against 1/6400 (no new κ)

research/crt-reservoir-production-ratio/README.md

@@ -0,0 +1,84 @@
+# Production envelope ratio
+
+**Scoped comparison. No new κ.** The selected conditional exponent stays
+60403/20000000. This does not accept PR #4100.
+
+## Result
+
+The ratio carried into the printed room is
+
+```text
+R = 3 r_max ((p+2) / 2^{ceil(log2(p+2))})^{64}.
+```
+
+On the #4174 production plan, `p = 9240576`, `ell = 24`, `L = 1540096`,
+`G = 3072`, and `r_max = 5`. Then `ceil(log2(9240578)) = 24`, because
+`2^{23} < 9240578 < 2^{24}`. The ratio is
+
+```text
+R = 15 (9240578 / 2^{24})^{64}.
+```
+
+The numerator `15 · 9240578^{64}` has bit length 1485, and the
+denominator is `2^{1536}`, so
+
+```text
+2^{-52} ≤ R < 2^{-51}.
+```
+
+In particular `R < 1/6400`. The integer quotient of `1/6400` by `R` is
+393602022308, with a positive remainder, so
+
+```text
+393602022308 < (1/6400) / R < 393602022309.
+```
+
+The bare room is larger still: its quotient by `R` is
+2519052942774845, again with a positive remainder. `C_E` multiplies both
+sides and is not evaluated. The 104,864-plan schedule is not replayed.
+
+`L ≤ p` does not force this. The constructor accepts `p = 2^{24} - 2`,
+`ell = 24`, and 65,536 widths of 23. There `L = 1507328 ≤ p`,
+`G = 3072`, `r_max = 4`, and `p+2` is a power of two, so `R = 12`. That
+exceeds both `1/6400` and the bare room. The production bound uses the
+gap between 9240578 and `2^{24}`.
+
+## Scope
+
+Card `formal-interface-lemma`, scope **refined**. This is the open
+question of the equality-case envelope product. Two layouts are
+checked. No census, no real `E` polynomial, and no multiplication
+theorem are claimed.
+
+Canonical main fetched 2026-10-23T00:04:29Z at
+`624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3.12 -B research/crt-reservoir-production-ratio/verify.py
+python3.12 -B scripts/research_package.py --package research/crt-reservoir-production-ratio
+```
+
+The direct command prints `PASS_CRT_RESERVOIR_PRODUCTION_RATIO`.
+
+## Open next questions
+
+1. On the edge layout `p = 2^{24} - 2`, `ell = 24`, `r_max = 4`, the
+   envelope ratio equals 12. Is 12 still at most `p/6400`, the
+   coefficient in the printed room line? The ratio exceeds `1/6400`
+   and the bare room, while `L ≤ p`. First step: compare `12 · 6400`
+   with `16777214`. Blocker: that comparison is not made here.
+
+## Credit
+
+Hiroki KUMAZAKI, PR #4174, for the production layout and the constructor.
+PR #4646 for the printed envelope. PR #4924 for the ratio on the
+equality case and on `p = 2`. Cinna Davis, PR #4100, for the CRT
+parameters.
+
+Prepared by James Reed with substantial Cursor Grok 4.7 assistance.
+Apache-2.0. No independent human review and no formal-kernel acceptance
+are claimed.

research/crt-reservoir-production-ratio/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/compact-switch-sharp-density/PROOF.md",
+      "usage": "input",
+      "git_blob": "f7132bb89ba2dc1153175d400c5baef38a894f3f",
+      "sha256": "7ef2e48db773013ab4978a1594116c1235110c148081656b6b2c6927b5db6e3f"
+    },
+    {
+      "path": "research/crt-reservoir-placement/allocator.py",
+      "usage": "input",
+      "git_blob": "4b3ad89652a28f7d142248d1b5747272e696493c",
+      "sha256": "b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688"
+    }
+  ]
+}

research/crt-reservoir-production-ratio/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.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": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "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",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "On the production plan p=9240576, ell=24, r_max=5, decide whether 15 ((p+2)/2^{ceil(log2(p+2))})^{64} is at most 1/6400.",
+  "scope_change_reason": "PR #4924 evaluated this ratio on the equality case and on p=2, and left the production plan open. The successive sixteenth walks are closed. This package evaluates that plan. It does not rerun the descriptor census and does not claim a new kappa.",
+  "bottleneck_link": "The repair room multiplies by the envelope. On the production plan the ratio is strictly below 1/6400 and lies in [2^{-52}, 2^{-51}). An L <= p layout with no envelope slack has ratio 12. The selected frontier is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the production ratio and the one power-of-two edge layout. Do not enumerate plans or search for the maximum ratio.",
+  "outcome": "completed",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/crt-reservoir-production-ratio",
+  "author": "James Reed",
+  "ai_assistance": "Substantial assistance from Cursor Grok 4.7.",
+  "open_questions": [
+    {
+      "question": "On the edge layout p=2^{24}-2, ell=24, r_max=4, the envelope ratio equals 12. Is 12 still at most p/6400, the coefficient in the printed room line?",
+      "why_it_matters": "The ratio exceeds 1/6400 and the bare room, while L <= p. The printed line uses p/6400 rather than 1/6400.",
+      "first_step": "Compare 12 * 6400 with 16777214.",
+      "blocked_by": "That comparison is not made here."
+    }
+  ]
+}

research/crt-reservoir-production-ratio/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/compact-switch-sharp-density/PROOF.md",
+    "research/crt-reservoir-placement/allocator.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "ceil(log2(9240578))=24. The production ratio 15 (9240578/2^{24})^{64} lies in [2^{-52}, 2^{-51}) and is strictly below 1/6400. The allowance is between 393602022308 and 393602022309 times the ratio. The edge layout p=2^{24}-2, ell=24, r_max=4 has L <= p and ratio exactly 12."
+    }
+  ]
+}

research/crt-reservoir-production-ratio/verify.py

@@ -0,0 +1,97 @@
+#!/usr/bin/env python3
+"""Production-plan envelope ratio against 1/6400.
+
+The plan is the #4174 census layout. The comparison is one integer.
+No schedule is replayed, and no new kappa is claimed.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import importlib.util
+import json
+import sys
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+PACKAGE = ROOT / "research" / "crt-reservoir-production-ratio"
+ALLOCATOR = ROOT / "research/crt-reservoir-placement/allocator.py"
+
+ENVELOPE = "E(p, ell) ≤ C_E 2^{4 ell} (p+2)^{16}"
+ROOM = "≤ 2^{−60 ell} (p+2)^{−48}"
+
+
+def need(condition: bool, message: str) -> None:
+    if not condition:
+        raise SystemExit("FAIL: " + message)
+
+
+def pins_and_phrases() -> None:
+    sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8"))
+    for row in sources["files"]:
+        if row["usage"] == "input":
+            digest = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest()
+            need(digest == row["sha256"], row["path"])
+    proof = (ROOT / "research/compact-switch-sharp-density/PROOF.md").read_text(encoding="utf-8")
+    need(ENVELOPE in proof, "printed E envelope")
+    need(ROOM in proof, "printed room line")
+    selected = json.loads(
+        (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")
+    )
+    need(selected["kappa"] == "60403/20000000", "selected kappa")
+
+
+def load_allocator():
+    spec = importlib.util.spec_from_file_location("crt_reservoir_allocator", ALLOCATOR)
+    module = importlib.util.module_from_spec(spec)
+    sys.modules[spec.name] = module
+    spec.loader.exec_module(module)
+    return module
+
+
+def production(allocator) -> None:
+    widths = tuple(24 - (i % 2) for i in range(65536))
+    length = sum(widths)
+    layout = allocator.Layout(6 * length, 24, widths)
+    need(layout.p == 9240576 and layout.L == 1540096 and layout.ell == 24, "production parameters")
+    need(layout.G == 3072 and layout.r_max == 5 and layout.L <= layout.p, "production guard")
+    logarithm = (layout.p + 1).bit_length()
+    need(logarithm == 24, "ceil(log2(9240578)) is 24")
+    need((1 << 23) < layout.p + 2 < (1 << 24), "p+2 lies strictly between 2^23 and 2^24")
+    need(layout.G == 64 * (layout.ell + logarithm), "guard formula")
+    base = layout.p + 2
+    power = base ** 64
+    denominator = 1 << (64 * logarithm)
+    numerator = 15 * power
+    need((1 << 1484) <= numerator < (1 << 1485), "ratio lies in [2^{-52}, 2^{-51})")
+    need(numerator * 6400 < denominator, "ratio is strictly below 1/6400")
+    allowance, remainder = divmod(denominator, numerator * 6400)
+    need(allowance == 393602022308 and remainder > 0, "allowance over the ratio")
+    room, room_remainder = divmod(denominator, numerator)
+    need(room == 2519052942774845 and room_remainder > 0, "bare room over the ratio")
+
+
+def power_edge(allocator) -> None:
+    """Same ell, L <= p, and p+2 a power of two. The ratio keeps the factor 3 r_max."""
+    modulus = (1 << 24) - 2
+    layout = allocator.Layout(modulus, 24, (23,) * 65536)
+    need(layout.p == 16777214 and layout.ell == 24 and layout.G == 3072, "edge parameters")
+    need(layout.r_max == 4 and layout.L == 1507328 and layout.L <= layout.p, "edge length")
+    need(layout.p + 2 == 1 << 24, "no envelope slack")
+    need(3 * layout.r_max == 12, "edge ratio equals 12")
+    need(12 * 6400 > 1, "edge ratio exceeds 1/6400")
+
+
+def main() -> None:
+    pins_and_phrases()
+    allocator = load_allocator()
+    production(allocator)
+    power_edge(allocator)
+    print(
+        "PASS_CRT_RESERVOIR_PRODUCTION_RATIO "
+        "log=24 ratio_bits=52 below_6400=1 edge_ratio=12"
+    )
+
+
+if __name__ == "__main__":
+    main()