Record the uniform reservoir constant 3 r_max / p (no new κ)

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

@@ -0,0 +1,100 @@
+# Uniform constant for accepted reservoir layouts
+
+**Scoped comparison. No new κ.** The selected conditional exponent stays
+60403/20000000. This does not accept PR #4100.
+
+## Result
+
+The #4174 constructor accepts only integer `p ≥ 1` and
+`ell ≥ max(2, ceil(log2(p+2)))`. For every such `p`,
+
+```text
+ceil(log2(p+2)) ≥ 2,
+```
+
+because `p+2 ≥ 3` and `(3-1).bit_length() = 2`. Thus `ell` and the
+logarithm are each at least 2, and the guard
+
+```text
+G = 64 (ell + ceil(log2(p+2)))
+```
+
+satisfies `G ≥ 256`. The bound is achieved: `p = 1`, `ell = 2`, and
+65,536 widths of 1 give `G = 256`, `L = 65536`, and `r_max = 2`.
+
+PR #4646 factors the sharp window term as
+
+```text
+2/B + β = 2^{-G} (2 + 2^{1−62G} − 2^{2−63G}).
+```
+
+For every integer `G ≥ 256` the exponent `1−62G` is at most `−1`, so the
+positive correction is at most `1/2`. The exact factor is therefore
+strictly less than `5/2`, and in particular strictly less than 3. At
+`r = r_max`,
+
+```text
+r (2/B + β) < 3 r_max 2^{-G} = (3 r_max / p) p 2^{-G}.
+```
+
+So `C = 3 r_max / p` is sufficient for every layout the constructor
+accepts. The same majorant covers the published term `8B/2^K`, whose
+correction `2^{3−62G}` is also at most `1/2` once `G ≥ 256`.
+
+On the equality-case layout the constant is `3 · 2 / 1 = 6`. Both `C = 1`
+and `C = 1/6400` fail there. The constructor rejects `ell = 1`, so the
+weaker floor `G ≥ 192` from an `ell ≥ 1` domain is not a layout this
+constructor emits.
+
+If a layout also has `L ≤ p`, then
+
+```text
+r_max ≤ L/(100G) ≤ p/(100 · 256) = p/25600,
+```
+
+and `3 r_max / p ≤ 3/25600 < 1/6400`. The production plan
+`r_max = 5`, `p = 9240576` satisfies `3 · 5 · 25600 ≤ p`. The constant
+`1/6400` remains sufficient on every accepted layout that also has
+`L ≤ p`.
+
+## Scope
+
+Card `formal-interface-lemma`, scope **refined**. This is the open
+question of the single-layout constant. The argument uses the
+constructor's inequalities and one equality witness. It does not
+enumerate layouts, multiply by the `E` envelope, or rerun the
+104,864-plan census. No multiplication theorem is claimed.
+
+Canonical main fetched 2026-10-22T23:52:56Z at
+`624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3.12 -B research/crt-reservoir-uniform-constant/verify.py
+python3.12 -B scripts/research_package.py --package research/crt-reservoir-uniform-constant
+```
+
+The direct command prints `PASS_CRT_RESERVOIR_UNIFORM_CONSTANT`.
+
+## Open next questions
+
+1. On the equality-case layout `p = 1`, `ell = 2`, `r_max = 2`,
+   `G = 256`, what does `3 r_max 2^{-G}` times the printed `E` envelope
+   become? The scalar comparison is settled, and `p/6400` is not the
+   prefactor when `L > p`. First step: multiply `6 · 2^{-256}` by
+   `2^{4 ell} (p+2)^{16}` and compare with
+   `2^{-60 ell} (p+2)^{-48}`. Blocker: that product is not formed here.
+
+## Credit
+
+Hiroki KUMAZAKI, PR #4174, for the constructor and its guard formula.
+PR #4646 for the factored window term and the constant `1/6400`.
+PR #4921 for the constant 3 on the single layout `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-uniform-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-uniform-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": "Decide whether C = 3 r_max / p is sufficient for r(2/B+beta) <= C p 2^{-G} at r = r_max on every layout the #4174 constructor accepts.",
+  "scope_change_reason": "PR #4921 found the constant 3 only for p=2 and ell=2. Its open question asks whether G >= 256 on every accepted layout, which would make C = 3 r_max / p uniform. The successive sixteenth walks are closed. This package answers that question. It does not rerun the descriptor census and does not claim a new kappa.",
+  "bottleneck_link": "The sharp-density factor 1/6400 needs L <= p. Every accepted layout has G >= 256, so the factored window term is strictly less than 3 and C = 3 r_max / p suffices. When L <= p this C is strictly below 1/6400. The selected frontier is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the guard floor, the majorant, and the equality-case witness. Do not enumerate layouts or multiply by the E envelope.",
+  "outcome": "completed",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/crt-reservoir-uniform-constant",
+  "author": "James Reed",
+  "ai_assistance": "Substantial assistance from Cursor Grok 4.7.",
+  "open_questions": [
+    {
+      "question": "On the equality-case layout p=1, ell=2, r_max=2, G=256, what does 3 r_max 2^{-G} times the printed E envelope become?",
+      "why_it_matters": "The scalar comparison is settled. The repair room still multiplies by E, and p/6400 is not the prefactor when L > p.",
+      "first_step": "Multiply 6 * 2^{-256} by 2^{4 ell} (p+2)^{16} and compare with 2^{-60 ell} (p+2)^{-48}.",
+      "blocked_by": "The E envelope is not multiplied in this package."
+    }
+  ]
+}

