From 2a49377931472fadf7016bc0b188d8322681e741 Mon Sep 17 00:00:00 2001 From: James Reed Date: Wed, 21 Oct 2026 18:58:31 -0700 Subject: [PATCH] Record the approximant base with coefficient 9 Co-authored-by: Cursor --- .../README.md | 156 ++++++++++++++++++ .../SOURCES.json | 24 +++ .../TASK.json | 74 +++++++++ .../VERIFY.json | 21 +++ .../verify.py | 119 +++++++++++++ 5 files changed, 394 insertions(+) create mode 100644 research/gaussian-tensor-nine-approximant/README.md create mode 100644 research/gaussian-tensor-nine-approximant/SOURCES.json create mode 100644 research/gaussian-tensor-nine-approximant/TASK.json create mode 100644 research/gaussian-tensor-nine-approximant/VERIFY.json create mode 100644 research/gaussian-tensor-nine-approximant/verify.py diff --git a/research/gaussian-tensor-nine-approximant/README.md b/research/gaussian-tensor-nine-approximant/README.md new file mode 100644 index 0000000000..0d7aadbf72 --- /dev/null +++ b/research/gaussian-tensor-nine-approximant/README.md @@ -0,0 +1,156 @@ +# The approximant base 9 p^2 + p^6 exp(-p^2) stays inside the budget + +**Claim type:** an explicit absorption bound for one approximant monomial. +**No new κ.** The section ceiling `9 p^2` and the section error +`p^6 exp(-p^2)` stay hypotheses. The selected record remains `23/10000`. + +## Question + +#4496 absorbs `g (9 p^2)^{g-1} p^6 exp(K p - p^2)` under the gate +`p ≥ max(64, 4K + 2C)` and `16 g ceil(log2 p) ≤ p`. If each of the `g - 1` +factors is an approximant, the base becomes `9 p^2 + p^6 exp(-p^2)`. Does + +```text +g (9 p^2 + p^6 exp(-p^2))^{g-1} p^6 exp(K p - p^2) +``` + +stay below `2^{-C p}` under that same 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 +g (9 p^2 + p^6 exp(-p^2))^{g-1} p^6 exp(K p - p^2) < 2^{-C p}. +``` + +The case `K = 0` is the monomial in the question. A global factor `exp(K p)` +does not change the conclusion. Whenever `g log p = o(p)`, every fixed pair +`K, C` satisfies the gate for all large `p`. + +For every integer `p ≥ 64`, the section error is strictly below `1/2`, so + +```text +9 p^2 + p^6 exp(-p^2) < 9 p^2 + 1 < 16 p^2. +``` + +The base therefore remains strictly below the power of two already used for +`(16 p^2)^{g-1}`. No extra bit is spent. The exponent is at most `-C p - 4`. +At `g = p^2` the same error is greater than 1 for every integer `p ≥ 2`, +because it is larger than the inverse-ceiling monomial, which is already +greater than 1. + +## 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 values at 2, 3 and 4 are `2`, `6` and `24`, +and the step uses `k + 1 ≥ 2`. The tail of `e` is then at most the geometric +series of ratio `1/2`, so `e < 3 < 4` and `exp(K p) ≤ 2^{2 K p}`, with +equality only at `K = 0`. + +For every integer `p ≥ 64`, `8 L ≤ p`. The base is `8 · 7 = 56 ≤ 64` at +`p = 2^6`, and `8 ≤ 64`. If `8(m + 1) ≤ 2^m`, then +`8(m + 2) ≤ 2^m + 8 ≤ 2^{m+1}`. On each dyadic interval the largest ratio of +`L` to `p` is at the left endpoint. From `8 L ≤ p`, `48 L = 6 · 8 L ≤ 6 p`. +The quadratic `4 p^2 - 3 p - 4` equals 6 at `p = 2` and increases by `8 p + 1` +at the next integer, so it stays positive. Equivalently +`6 p ≤ 8(p^2 - 1)`. Combining these estimates gives `6 L ≤ p^2 - 1`. Since +`p ≤ 2^L`, `p^6 ≤ 2^{6 L} ≤ 2^{p^2 - 1}`, and therefore + +```text +p^6 exp(-p^2) < p^6 2^{-p^2} ≤ 1/2. +``` + +Hence `9 p^2 + p^6 exp(-p^2) < 9 p^2 + 1`. Also `1 < 7 p^2` for every +integer `p ≥ 2`, so `9 p^2 + 1 < 16 p^2`. The approximant base is strictly +smaller than `16 p^2`. + +At `g = 1` the power `g - 1` is zero. For `g ≥ 2`, + +```text +(9 p^2 + p^6 exp(-p^2))^{g-1} < (16 p^2)^{g-1} + = 2^{4(g-1)} p^{2(g-1)}. +``` + +In both cases + +```text +g (9 p^2 + p^6 exp(-p^2))^{g-1} p^6 exp(K p - p^2) + < g 2^{4g-4} p^{2g+4} 2^{2 K p - p^2}. +``` + +The gate forces `g < 2^L`, because `L ≥ 1` and `g ≤ p/(16 L) ≤ p/16`. +Together with `p ≤ 2^L`, the product is strictly less than + +```text +2^{2 g L + 4 g + 5 L - 4 + 2 K p - p^2}. +``` + +Clear the eighths. The four pieces scale as `8 · 2 g L = 16 g L ≤ p`, +`8 · 4 g = 2 · 16 g ≤ 2 p`, `8 · 5 L = 5 · 8 L ≤ 5 p`, and +`8 (2 K + C) p ≤ 4 p^2` once `p ≥ 4 K + 2 C`, because +`8(2 K + C) = 4(4 K + 2 C)`. The constant `-4` contributes `-32`. The sum +is at most `-4(p^2 - 2 p + 8)`. The coefficients of `p` are `1 + 2 + 5 = 8`. +At `p = 2` the polynomial equals 8, and the step to the next integer is +`2 p - 1`. It is therefore at least 8, so eight times the shifted exponent +is at most `-32`. The exponent is at most `-C p - 4`. + +If `g log p = o(p)`, then `g log2 p ≤ p/32` for large `p`. For `p ≥ 3`, +`L ≤ 2 log2 p`, so the gate holds eventually, and every fixed `K` and `C` +satisfy `p ≥ 4 K + 2 C` as well. + +At `g = p^2` the approximant monomial is larger than +`g (9 p^2)^{g-1} p^6 exp(-p^2)`, since the added section error is positive +and `g ≥ 2`. The smaller monomial equals +`g (9 p^2)^g exp(-p^2) · p^4 / 9`. Here +`(9 p^2)^{p^2} > 4^{p^2} > exp(p^2)` because `9 p^2 ≥ 36 > 4` and `e < 4`, +while `p^4 / 9 > 1` because `p^4 ≥ 16 > 9`. That product is greater than 1, +and so is the approximant monomial. + +## Not covered + +- A proof that a section inverse is at most `9 p^2`, or that a section + error is less than `p^6 exp(-p^2)`. The approximant ceiling is their sum. +- The factor `2` in front of `g`. +- 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-tensor-nine-approximant --check-only +python3.12 -B scripts/research_package.py --package research/gaussian-tensor-nine-approximant +``` + +Base `2a13eb1827784206202db90e5dc8327cf8a250db`, priority revision 7, selection +refresh κ = `23/10000`. Upstream was fetched at 2026-10-22T01:56:48Z and was +still that commit. + +Overlap snapshot: open PRs fetched 2026-10-22T01:57:24Z (350 records) and +discussions fetched 2026-10-22T01:58:13Z (3374 records). A search for +`9 p^2 + 1`, `9 p^2 + p^6` and `approximant base` returned this draft, #4496, +which leaves the base open, and the coefficient-10 packages #4486 and #4487. +A search miss is not a novelty certificate. #4496 is the predecessor fold. +HALO is the written error. + +## Open next questions + +1. **Does the face factor 2 still fit?** The exponent above is at most + `-C p - 4`. The first step is to charge that extra factor of 2 against + this slack of 4. + +## Credit + +- The section-error comparison `p^6 2^{-p^2} ≤ 1/2` is the route of #4486. +- The predecessor fold with coefficient 9 is #4496. +- The section error `p^6 exp(-p^2)` is the within-cell bound of #4452. +- 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-tensor-nine-approximant/SOURCES.json b/research/gaussian-tensor-nine-approximant/SOURCES.json new file mode 100644 index 0000000000..b6dd82035c --- /dev/null +++ b/research/gaussian-tensor-nine-approximant/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "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/unconditional-batched-crt/HALO.md", + "usage": "input", + "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b", + "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc" + } + ] +} diff --git a/research/gaussian-tensor-nine-approximant/TASK.json b/research/gaussian-tensor-nine-approximant/TASK.json new file mode 100644 index 0000000000..c592e865bb --- /dev/null +++ b/research/gaussian-tensor-nine-approximant/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "2a13eb1827784206202db90e5dc8327cf8a250db", + "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": "Decide whether g (9 p^2 + p^6 exp(-p^2))^{g-1} p^6 exp(K p - p^2) stays below 2^{-C p} under the same gate, after checking p^6 exp(-p^2) < 1/2 and 9 p^2 + 1 < 16 p^2.", + "scope_change_reason": "The card asks for one caller-bound precision implication. This package only places the approximant base under the telescoping budget. It does not prove the section bounds and does not claim a new kappa.", + "bottleneck_link": "The selected frontier is unchanged. This is the approximant base left open by the coefficient-9 fold.", + "budget_minutes": 60, + "stop_rule": "Stop once the approximant base is compared with 16 p^2 and the monomial is absorbed. Do not charge the face factor 2, do not prove the ideal gaps, 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-tensor-nine-approximant", + "author": "James Reed", + "ai_assistance": "Substantial help from Cursor Grok 4.7 on the approximant comparison and the package text.", + "open_questions": [ + { + "question": "Does the face factor 2 still fit in front of the coefficient-9 approximant monomial?", + "why_it_matters": "The exponent slack is 4, and a review note asks for a constant 2 in front of the core error.", + "first_step": "Charge that extra factor of 2 against the slack of 4, leaving an exponent of at most -C p - 3.", + "blocked_by": "The section ceiling 9 p^2 and the section error p^6 exp(-p^2) remain hypotheses until the ideal gaps are proved." + } + ] +} diff --git a/research/gaussian-tensor-nine-approximant/VERIFY.json b/research/gaussian-tensor-nine-approximant/VERIFY.json new file mode 100644 index 0000000000..4305d9c441 --- /dev/null +++ b/research/gaussian-tensor-nine-approximant/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/unconditional-batched-crt/HALO.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "For p >= 64, p^6 exp(-p^2) < 1/2, so 9 p^2 + p^6 exp(-p^2) < 9 p^2 + 1 < 16 p^2; under the same gate the approximant monomial stays below 2^{-C p} with exponent at most -C p - 4." + } + ] +} diff --git a/research/gaussian-tensor-nine-approximant/verify.py b/research/gaussian-tensor-nine-approximant/verify.py new file mode 100644 index 0000000000..37cfe979e1 --- /dev/null +++ b/research/gaussian-tensor-nine-approximant/verify.py @@ -0,0 +1,119 @@ +#!/usr/bin/env python3 +"""The approximant base 9 p^2 + p^6 exp(-p^2) stays inside the telescoping budget. + +Every comparison is an integer identity. The section ceiling and the section +error are hypotheses. +""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "gaussian-tensor-nine-approximant" + + +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") + selected = json.loads( + (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8") + ) + assert "g p^(10g) exp(-p^2)," in halo + assert "exp(O(p)) leaves this below 2^-Cp for every fixed C eventually, provided" in halo + assert "g log p=o(p)." in halo + assert selected["kappa"] == "23/10000" + + +def series_bounds() -> None: + # e > 1 + 1 + 1/2 = 5/2 > 2, and e < 3 < 4. + assert 5 > 4 + assert 3 < 4 + assert 2 >= 2 + assert 6 >= 4 + assert 24 >= 8 + assert 3 >= 2 + # 9 p^2 + 1 < 16 p^2 because 1 < 7 p^2. At g = 1 the power g-1 vanishes. + assert 7 * 4 > 1 + assert 9 < 16 + assert 2**4 == 16 + assert 4 * 1 - 4 == 0 + + +def section_error_room() -> None: + # 8 L <= p implies 48 L <= 6 p, and 6 p <= 8(p^2 - 1) for every integer p >= 2. + assert 6 * 8 == 48 + assert 8 * (2**2 - 1) - 6 * 2 == 2 * (4 * 2**2 - 3 * 2 - 4) + assert 4 * 2**2 - 3 * 2 - 4 == 6 + assert (4 * 3**2 - 3 * 3 - 4) - (4 * 2**2 - 3 * 2 - 4) == 8 * 2 + 1 + # Witness: p=128, L=7 has 6 L <= p^2 - 1, so p^6 2^{-p^2} <= 1/2. + assert ceil_log2(128) == 7 + assert 6 * 7 <= 128**2 - 1 + assert 2 * (2**3) == 2**4 + + +def log_induction() -> None: + # For m >= 6, 8(m+1) <= 2^m, so 8 ceil(log2 p) <= p for every integer p >= 64. + assert 8 * 7 <= 64 + assert 8 <= 64 + assert 2**6 + 8 <= 2**7 + assert ceil_log2(2) == 1 + assert ceil_log2(64) == 6 + assert ceil_log2(65) == 7 + assert ceil_log2(128) == 7 + assert 8 * ceil_log2(128) <= 128 + + +def budget() -> None: + # The same eighths as the inverse-ceiling fold, with constant -4. + assert 8 * 2 == 16 + assert 8 * 4 == 2 * 16 + assert 8 * 5 == 5 * 8 + assert 1 + 2 + 5 == 8 + assert 4 * (4 * 3 + 2 * 5) == 8 * (2 * 3 + 5) + prime = 7 + budget_value = prime + 2 * prime + 5 * prime + 4 * prime * prime - 32 - 8 * prime * prime + assert budget_value == -4 * (prime * prime - 2 * prime + 8) + assert 2**2 - 2 * 2 + 8 == 8 + assert (3**2 - 2 * 3 + 8) - (2**2 - 2 * 2 + 8) == 2 * 2 - 1 + assert 8 * 4 == 32 + width = 128 + level = ceil_log2(width) + groups = 1 + assert 16 * groups * level <= width + slack = 2 * groups * level + 4 * groups + 5 * level - 4 - width * width + assert slack <= -4 + # g = p^2 still leaves the smaller inverse-ceiling monomial above 1. + assert 9 * 4 > 4 + assert 2**4 > 9 + + +def main() -> None: + pins_and_phrases() + series_bounds() + section_error_room() + log_induction() + budget() + print("PASS_GAUSSIAN_TENSOR_NINE_APPROXIMANT") + + +if __name__ == "__main__": + main()