From 290fb5353db1b207a3eb2078e38717ff4c7a2ed7 Mon Sep 17 00:00:00 2001 From: James Reed Date: Thu, 22 Oct 2026 08:32:54 -0700 Subject: [PATCH] Record the factor-3 gate for one heavy slice Co-authored-by: Cursor --- research/gaussian-slice-three-gate/README.md | 128 ++++++++++++++++++ .../gaussian-slice-three-gate/SOURCES.json | 36 +++++ research/gaussian-slice-three-gate/TASK.json | 74 ++++++++++ .../gaussian-slice-three-gate/VERIFY.json | 23 ++++ research/gaussian-slice-three-gate/verify.py | 99 ++++++++++++++ 5 files changed, 360 insertions(+) create mode 100644 research/gaussian-slice-three-gate/README.md create mode 100644 research/gaussian-slice-three-gate/SOURCES.json create mode 100644 research/gaussian-slice-three-gate/TASK.json create mode 100644 research/gaussian-slice-three-gate/VERIFY.json create mode 100644 research/gaussian-slice-three-gate/verify.py diff --git a/research/gaussian-slice-three-gate/README.md b/research/gaussian-slice-three-gate/README.md new file mode 100644 index 0000000000..1db6df48f6 --- /dev/null +++ b/research/gaussian-slice-three-gate/README.md @@ -0,0 +1,128 @@ +# The factor-3 gate absorbs one heavy slice + +**Claim type:** an explicit absorption bound for one tensor slice. +**No new κ.** The trailing bound `p^{10}`, the section error, and the +ceiling `9 p^2` stay hypotheses. The selected record is `60403/20000000`. +The coefficient-9 monomials keep the published gate `16 g L ≤ p`. + +## Question + +#4676 absorbs the `g` copies under `4 g L ≤ p`, and asks whether one heavy +slice already fits under `3 g L ≤ p`. The exponent spends `10 g L`. The +named step is the thirds identity `240 g L = 80 · 3 g L`, then the test of +`12 p^2 - 80 p - 48` at `p = 64`. + +This `3` is the coefficient of `g L`. It is not a three-bit majorant of +the ceiling `9`. #4495 still rejects three bits for that ceiling, because +`9 > 8`, and it still uses four bits because `9 < 16`. + +## 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 3 g L ≤ p, +``` + +then + +```text +(p^{10})^{g-1} p^6 (1 + p^4) exp(K p - p^2) +``` + +is strictly below `2^{-C p}`. The case `K = 0` is the slice in the +question. The exponent is at most `-C p - 1`. + +This hypothesis is wider than the factor-4 gate. At `p = 84` and `g = 4`, +`L = 7`, so `3 g L = 84 ≤ 84` while `4 g L = 112 > 84`. The exponent +there is `-6775`. The factor-4 comparison `320 g L ≤ 80 p` fails at that +point: `8960 > 6720`. + +At `p = 2` and `g = 1` the hypothesis fails, and the slice is larger +than `1`. + +## Proof + +Dropping the `1` in `1 + p^4` leaves exactly `p^{10 g}`. Since +`1 + p^4 < 2 p^4 ≤ 2^{4 L + 1}` and `p ≤ 2^L`, the polynomial part is +strictly below `2^{10 g L + 1}`. With `exp(-p^2) < 2^{-p^2}` and +`exp(K p) ≤ 2^{2 K p}`, the slice is strictly below `2^E` for + +```text +E = 10 g L + 1 + 2 K p - p^2. +``` + +Clear `24 (E + C p)`, which is three times `8 (E + C p)`. The new gate +gives `240 g L = 80 · 3 g L ≤ 80 p`. The identity +`24 (2 K + C) = 12 (4 K + 2 C)` gives a linear contribution of at most +`12 p^2` once `p ≥ 4 K + 2 C`. The constant `1` contributes `24`. The +sum is at most + +```text +-(12 p^2 - 80 p - 24). +``` + +The polynomial `12 p^2 - 80 p - 48` equals `43984` at `p = 64` and then +increases by `24 p - 68`. Thus `12 p^2 - 80 p - 24 ≥ 24` for every +integer `p ≥ 64`, so `24 (E + C p) ≤ -24` and `E ≤ -C p - 1`. + +At `p = 2` and `g = 1`, `3 g L = 3 > 2`. The series of `e` through +`1/6!` is `13699/5040`. Terms after that have ratios at most `1/8`, so +the tail is strictly below `8/(7 · 5040)`. The gap up to `3` is +`1421/5040`, and `8 < 1421 · 7`, so `e < 3` and `exp(4) < 81`. The slice +equals `1088 exp(-4)`, and `81 < 1088`, so the slice is larger than `1`. + +## Not covered + +- The `g` copies of this slice under `3 g L ≤ p`. +- A gate factor smaller than `3`. +- A proof that `||H^{-1}||_2 ≤ p^{10}`. HALO assumes it. +- The section error `p^6 exp(-p^2)` and the leading ceiling `9 p^2`. +- Editing the #4100 notes, or the #4495 gate. +- Any new κ. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/gaussian-slice-three-gate --check-only +python3.12 -B scripts/research_package.py --package research/gaussian-slice-three-gate +``` + +Base `b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, priority revision 7. +Upstream was fetched at 2026-10-22T15:31:12Z and was that commit. The +pre-submit fetch at 2026-10-22T15:32:46Z was the same commit. The pinned +blobs for the selected record, the catalogue, both source READMEs, and +HALO.md match that main. The selection is κ = `60403/20000000`. + +Overlap snapshot: open PRs fetched 2026-10-22T15:31:50Z (446 records) and +discussions fetched 2026-10-22T15:32:39Z (3604 records). Terms +`12 p^2 - 80 p - 48`, `slice-three-gate`, and `6775` reported 20 matches +and showed 8. The first two were this README and this TASK. One shown hit +is the #4676 DONE (discussioncomment-19126711). The other shown hits +contain the digits `6775` inside timestamps, job ids, comment URLs, or +commit hashes. A second search of the same cache, offline, dropped +`6775`. It returned this README, this TASK, and that #4676 DONE. That +note leaves this one-slice question open and names the test at `p = 64`. +The handoff thread, reread at the pre-submit fetch, still ends at that +#4676 DONE. The open-PR list at that time still starts at #4676. No +matches is not a novelty certificate. + +## Open next questions + +1. **Do the `g` copies stay below `2^{-C p}` under `3 g L ≤ p`?** The + one-slice thirds spend `80 p`. Copies add one `L`, and `8 L ≤ p` + turns `24 L` into `3 p`. The first step is to test + `12 p^2 - 83 p - 48` at `p = 64`. Do not change the coefficient-9 + monomial gate. + +## Credit + +- The factor-4 copies, and this question, are #4676's. +- The factor-4 slice is #4673's. +- The unequal factor `1 + p^4` is #4524's. +- The published gate `16 g L ≤ p` is #4495's. It is unchanged. +- The ceiling `9 p^2` is #4493's. +- The written tail `p^{10} 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-slice-three-gate/SOURCES.json b/research/gaussian-slice-three-gate/SOURCES.json new file mode 100644 index 0000000000..3f486d5587 --- /dev/null +++ b/research/gaussian-slice-three-gate/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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/gaussian-neumann-nine/README.md", + "usage": "input", + "git_blob": "54a8ce117a233e54e5057fd1edfa378e59527592", + "sha256": "189a0fb9ede1649ffea24ea22605a573366170e172ac563dd001c68d65b966ac" + }, + { + "path": "research/gaussian-tensor-nine/README.md", + "usage": "input", + "git_blob": "96c9f03626d145bf38a9d4850f0aba4b05c0279c", + "sha256": "a71bc77ba9885e1c5f231ad3b89d01da7860aae53b08ac87b4abca507fec8b82" + }, + { + "path": "research/unconditional-batched-crt/HALO.md", + "usage": "input", + "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b", + "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc" + } + ] +} diff --git a/research/gaussian-slice-three-gate/TASK.json b/research/gaussian-slice-three-gate/TASK.json new file mode 100644 index 0000000000..c61d37b087 --- /dev/null +++ b/research/gaussian-slice-three-gate/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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": "Show that 3 g ceil(log2 p) <= p and p >= max(64, 4K + 2C) put one heavy slice (p^{10})^{g-1} p^6 (1 + p^4) exp(K p - p^2) strictly below 2^{-C p}.", + "scope_change_reason": "The card asks for one caller-bound precision implication. This package only clears that scalar exponent under the factor-3 gate. It does not replace the coefficient-9 monomial gate, does not prove ||H^{-1}||_2 <= p^{10}, and does not claim a new kappa.", + "bottleneck_link": "The selected frontier is unchanged. This is the factor-3 gate left open by the factor-4 copies.", + "budget_minutes": 60, + "stop_rule": "Stop once one heavy slice is below 2^{-C p} under 3 g L <= p. Do not absorb the g copies under this gate, do not lower the factor from 3 to 2, do not change the coefficient-9 monomial gate, do not prove the inverse bound, and do not claim a new kappa.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/gaussian-slice-three-gate", + "author": "James Reed", + "ai_assistance": "Substantial help from Cursor Grok 4.7 on the factor-3 exponent and the package text.", + "open_questions": [ + { + "question": "Do the g copies of this slice stay below 2^{-C p} under 3 g ceil(log2 p) <= p?", + "why_it_matters": "The one-slice thirds spend 80 p. Copies add one L, and 8 L <= p turns 24 L into 3 p. The coefficient-9 monomials still use 16.", + "first_step": "Test 12 p^2 - 83 p - 48 at p = 64. Do not change the coefficient-9 monomial gate.", + "blocked_by": "The trailing p^{10} factor and the section error remain hypotheses." + } + ] +} diff --git a/research/gaussian-slice-three-gate/VERIFY.json b/research/gaussian-slice-three-gate/VERIFY.json new file mode 100644 index 0000000000..124a5f4398 --- /dev/null +++ b/research/gaussian-slice-three-gate/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/gaussian-neumann-nine/README.md", + "research/gaussian-tensor-nine/README.md", + "research/unconditional-batched-crt/HALO.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Under 3 g L <= p and p >= 64 the heavy-slice exponent is at most -C p - 1. At p = 84 and g = 4 this gate holds and the factor-4 gate fails. At p = 2 and g = 1 the slice exceeds 1." + } + ] +} diff --git a/research/gaussian-slice-three-gate/verify.py b/research/gaussian-slice-three-gate/verify.py new file mode 100644 index 0000000000..dcdd2e3768 --- /dev/null +++ b/research/gaussian-slice-three-gate/verify.py @@ -0,0 +1,99 @@ +#!/usr/bin/env python3 +"""Absorb one heavy slice by the factor-3 gate. + +Every comparison is an integer identity. The inverse bound stays a hypothesis. +The coefficient-9 monomial gate stays at 16. +""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "gaussian-slice-three-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"] + gate = (ROOT / "research/gaussian-tensor-nine/README.md").read_text(encoding="utf-8") + nine = (ROOT / "research/gaussian-neumann-nine/README.md").read_text(encoding="utf-8") + halo = (ROOT / "research/unconditional-batched-crt/HALO.md").read_text(encoding="utf-8") + selected = json.loads( + (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8") + ) + assert "16 g L ≤ p" in gate + assert "9 < 16" in gate + assert "9 > 8" in gate + assert "8 p^2 < U < 9 p^2." in nine + assert "||P_i-H_i^-1||_2 <= p^10 exp(-p^2)." in halo + assert selected["kappa"] == "60403/20000000" + + +def thirds() -> None: + # Three times the eighths is 24 (E + C p). The gate enters as 80 * 3 g L. + assert 80 * 3 == 240 + assert 3 * 8 == 24 + assert 3 * 4 == 12 + assert 24 * (2 * 3 + 5) == 12 * (4 * 3 + 2 * 5) + # 12 p^2 - 80 p - 48 is positive at p = 64 and increases by 24 p - 68. + assert 12 * 64 * 64 - 80 * 64 - 48 == 43984 + assert 43984 > 0 + assert (12 * 65 * 65 - 80 * 65 - 48) - 43984 == 24 * 64 - 68 + # Dropping the 1 in 1 + p^4 leaves p^{10 g}. + assert 10 * (2 - 1) + 6 + 4 == 10 * 2 + assert 1 + 2**4 < 2 * 2**4 + + +def separates_four() -> None: + # p = 84, g = 4 meets factor 3 and misses factor 4. + assert ceil_log2(84) == 7 + assert 3 * 4 * 7 <= 84 + assert 4 * 4 * 7 > 84 + # The factor-4 line 320 g L <= 80 p fails at this point. + assert 320 * 4 * 7 > 80 * 84 + one = 10 * 4 * 7 + 1 - 84 * 84 + assert one == -6775 + assert one <= -1 + + +def outside() -> None: + # At p = 2 and g = 1 the factor-3 hypothesis fails, and the slice exceeds 1. + assert ceil_log2(2) == 1 + assert 3 * 1 * 1 > 2 + total = 5040 + 5040 + 2520 + 840 + 210 + 42 + 7 + assert total == 13699 + assert 3 * 5040 - total == 1421 + assert 8 < 1421 * 7 + assert 3**4 == 81 + assert 2**6 * (1 + 2**4) == 1088 + assert 81 < 1088 + + +def main() -> None: + pins_and_phrases() + thirds() + separates_four() + outside() + print("PASS_GAUSSIAN_SLICE_THREE_GATE") + + +if __name__ == "__main__": + main()