From 021864cf72ef43ed82f98bd3b711948f6b4c8a95 Mon Sep 17 00:00:00 2001 From: James Reed Date: Thu, 22 Oct 2026 17:14:31 -0700 Subject: [PATCH] Record the edge ratio against p/6400 On p=2^{24}-2, ell=24, r_max=4 the envelope ratio is 12, and 12*6400=76800 is strictly below 16777214. The quotient is 218 with remainder 34814. No new kappa. Co-authored-by: Cursor --- .../crt-reservoir-edge-allowance/README.md | 85 ++++++++++++++++++ .../crt-reservoir-edge-allowance/SOURCES.json | 30 +++++++ .../crt-reservoir-edge-allowance/TASK.json | 89 +++++++++++++++++++ .../crt-reservoir-edge-allowance/VERIFY.json | 21 +++++ .../crt-reservoir-edge-allowance/verify.py | 76 ++++++++++++++++ 5 files changed, 301 insertions(+) create mode 100644 research/crt-reservoir-edge-allowance/README.md create mode 100644 research/crt-reservoir-edge-allowance/SOURCES.json create mode 100644 research/crt-reservoir-edge-allowance/TASK.json create mode 100644 research/crt-reservoir-edge-allowance/VERIFY.json create mode 100644 research/crt-reservoir-edge-allowance/verify.py diff --git a/research/crt-reservoir-edge-allowance/README.md b/research/crt-reservoir-edge-allowance/README.md new file mode 100644 index 0000000000..70d8785b44 --- /dev/null +++ b/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. diff --git a/research/crt-reservoir-edge-allowance/SOURCES.json b/research/crt-reservoir-edge-allowance/SOURCES.json new file mode 100644 index 0000000000..239d6caf16 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/crt-reservoir-edge-allowance/TASK.json b/research/crt-reservoir-edge-allowance/TASK.json new file mode 100644 index 0000000000..45fa78e46b --- /dev/null +++ b/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." +} diff --git a/research/crt-reservoir-edge-allowance/VERIFY.json b/research/crt-reservoir-edge-allowance/VERIFY.json new file mode 100644 index 0000000000..94dc80756a --- /dev/null +++ b/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." + } + ] +} diff --git a/research/crt-reservoir-edge-allowance/verify.py b/research/crt-reservoir-edge-allowance/verify.py new file mode 100644 index 0000000000..c95ddfb507 --- /dev/null +++ b/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()