Record the constant 3 on the longer reservoir layout (no new κ)

research/crt-reservoir-length-constant/README.md

@@ -0,0 +1,72 @@
+# Constant on the longer reservoir layout
+
+**Scoped comparison. No new κ.** The selected conditional exponent stays
+60403/20000000. This does not accept PR #4100.
+
+## Result
+
+PR #4646 proves, when `L ≤ p` and `r ≤ floor(L/(100G))`,
+
+```text
+r (2/B + β) < r (2 + 2^{1−62G}) 2^{−G} ≤ p 2^{−G} / 6400.
+```
+
+PR #4913's admitted layout `p = 2`, `ell = 2`, and 65,536 widths of 1 has
+`L = 65536 > p`, `G = 256`, and `r_max = 2`. At `r = r_max` the factor
+`1/6400` does not survive. The exact sharp ratio is
+
+```text
+C_* = 2 + 2^{-15871} - 2^{-16126}.
+```
+
+It is the number `C` in `r (2/B + β) = C p 2^{-G}`. It lies strictly
+between 2 and 3, so `C = 2` fails and `C = 3` holds. Thus 3 is the
+smallest integer constant that replaces `1/6400` for this one inequality.
+
+The published window term has exact ratio `2 + 2^{-15869}`. It has the
+same integer threshold: `1/6400` and `2` fail, and `3` holds.
+
+The production plan `L = 1540096`, `p = 9240576`, `r_max = 5` still
+satisfies `5 · 3 · 6400 ≤ p`. This package does not replace `1/6400`
+there. The `< 3` majorant is the one PR #4646 uses to reach `1/6400`.
+
+## Scope
+
+Card `formal-interface-lemma`, scope **refined**. This is the open
+question of the production address-length comparison. The check is one
+layout at `r = r_max`. It does not give a constant for every layout with
+`L > p`, and it does not rerun the 104,864-plan census. No repair
+tariff, `E` multiplication, or multiplication theorem is claimed.
+
+Canonical main fetched 2026-10-22T23:47:42Z at
+`624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3.12 -B research/crt-reservoir-length-constant/verify.py
+python3.12 -B scripts/research_package.py --package research/crt-reservoir-length-constant
+```
+
+The direct command prints `PASS_CRT_RESERVOIR_LENGTH_CONSTANT`.
+
+## Open next questions
+
+1. For every layout the #4174 constructor accepts, is
+   `C = 3 r_max / p` sufficient for
+   `r (2/B + β) ≤ C p 2^{-G}` at `r = r_max`? The constant 3 is proved
+   here only for `p = 2` and `ell = 2`. First step: show that every
+   accepted layout has `G ≥ 256`, so `2 + 2^{1−62G} < 3`. Blocker: this
+   package checks only the one longer layout.
+
+## Credit
+
+Hiroki KUMAZAKI, PR #4174, for the constructor that admits this layout.
+PR #4646 for the `1/6400` absorption. PR #4328 for the `L ≤ p` hypothesis
+that absorption uses. 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-length-constant/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-length-constant/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": "Evaluate r(2/B+beta) against C p 2^{-G} at r=r_max on the one admitted layout p=2, ell=2, L=65536, and name the constant that replaces 1/6400 there.",
+  "scope_change_reason": "PR #4913 showed that this layout has L > p, so the production factor 1/6400 does not transfer. The successive sixteenth walks are closed. This package evaluates that one inequality. It does not retune the production plan, does not rerun the descriptor census, and does not claim a new kappa.",
+  "bottleneck_link": "The sharp-density line uses C=1/6400 only under L <= p. On this layout the exact ratio is strictly between 2 and 3, so the smallest integer constant is 3. The selected frontier is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after this one layout at r=r_max, for the sharp window and the published window term. Do not scan other layouts or replay the 104864-plan census.",
+  "outcome": "completed",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/crt-reservoir-length-constant",
+  "author": "James Reed",
+  "ai_assistance": "Substantial assistance from Cursor Grok 4.7.",
+  "open_questions": [
+    {
+      "question": "For every layout the #4174 constructor accepts, is C = 3 r_max / p sufficient for r(2/B+beta) <= C p 2^{-G} at r = r_max?",
+      "why_it_matters": "The constant 3 is proved here only for p=2 and ell=2. A uniform factor would say when 1/6400 still applies and when it must grow.",
+      "first_step": "Show that every accepted layout has G >= 256, so 2 + 2^{1-62G} < 3.",
+      "blocked_by": "This package checks only the one longer layout."
+    }
+  ]
+}

