From a25d6a1289daf53d9360889d8b2e82a04022173b Mon Sep 17 00:00:00 2001 From: James Reed Date: Wed, 21 Oct 2026 20:22:45 -0700 Subject: [PATCH] Record the four-bit bound for the restricted monomial Co-authored-by: Cursor --- research/gaussian-restricted-gate/README.md | 139 ++++++++++++++++++ .../gaussian-restricted-gate/SOURCES.json | 36 +++++ research/gaussian-restricted-gate/TASK.json | 74 ++++++++++ research/gaussian-restricted-gate/VERIFY.json | 23 +++ research/gaussian-restricted-gate/verify.py | 119 +++++++++++++++ 5 files changed, 391 insertions(+) create mode 100644 research/gaussian-restricted-gate/README.md create mode 100644 research/gaussian-restricted-gate/SOURCES.json create mode 100644 research/gaussian-restricted-gate/TASK.json create mode 100644 research/gaussian-restricted-gate/VERIFY.json create mode 100644 research/gaussian-restricted-gate/verify.py diff --git a/research/gaussian-restricted-gate/README.md b/research/gaussian-restricted-gate/README.md new file mode 100644 index 0000000000..a28c68f2b0 --- /dev/null +++ b/research/gaussian-restricted-gate/README.md @@ -0,0 +1,139 @@ +# The restricted monomial keeps the four-bit gate + +**Claim type:** an explicit absorption bound for one scalar monomial. +**No new κ.** The ceiling `9 p^2` and the section error `p^6 exp(-p^2)` +stay hypotheses. The selected record remains `23/10000`. + +## Question + +#4517 bounds the kept core outputs by + +```text +2 g M^{g-1} ε, +``` + +and asks whether that scalar, at `M = 9 p^2` and `ε = p^6 exp(-p^2)`, +still lies below `2^{-C p}`. The named step is to replace the base +`9 p^2 + ε` in #4506 by `9 p^2` and recheck the four-bit gate. + +## Lemma + +Let `p ≥ 2`, `g ≥ 1`, `K ≥ 0` and `C ≥ 0` be integers, and let +`L = ceil(log2 p)`. If + +```text +p ≥ max(64, 4K + 2C) and 16 g L ≤ p, +``` + +then + +```text +2 g (9 p^2)^{g-1} p^6 exp(K p - p^2) < 2^{-C p}. +``` + +The case `K = 0` is the monomial in the question. The factor 2 is one bit. +The exponent is at most `-C p - 2`. Whenever `g log p = o(p)`, every fixed +pair `K, C` satisfies the gate for all large `p`. + +Four bits still majorize the coefficient, because `9 < 16`. Three bits do +not: `9 > 8`. Removing `ε` from the base does not change that count. It +removes the separate room `p^6 exp(-p^2) < 1/2` used by #4506. + +At `g = p^2` the monomial is greater than 1 for every integer `p ≥ 2`. + +## Proof + +The series `1 + 1 + 1/2 = 5/2 > 2` gives `e > 2`, so `exp(-p^2) < 2^{-p^2}`. +For `k ≥ 2`, `k! ≥ 2^{k-1}`. The tail of `e` is then at most a geometric +series of ratio `1/2`, so `e < 4` and `exp(K p) < 2^{2 K p}` whenever +`K p > 0`. At `K = 0` the factor is 1. + +#4496 places the telescoping monomial strictly below `2^{E_0}`, where + +```text +E_0 = 2 g L + 4 g + 5 L - 3 + 2 K p - p^2, +``` + +and proves `E_0 ≤ -C p - 3` under this gate. The identity behind that +exponent is `g (9 p^2)^{g-1} p^6 = g (9 p^2)^g (p^4 / 9)`, with +`p^4 / 9 < 2^{4 L - 3}` because `9 > 8` and `p ≤ 2^L`. The factor 2 in +the present monomial multiplies that bound by `2^1`, so the new exponent is + +```text +E = E_0 + 1 = 2 g L + 4 g + 5 L - 2 + 2 K p - p^2. +``` + +Clear eight times `E + C p`. The pieces scale as `8 · 2 g L = 16 g L ≤ p`, +`8 · 4 g = 32 g ≤ 2 p` because `L ≥ 1` turns the gate into `16 g ≤ p`, +`8 · 5 L = 40 L ≤ 5 p` because `8 L ≤ p` for every integer `p ≥ 64`, and +`8 (2 K + C) p ≤ 4 p^2` once `p ≥ 4 K + 2 C`. The constant `-2` contributes +`-16`. The sum is at most + +```text +-4 (p^2 - 2 p + 4). +``` + +At `p = 2` the polynomial equals 4, and the step to the next integer is +`2 p - 1 ≥ 1`. Eight times `E + C p` is therefore at most `-16`, and +`E ≤ -C p - 2`. The monomial is strictly less than `2^E`, hence strictly +less than `2^{-C p}`. + +The same induction `8(m + 1) ≤ 2^m` for `m ≥ 6` gives `8 L ≤ p` on +`p ≥ 64`. Its base is `8 · 7 = 56 ≤ 64`. + +The three-bit comparison still reverses: `(9 p^2)^g > 2^{3 g} p^{2 g}`. +At the legal point `p = 128`, `L = 7`, `g = 1`, both the three-bit and +four-bit exponents are negative, while `9 p^2 > 8 p^2`. + +At `g = p^2` the monomial is twice the #4496 monomial. That smaller +monomial is already greater than 1, because `(9 p^2)^{p^2} > 4^{p^2}` +and `4 > e`, while `p^4 / 9 > 1`. The extra factor 2 keeps it above 1. + +## Not covered + +- A proof of the restricted tensor bound in #4517. This package absorbs + the scalar only after `M = 9 p^2` and `ε = p^6 exp(-p^2)` are granted. +- A proof that `||C_i|| ≤ 9 p^2`, or that `||P_glob - C_i||_2 < ε`. +- Either ideal-gap hypothesis. +- Editing the #4100 notes. They still say `g p^{10 g} exp(-p^2)`. +- Any new κ. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/gaussian-restricted-gate --check-only +python3.12 -B scripts/research_package.py --package research/gaussian-restricted-gate +``` + +Base `f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc`, priority revision 7, selection +refresh κ = `23/10000`. Upstream was fetched at 2026-10-22T03:18:46Z and was +that commit. + +Overlap snapshot: open PRs fetched 2026-10-22T03:21:17Z (305 records) and +discussions fetched 2026-10-22T03:21:59Z (3397 records). A search for +`restricted bound`, `(9 p^2)^{g-1}` and `Cp - 2` returned #4496, which +absorbs the monomial without the factor 2, and #4506, which absorbs the +factor 2 only after the base has grown by `ε`. The other hits are the +predecessor gate and unrelated restricted bounds. No result charges the +factor 2 against the fold slack of 3. A search miss is not a novelty +certificate. #4496 is the fold. #4506 is the larger base. HALO is the +written error. + +## Open next questions + +1. **Is `||P_glob - C_i||_2` below `p^6 exp(-p^2)`, or only the written + `p^{10} exp(-p^2)`?** The restricted monomial uses the section error. + The global tail in HALO is `p^{10}`. Replacing the section error by + that tail would add `4 L` to the exponent. The first step is to compare + `P - H^{-1} = -Q^J H^{-1}` with the within-cell `p^6` bound, and not + to put `p^{10}` into this gate yet. + +## Credit + +- The fold exponent `-C p - 3`, and the factor `p^4 / 9`, are #4496's. +- The face-factor inequality with base `9 p^2 + ε` is #4506's. +- The restricted scalar `2 g M^{g-1} ε`, and this question, are #4517's. +- The four-bit gate is #4495's. +- The written error `g p^{10 g} exp(-p^2)` is #4100's. + +Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0. diff --git a/research/gaussian-restricted-gate/SOURCES.json b/research/gaussian-restricted-gate/SOURCES.json new file mode 100644 index 0000000000..e599896ee9 --- /dev/null +++ b/research/gaussian-restricted-gate/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/gaussian-tensor-nine-faces/README.md", + "usage": "input", + "git_blob": "03ac0ffa1ed344a62902cd9b2320e26d60cca003", + "sha256": "bb733a49416eddd574d64a9e9092ef1ba8dc0fb22f2eea15f7f3ce0d280d7aee" + }, + { + "path": "research/gaussian-tensor-nine-fold/README.md", + "usage": "input", + "git_blob": "af78553b992a9f1801423b3ba42d984cdbe12c4d", + "sha256": "8e003f1ec809b5c7b8f6552592ccd32d1d806ba55b58bae60fff220b959b2d05" + }, + { + "path": "research/unconditional-batched-crt/HALO.md", + "usage": "input", + "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b", + "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc" + } + ] +} diff --git a/research/gaussian-restricted-gate/TASK.json b/research/gaussian-restricted-gate/TASK.json new file mode 100644 index 0000000000..bae3ff43c8 --- /dev/null +++ b/research/gaussian-restricted-gate/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Absorb 2 g (9 p^2)^{g-1} p^6 exp(K p - p^2) by the same four-bit gate, with the approximant increment removed from the base.", + "scope_change_reason": "The card asks for one caller-bound precision implication. This package only rechecks that scalar gate. It does not prove the restricted tensor bound, the ideal gaps, or a new kappa.", + "bottleneck_link": "The selected frontier is unchanged. This is the 2^{-C p} comparison left open by the core-row operator lift.", + "budget_minutes": 60, + "stop_rule": "Stop once the restricted monomial is below 2^{-C p}. Do not prove ||C_i|| <= 9 p^2, do not replace p^6 by the global tail, do not edit the #4100 notes, and do not claim a new kappa.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/gaussian-restricted-gate", + "author": "James Reed", + "ai_assistance": "Substantial help from Cursor Grok 4.7 on the one-bit slack check and the package text.", + "open_questions": [ + { + "question": "Is ||P_glob - C_i||_2 below p^6 exp(-p^2), or only the written p^{10} exp(-p^2)?", + "why_it_matters": "The restricted monomial uses the section error p^6. The global tail in HALO is p^{10}, and replacing it would add 4 L to the exponent.", + "first_step": "Compare the global identity P - H^{-1} = -Q^J H^{-1} with the within-cell p^6 bound, and do not put p^{10} into this gate yet.", + "blocked_by": "The section ceiling 9 p^2 and both ideal-gap gauges remain hypotheses, and the global inverse norm is not the within-cell Neumann ceiling." + } + ] +} diff --git a/research/gaussian-restricted-gate/VERIFY.json b/research/gaussian-restricted-gate/VERIFY.json new file mode 100644 index 0000000000..2f0129bab1 --- /dev/null +++ b/research/gaussian-restricted-gate/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/gaussian-tensor-nine-faces/README.md", + "research/gaussian-tensor-nine-fold/README.md", + "research/unconditional-batched-crt/HALO.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Under p >= max(64, 4K+2C) and 16 g L <= p, the factor 2 adds one bit to the fold exponent. Eight times the new exponent is at most -16, so the exponent is at most -C p - 2. Three bits still fail because 9 > 8. At g = p^2 the monomial exceeds 1." + } + ] +} diff --git a/research/gaussian-restricted-gate/verify.py b/research/gaussian-restricted-gate/verify.py new file mode 100644 index 0000000000..4e5c668b09 --- /dev/null +++ b/research/gaussian-restricted-gate/verify.py @@ -0,0 +1,119 @@ +#!/usr/bin/env python3 +"""Absorb the restricted monomial by the same four-bit gate. + +Every comparison is an integer identity. The ceiling and the section error +stay hypotheses. +""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "gaussian-restricted-gate" + + +def digest(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def ceil_log2(value: int) -> int: + level = 0 + power = 1 + while power < value: + power *= 2 + level += 1 + return level + + +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": + assert digest(ROOT / row["path"]) == row["sha256"], row["path"] + halo = (ROOT / "research/unconditional-batched-crt/HALO.md").read_text(encoding="utf-8") + fold = (ROOT / "research/gaussian-tensor-nine-fold/README.md").read_text(encoding="utf-8") + faces = (ROOT / "research/gaussian-tensor-nine-faces/README.md").read_text(encoding="utf-8") + selected = json.loads( + (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8") + ) + assert "g p^(10g) exp(-p^2)," in halo + assert "Keep outputs at distance A" in halo + assert "The resulting exponent is at most" in fold + assert "`-C p - 3`" in fold + assert ( + "2 g (9 p^2 + p^6 exp(-p^2))^{g-1} p^6 exp(K p - p^2) < 2^{-C p}." + in faces + ) + assert selected["kappa"] == "23/10000" + + +def series_and_bits() -> None: + # e > 5/2 > 2 and e < 4. Four bits clear 9; three bits do not. + assert 2 + 2 + 1 > 4 + assert 3 < 4 + assert 2 >= 2 and 6 >= 4 and 24 >= 8 + assert 8 < 9 < 16 + assert 2**3 == 8 + assert 2**4 == 16 + # The factor 2 is one bit, taken from the fold slack of 3. + assert 2**1 == 2 + assert 8 * (-3) == -24 + assert 8 * (-2) == -16 + assert -24 + 8 == -16 + + +def log_and_budget() -> None: + # 8 L <= p for every integer p >= 64, by the same induction as #4495. + assert 8 * 7 <= 64 + assert 8 <= 64 + assert 2**6 + 8 <= 2**7 + assert ceil_log2(64) == 6 + assert ceil_log2(128) == 7 + # Eight times the new pieces: 2 g L, 4 g, 5 L, and the constant -2. + assert 8 * 2 == 16 + assert 8 * 4 == 32 + assert 32 == 2 * 16 + assert 8 * 5 == 40 + assert 40 == 5 * 8 + assert 1 + 2 + 5 == 8 + # (2K + C) p <= p^2 / 2 becomes 8(2K + C) p <= 4 p^2 when p >= 4K + 2C. + assert 8 * (2 * 3 + 5) == 4 * (4 * 3 + 2 * 5) + # p^2 - 2 p + 4 is 4 at p = 2 and then increases by 2 p - 1. + assert 2 * 2 - 2 * 2 + 4 == 4 + assert -4 * 4 == -16 + assert (3 * 3 - 2 * 3 + 4) - (2 * 2 - 2 * 2 + 4) == 2 * 2 - 1 + + +def witness_and_failures() -> None: + prime = 128 + level = ceil_log2(prime) + groups = 1 + assert 16 * groups * level <= prime + # E = 2 g L + 4 g + 5 L - 2 - p^2 at K = 0. + exponent = 2 * groups * level + 4 * groups + 5 * level - 2 - prime * prime + assert exponent == -16333 + assert exponent <= -2 + # Three bits do not majorize 9, even though that exponent is negative. + four_bit = level + 4 * groups + 2 * groups * level - prime * prime + three_bit = level + 3 * groups + 2 * groups * level - prime * prime + assert four_bit < 0 and three_bit < 0 + assert 9 * prime * prime > 8 * prime * prime + # At g = p^2 the monomial exceeds 1. These are the integer ingredients. + assert 9 * 2 * 2 > 4 + assert 2**4 > 9 + assert 2 > 1 + + +def main() -> None: + pins_and_phrases() + series_and_bits() + log_and_budget() + witness_and_failures() + print("PASS_GAUSSIAN_RESTRICTED_GATE") + + +if __name__ == "__main__": + main()