From e37a6fc6c947e3555d8f090d50e7d62928080b26 Mon Sep 17 00:00:00 2001 From: James Reed Date: Thu, 22 Oct 2026 17:00:38 -0700 Subject: [PATCH] Record the equality-case envelope product On p=1, ell=2 and G=256, 6 * 2^{-256} times the printed envelope is 3^{17}/2^{247}, which is 3^{65}/2^{127} of the room line. The p=2 layout exceeds the room by 6. No new kappa. Co-authored-by: Cursor --- .../crt-reservoir-envelope-product/README.md | 89 +++++++++++++++ .../SOURCES.json | 30 +++++ .../crt-reservoir-envelope-product/TASK.json | 95 ++++++++++++++++ .../VERIFY.json | 21 ++++ .../crt-reservoir-envelope-product/verify.py | 104 ++++++++++++++++++ 5 files changed, 339 insertions(+) create mode 100644 research/crt-reservoir-envelope-product/README.md create mode 100644 research/crt-reservoir-envelope-product/SOURCES.json create mode 100644 research/crt-reservoir-envelope-product/TASK.json create mode 100644 research/crt-reservoir-envelope-product/VERIFY.json create mode 100644 research/crt-reservoir-envelope-product/verify.py diff --git a/research/crt-reservoir-envelope-product/README.md b/research/crt-reservoir-envelope-product/README.md new file mode 100644 index 0000000000..1ddc02e035 --- /dev/null +++ b/research/crt-reservoir-envelope-product/README.md @@ -0,0 +1,89 @@ +# Envelope product on the equality-case layout + +**Scoped comparison. No new κ.** The selected conditional exponent stays +60403/20000000. This does not accept PR #4100. + +## Result + +PR #4646 uses the printed envelope + +```text +E(p, ell) ≤ C_E 2^{4 ell} (p+2)^{16} +``` + +and the room line + +```text +2^{-G} 2^{4 ell} (p+2)^{16} ≤ 2^{-60 ell} (p+2)^{-48}. +``` + +On the equality-case layout `p = 1`, `ell = 2`, `G = 256`, `r_max = 2`, +the scalar prefactor from PR #4923 is `3 r_max = 6`. The product asked +for is + +```text +6 · 2^{-256} · 2^{8} · 3^{16} = 3^{17} / 2^{247}. +``` + +The room line at these parameters is `1 / (2^{120} · 3^{48})`. Their +ratio is + +```text +3^{65} / 2^{127}. +``` + +Since `2^{103} ≤ 3^{65} < 2^{104}`, this ratio lies in +`[2^{-24}, 2^{-23})`. It is strictly less than 1, so the product is +strictly below the room line. It is also strictly less than `1/6400`: +`6400 · 3^{65} < 2^{127}`, and `2^{127} / (6400 · 3^{65})` has integer +quotient 2580. Because `p = 1`, that is the same comparison as the older +allowance `(C_E p / 6400)` times the room. The scalar step with +`C = 1/6400` still fails on this layout. The slack in the envelope, +`(3/4)^{64}`, is what brings the product back under that allowance. +`C_E` multiplies both sides and is not evaluated. + +The same ratio on the admitted layout `p = 2`, `ell = 2`, `r_max = 2` +is exactly 6, because `p+2 = 4` is a power of two and the envelope has +no slack. There the product exceeds the room line. The equality-case +bound does not extend to every accepted layout. + +## Scope + +Card `formal-interface-lemma`, scope **refined**. This is the open +question of the uniform constant. The check is two layouts and exact +integer arithmetic. It does not evaluate the production plan, form the +real `E` polynomial, or rerun the 104,864-plan census. No multiplication +theorem is claimed. + +Canonical main fetched 2026-10-23T00:00:26Z at +`624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B research/crt-reservoir-envelope-product/verify.py +python3.12 -B scripts/research_package.py --package research/crt-reservoir-envelope-product +``` + +The direct command prints `PASS_CRT_RESERVOIR_ENVELOPE_PRODUCT`. + +## Open next questions + +1. On the production plan `p = 9240576`, `ell = 24`, `r_max = 5`, is + `3 r_max ((p+2) / 2^{ceil(log2(p+2))})^{64}` at most `1/6400`? The + equality case is below that allowance, and the layout `p = 2` is + above the room itself. First step: compute `ceil(log2(9240578))` and + compare `15 (p+2)^{64}` with `2^{64 ceil(log2(p+2))} / 6400`. + Blocker: the production plan is not evaluated here. + +## Credit + +Hiroki KUMAZAKI, PR #4174, for the constructor that admits both layouts. +PR #4646 for the printed envelope and room line. PR #4923 for the +prefactor `3 r_max`. 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-envelope-product/SOURCES.json b/research/crt-reservoir-envelope-product/SOURCES.json new file mode 100644 index 0000000000..239d6caf16 --- /dev/null +++ b/research/crt-reservoir-envelope-product/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-envelope-product/TASK.json b/research/crt-reservoir-envelope-product/TASK.json new file mode 100644 index 0000000000..d3fbc0bca6 --- /dev/null +++ b/research/crt-reservoir-envelope-product/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": "Multiply 6 * 2^{-256} by the printed E envelope 2^{4 ell} (p+2)^{16} on the equality-case layout p=1, ell=2, and compare the product with 2^{-60 ell} (p+2)^{-48}.", + "scope_change_reason": "PR #4923 settled the scalar constant and left this one product open. The successive sixteenth walks are closed. This package evaluates that product. It does not rerun the descriptor census and does not claim a new kappa.", + "bottleneck_link": "The repair room multiplies the scalar bound by E. On this layout the product is 3^{65}/2^{127} of the printed room line, strictly below it and strictly below the older p/6400 allowance. The selected frontier is unchanged.", + "budget_minutes": 60, + "stop_rule": "Stop after this layout and the p=2 control. Do not evaluate the production plan or replay the 104864-plan census.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/crt-reservoir-envelope-product", + "author": "James Reed", + "ai_assistance": "Substantial assistance from Cursor Grok 4.7.", + "open_questions": [ + { + "question": "On the production plan p=9240576, ell=24, r_max=5, is 3 r_max ((p+2)/2^{ceil(log2(p+2))})^{64} at most 1/6400?", + "why_it_matters": "The equality case fits the room. The same ratio equals 6 on the admitted layout p=2, ell=2, so the room does not survive for every accepted layout.", + "first_step": "Compute ceil(log2(9240578)) and compare 15 (p+2)^{64} with 2^{64 ceil(log2(p+2))} / 6400.", + "blocked_by": "The production plan is not evaluated here." + } + ] +} diff --git a/research/crt-reservoir-envelope-product/VERIFY.json b/research/crt-reservoir-envelope-product/VERIFY.json new file mode 100644 index 0000000000..1cc3a827e5 --- /dev/null +++ b/research/crt-reservoir-envelope-product/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=1, ell=2, G=256, r_max=2 the product 6 * 2^{-256} * 2^{8} * 3^{16} equals 3^{17}/2^{247}. It is 3^{65}/2^{127} of the room line, strictly below 1 and strictly below 1/6400. On p=2, ell=2, r_max=2 the same ratio equals 6 and exceeds the room." + } + ] +} diff --git a/research/crt-reservoir-envelope-product/verify.py b/research/crt-reservoir-envelope-product/verify.py new file mode 100644 index 0000000000..66446c7958 --- /dev/null +++ b/research/crt-reservoir-envelope-product/verify.py @@ -0,0 +1,104 @@ +#!/usr/bin/env python3 +"""Product of 6 * 2^{-256} with the printed E envelope. + +The layout is the #4174 equality case p=1, ell=2, r_max=2, G=256. +The comparison is one rational. No 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-envelope-product" +ALLOCATOR = ROOT / "research/crt-reservoir-placement/allocator.py" + +ENVELOPE = "E(p, ell) ≤ C_E 2^{4 ell} (p+2)^{16}" +ROOM = "≤ 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(ENVELOPE in proof, "printed E envelope") + need(ROOM in proof, "printed room 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 ratio(modulus: int, guard_log: int, factor: int) -> tuple[int, int]: + """factor * ((p+2) / 2^{log})^{64} as an unreduced integer pair.""" + base = modulus + 2 + return factor * base ** 64, 1 << (64 * guard_log) + + +def equality_case(allocator) -> None: + layout = allocator.Layout(1, 2, (1,) * 65536) + need(layout.p == 1 and layout.ell == 2 and layout.G == 256, "equality parameters") + need(layout.r_max == 2 and layout.L == 65536, "equality batch and length") + logarithm = (layout.p + 1).bit_length() + need(logarithm == 2 and layout.G == 64 * (layout.ell + logarithm), "guard matches the formula") + factor = 3 * layout.r_max + need(factor == 6, "prefactor is 6") + numerator, denominator = ratio(layout.p, logarithm, factor) + need(numerator == 6 * 3 ** 64 and denominator == 1 << 128, "raw ratio") + need(numerator // 2 == 3 ** 65 and denominator // 2 == 1 << 127, "reduced ratio 3^{65}/2^{127}") + # 6 * 3^{16} / 2^{248} = 3^{17} / 2^{247}. + need(6 * 3 ** 16 == 2 * 3 ** 17 and (1 << 248) == 2 * (1 << 247), "product is 3^{17}/2^{247}") + room_den = (1 << (60 * layout.ell)) * 3 ** 48 + need(room_den == (1 << 120) * 3 ** 48, "room denominator") + need(3 ** 17 * room_den < (1 << 247), "product is strictly below the room") + need(1 << 103 <= 3 ** 65 < 1 << 104, "ratio lies between 2^{-24} and 2^{-23}") + need(6400 * 3 ** 65 < 1 << 127, "ratio is strictly below 1/6400") + quotient, remainder = divmod(1 << 127, 6400 * 3 ** 65) + need(quotient == 2580 and remainder > 0, "room allowance over the product") + + +def power_of_two_control(allocator) -> None: + """p+2 = 4 is a power of two, so the envelope slack is 1 and the factor 6 remains.""" + layout = allocator.Layout(2, 2, (1,) * 65536) + need(layout.p == 2 and layout.ell == 2 and layout.G == 256 and layout.r_max == 2, "control layout") + logarithm = (layout.p + 1).bit_length() + need(logarithm == 2 and (1 << logarithm) == layout.p + 2, "no envelope slack") + numerator, denominator = ratio(layout.p, logarithm, 3 * layout.r_max) + need(numerator == 6 * denominator, "ratio equals 6") + need(numerator > denominator, "product exceeds the room") + + +def main() -> None: + pins_and_phrases() + allocator = load_allocator() + equality_case(allocator) + power_of_two_control(allocator) + print( + "PASS_CRT_RESERVOIR_ENVELOPE_PRODUCT " + "ratio=3^65/2^127 below_room=1 below_6400=1 control_ratio=6" + ) + + +if __name__ == "__main__": + main()