research/crt-reservoir-length-constant/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, ell=2, L=65536, r=2, G=256 the exact sharp ratio is 2 + 2^{-15871} - 2^{-16126}. It is strictly between 2 and 3, so C=3 works and C=2 and C=1/6400 fail. The published window term has the same integer threshold. The production majorant still fits 1/6400."
+    }
+  ]
+}

research/crt-reservoir-length-constant/verify.py

@@ -0,0 +1,108 @@
+#!/usr/bin/env python3
+"""Replace 1/6400 on the one #4174 layout with L > p.
+
+The comparison is r (2/B + beta) <= C p 2^{-G} at r = r_max. The layout
+is p=2, ell=2, and 65536 widths of 1. No other layout is scanned, 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-length-constant"
+ALLOCATOR = ROOT / "research/crt-reservoir-placement/allocator.py"
+
+# The minus signs in the exponent are U+2212, as printed in PROOF.md.
+ABSORPTION = "r (2/B + β) < r (2 + 2^{1−62G}) 2^{−G} ≤ p 2^{−G} / 6400."
+
+
+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(ABSORPTION in proof, "printed 1/6400 absorption")
+    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 sharp_unit(guard: int) -> int:
+    """(2/B + beta) * 2^{G + 63G}, with B = 2^G and beta = 2(B-2)/2^{64G}."""
+    return (1 << (1 + 63 * guard)) + (1 << (1 + guard)) - 4
+
+
+def published_unit(guard: int) -> int:
+    """(2/B + 8B/2^K) * 2^{G + 63G}."""
+    return (1 << (1 + 63 * guard)) + (1 << (3 + guard))
+
+
+def fits(numerator: int, constant_num: int, constant_den: int, modulus: int, scale: int) -> bool:
+    """numerator / scale <= (constant_num / constant_den) * modulus."""
+    return numerator * constant_den <= constant_num * modulus * scale
+
+
+def one_layout(allocator) -> None:
+    layout = allocator.Layout(2, 2, (1,) * 65536)
+    need(layout.p == 2 and layout.ell == 2 and layout.L == 65536, "longer layout")
+    need(layout.G == 256 and layout.r_max == 2, "longer guard and batch")
+    need(layout.L > layout.p, "address longer than p")
+    guard = layout.G
+    batch = layout.r_max
+    modulus = layout.p
+    scale = 1 << (63 * guard)
+    sharp = batch * sharp_unit(guard)
+    published = batch * published_unit(guard)
+    # Exact sharp ratio C_* = sharp / (p * 2^{63G}) = 2 + 2^{-15871} - 2^{-16126}.
+    need(sharp == (1 << 16130) + (1 << 258) - 8, "exact sharp numerator")
+    need(2 * modulus * scale < sharp < 3 * modulus * scale, "sharp ratio is strictly between 2 and 3")
+    need(not fits(sharp, 1, 6400, modulus, scale), "1/6400 fails on the sharp term")
+    need(not fits(sharp, 2, 1, modulus, scale), "integer 2 fails on the sharp term")
+    need(fits(sharp, 3, 1, modulus, scale), "integer 3 holds on the sharp term")
+    # Published window ratio C = published / (p * 2^{63G}) = 2 + 2^{-15869}.
+    need(published == (1 << 16130) + (1 << 260), "exact published numerator")
+    need(2 * modulus * scale < published < 3 * modulus * scale, "published ratio is strictly between 2 and 3")
+    need(not fits(published, 1, 6400, modulus, scale), "1/6400 fails on the published term")
+    need(not fits(published, 2, 1, modulus, scale), "integer 2 fails on the published term")
+    need(fits(published, 3, 1, modulus, scale), "integer 3 holds on the published term")
+
+
+def production_majorant() -> None:
+    """The recorded production plan still fits the old constant under factor < 3."""
+    need(5 * 3 * 6400 <= 9240576, "production majorant still fits 1/6400")
+
+
+def main() -> None:
+    pins_and_phrases()
+    one_layout(load_allocator())
+    production_majorant()
+    print(
+        "PASS_CRT_RESERVOIR_LENGTH_CONSTANT "
+        "layout_p=2 layout_L=65536 r=2 G=256 sharp_between=2,3 integer_C=3"
+    )
+
+
+if __name__ == "__main__":
+    main()