From 8d7b7ac0b64db68318d7437256309406fef9e0c8 Mon Sep 17 00:00:00 2001 From: James Reed Date: Thu, 22 Oct 2026 16:53:10 -0700 Subject: [PATCH] Record the uniform reservoir constant 3 r_max / p Every layout the #4174 constructor accepts has G >= 256, so the factored window term is strictly less than 3. Then C = 3 r_max / p suffices at r = r_max. No new kappa. Co-authored-by: Cursor --- .../crt-reservoir-uniform-constant/README.md | 100 +++++++++++++ .../SOURCES.json | 30 ++++ .../crt-reservoir-uniform-constant/TASK.json | 95 +++++++++++++ .../VERIFY.json | 21 +++ .../crt-reservoir-uniform-constant/verify.py | 131 ++++++++++++++++++ 5 files changed, 377 insertions(+) create mode 100644 research/crt-reservoir-uniform-constant/README.md create mode 100644 research/crt-reservoir-uniform-constant/SOURCES.json create mode 100644 research/crt-reservoir-uniform-constant/TASK.json create mode 100644 research/crt-reservoir-uniform-constant/VERIFY.json create mode 100644 research/crt-reservoir-uniform-constant/verify.py diff --git a/research/crt-reservoir-uniform-constant/README.md b/research/crt-reservoir-uniform-constant/README.md new file mode 100644 index 0000000000..275a4c26ea --- /dev/null +++ b/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. diff --git a/research/crt-reservoir-uniform-constant/SOURCES.json b/research/crt-reservoir-uniform-constant/SOURCES.json new file mode 100644 index 0000000000..239d6caf16 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/crt-reservoir-uniform-constant/TASK.json b/research/crt-reservoir-uniform-constant/TASK.json new file mode 100644 index 0000000000..7989e88dbd --- /dev/null +++ b/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." + } + ] +} diff --git a/research/crt-reservoir-uniform-constant/VERIFY.json b/research/crt-reservoir-uniform-constant/VERIFY.json new file mode 100644 index 0000000000..31a43a2996 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/crt-reservoir-uniform-constant/verify.py b/research/crt-reservoir-uniform-constant/verify.py new file mode 100644 index 0000000000..9b823b817f --- /dev/null +++ b/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()