research/crt-reservoir-uniform-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": "Every accepted layout has G >= 256 because ell and ceil(log2(p+2)) are at least 2. The factored window term is then strictly less than 3, so C = 3 r_max / p works at r = r_max. The equality witness p=1, ell=2 has G=256 and C=6. Layouts with ell=1 are rejected. Under L <= p the same C is strictly below 1/6400."
+    }
+  ]
+}

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

@@ -0,0 +1,131 @@
+#!/usr/bin/env python3
+"""Uniform constant for every layout the #4174 constructor accepts.
+
+C = 3 r_max / p is enough for the factored window term once G >= 256.
+The constructor forces that floor. No layout census is run, 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-uniform-constant"
+ALLOCATOR = ROOT / "research/crt-reservoir-placement/allocator.py"
+
+ABSORPTION = "r (2/B + β) < r (2 + 2^{1−62G}) 2^{−G} ≤ p 2^{−G} / 6400."
+GUARD_LINE = "guard_digit_bits = 64 * (ell + logarithm)"
+
+
+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")
+    allocator = ALLOCATOR.read_text(encoding="utf-8")
+    need(ABSORPTION in proof, "printed 1/6400 absorption")
+    need(GUARD_LINE in allocator, "constructor guard formula")
+    need('ell >= logarithm' in allocator, "constructor logarithm floor")
+    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 logarithm_floor(allocator) -> None:
+    """Every integer p >= 1 has ceil(log2(p+2)) >= 2."""
+    need((1).bit_length() == 1 and (2).bit_length() == 2, "bit length of 1 and 2")
+    # If m >= 4 and m//2 <= 1, then m = 2*(m//2) + (m%2) <= 3.
+    need(2 * 1 + 1 < 4, "no integer m >= 4 has m//2 <= 1")
+    need(allocator.ceil_log2(3) == 2, "ceil(log2(3)) is 2")
+    # p >= 1 ⇒ p+2 >= 3 ⇒ (p+1) >= 2. Descent reaches 2 or 3, both of bit length 2.
+    need((3).bit_length() == 2, "bit length of 3")
+
+
+def guard_floor() -> None:
+    """ell >= log >= 2, so G = 64*(ell+log) >= 256."""
+    log_min = 2
+    ell_min = log_min
+    need(64 * (ell_min + log_min) == 256, "minimum guard is 256")
+    need(62 * 256 >= 2, "62G is at least 2 at the floor")
+    # Exponent 1-62G <= -1, and 3-62G <= -1, so each tiny term is at most 1/2.
+    need(1 - 62 * 256 <= -1 and 3 - 62 * 256 <= -1, "both window corrections are at most 1/2")
+
+
+def sharp_unit(guard: int) -> int:
+    return (1 << (1 + 63 * guard)) + (1 << (1 + guard)) - 4
+
+
+def published_unit(guard: int) -> int:
+    return (1 << (1 + 63 * guard)) + (1 << (3 + guard))
+
+
+def fits(numerator: int, constant_num: int, constant_den: int, modulus: int, scale: int) -> bool:
+    return numerator * constant_den <= constant_num * modulus * scale
+
+
+def equality_witness(allocator) -> None:
+    layout = allocator.Layout(1, 2, (1,) * 65536)
+    need(layout.G == 256 and layout.r_max == 2 and layout.p == 1, "equality-case parameters")
+    need(layout.L == 65536 and layout.L > layout.p, "equality-case address is longer than p")
+    scale = 1 << (63 * layout.G)
+    sharp = layout.r_max * sharp_unit(layout.G)
+    published = layout.r_max * published_unit(layout.G)
+    # C = 3 r_max / p = 6.
+    need(3 * layout.r_max == 6 * layout.p, "equality-case constant is 6")
+    need(fits(sharp, 6, 1, layout.p, scale), "C=6 holds on the sharp term")
+    need(fits(published, 6, 1, layout.p, scale), "C=6 holds on the published term")
+    need(not fits(sharp, 1, 1, layout.p, scale), "C=1 fails on the equality case")
+    need(not fits(sharp, 1, 6400, layout.p, scale), "1/6400 fails on the equality case")
+
+
+def old_constant_survives_when_address_is_short() -> None:
+    """L <= p and G >= 256 give 3 r_max / p <= 3/25600 < 1/6400."""
+    need(3 * 6400 < 25600, "3/25600 is strictly below 1/6400")
+    need(3 * 5 * 25600 <= 9240576, "production plan still fits the tighter majorant")
+
+
+def rejected(allocator) -> None:
+    try:
+        allocator.Layout(1, 1, (1,) * 65536)
+    except ValueError:
+        return
+    raise SystemExit("FAIL: ell=1 was accepted")
+
+
+def main() -> None:
+    pins_and_phrases()
+    allocator = load_allocator()
+    logarithm_floor(allocator)
+    guard_floor()
+    equality_witness(allocator)
+    old_constant_survives_when_address_is_short()
+    rejected(allocator)
+    print(
+        "PASS_CRT_RESERVOIR_UNIFORM_CONSTANT "
+        "G_min=256 equality_p=1 equality_r=2 integer_factor=3"
+    )
+
+
+if __name__ == "__main__":
+    main()