Record the edge ratio against p/6400 (no new κ)

research/crt-reservoir-edge-allowance/README.md

@@ -0,0 +1,85 @@
+# Edge allowance against p/6400
+
+**Scoped comparison. No new κ.** The selected conditional exponent stays
+60403/20000000. This does not accept PR #4100.
+
+## Result
+
+On the edge layout `p = 2^{24} - 2 = 16777214`, `ell = 24`, and 65,536
+widths of 23, the constructor gives `L = 1507328 ≤ p`, `G = 3072`, and
+`r_max = 4`. Here `p + 2 = 2^{24}`, so the envelope ratio is exactly
+
+```text
+R = 3 r_max = 12.
+```
+
+The printed product line uses the coefficient `p/6400`, with `C_E` left
+as a common factor:
+
+```text
+r (2/B + β) E ≤ (C_E p / 6400) 2^{−60 ell} (p+2)^{−48}.
+```
+
+The comparison asked by PR #4925 is `12 · 6400` against `p`:
+
+```text
+12 · 6400 = 76800 < 16777214 = p.
+```
+
+So `12 < p/6400`. Division gives
+
+```text
+p = 218 · 76800 + 34814,
+```
+
+and therefore
+
+```text
+218 < (p/6400) / 12 < 219.
+```
+
+The additive gap is
+
+```text
+p/6400 − 12 = 2609 + 2814/6400.
+```
+
+`C_E` is not evaluated. No larger ratio is sought, and the 104,864-plan
+schedule is not replayed.
+
+## Scope
+
+Card `formal-interface-lemma`, scope **refined**. This is the open
+question of the production envelope ratio. One layout and one division
+are checked. No census and no multiplication theorem are claimed.
+
+Canonical main fetched 2026-10-23T00:13:18Z at
+`624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3.12 -B research/crt-reservoir-edge-allowance/verify.py
+python3.12 -B scripts/research_package.py --package research/crt-reservoir-edge-allowance
+```
+
+The direct command prints `PASS_CRT_RESERVOIR_EDGE_ALLOWANCE`.
+
+## Open next questions
+
+None of the same kind. PR #4925 asked whether 12 is at most `p/6400` on
+this edge. The comparison holds, and the quotient above is the result.
+`C_E` remains the unevaluated common factor already excluded from that
+question. Searching for a larger ratio was excluded by the predecessor.
+
+## Credit
+
+Hiroki KUMAZAKI, PR #4174, for the constructor. PR #4646 for the printed
+product line. PR #4925 for the edge layout and the ratio 12. 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-edge-allowance/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-edge-allowance/TASK.json

@@ -0,0 +1,89 @@
+{
+  "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 edge layout p=2^{24}-2, ell=24, r_max=4, decide whether the envelope ratio 12 is at most p/6400.",
+  "scope_change_reason": "PR #4925 left this comparison open after showing the edge ratio equals 12. The successive sixteenth walks are closed. This package compares 12*6400 with 16777214. It does not search for a larger ratio and does not claim a new kappa.",
+  "bottleneck_link": "The printed product uses the coefficient p/6400. On this edge the ratio is 12, and 12*6400 is strictly below p, so the ratio lies strictly below that coefficient. The selected frontier is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the integer comparison of 12*6400 with p on this one edge layout. Do not evaluate C_E and do not search for the maximum ratio.",
+  "outcome": "completed",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/crt-reservoir-edge-allowance",
+  "author": "James Reed",
+  "ai_assistance": "Substantial assistance from Cursor Grok 4.7.",
+  "open_questions": [],
+  "no_open_questions_reason": "PR #4925 asked only whether 12 is at most p/6400 on this edge. The comparison holds, and the exact quotient is part of the result. C_E remains the unevaluated common factor already excluded from that question. Searching for a larger ratio was excluded by the predecessor. No further comparison of this edge ratio is posed."
+}

research/crt-reservoir-edge-allowance/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": "On p=2^{24}-2, ell=24, r_max=4, the ratio is 12. Then 12*6400=76800 is strictly below 16777214, the quotient is 218 with remainder 34814, and p/6400-12 = 2609 + 2814/6400."
+    }
+  ]
+}

research/crt-reservoir-edge-allowance/verify.py

@@ -0,0 +1,76 @@
+#!/usr/bin/env python3
+"""Edge ratio 12 against the printed coefficient p/6400.
+
+The layout is the power-of-two edge from the production-ratio package.
+The comparison is one integer division. 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-edge-allowance"
+ALLOCATOR = ROOT / "research/crt-reservoir-placement/allocator.py"
+
+PRODUCT = "r (2/B + β) E ≤ (C_E p / 6400) 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(PRODUCT in proof, "printed product 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 edge(allocator) -> None:
+    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")
+    threshold = 12 * 6400
+    need(threshold == 76800 and threshold < layout.p, "12 * 6400 is strictly below p")
+    quotient, remainder = divmod(layout.p, threshold)
+    need(quotient == 218 and remainder == 34814, "p / (12 * 6400) lies in (218, 219)")
+    gap, gap_remainder = divmod(layout.p - threshold, 6400)
+    need(gap == 2609 and gap_remainder == 2814, "p/6400 - 12 = 2609 + 2814/6400")
+
+
+def main() -> None:
+    pins_and_phrases()
+    edge(load_allocator())
+    print(
+        "PASS_CRT_RESERVOIR_EDGE_ALLOWANCE "
+        "threshold=76800 quotient=218 remainder=34814"
+    )
+
+
+if __name__ == "__main__":
+    main()