diff --git a/research/gaussian-core-side/README.md b/research/gaussian-core-side/README.md new file mode 100644 index 000000000..5c7a6ad38 --- /dev/null +++ b/research/gaussian-core-side/README.md @@ -0,0 +1,116 @@ +# The core side exponent falls from 400 to 80 + +**Claim type:** exponent arithmetic for HALO's sparse volume. +**No new κ.** The agreement distance `p^{26}` and the ideal gaps stay +hypotheses. The selected record remains `23/10000`. + +## Question + +#4481 leaves the core side `L = 2^{ceil(400 log2 p)}` untouched. HALO compares +the two sparse powers in + +```text +O(V [d/g + d g A^3/L + d A p^2/L] polylog p) +``` + +at `A = p^{48}` and `L ≥ p^{400}`. Both are negative for group exponents +`ε, β < 1`. What is the smallest integer `C` for which `L ≥ p^C` still makes +both powers negative when `A = p^{26}`? + +## Lemma + +Let `A = p^{26}` and let `d = p^ε`, `g = p^β` with real exponents `ε < 1` and +`β < 1`. For an integer `C` and `L ≥ p^C`, the two sparse powers are + +```text +ε + β + 78 - C, ε + 28 - C. +``` + +Both are negative for every such pair if and only if `C ≥ 80`. Thus 80 is +the smallest uniform integer with that property. The same `C = 80` also gives +`p^{80} > 4 p^{26}` for every integer `p ≥ 2`, and `g A/L` has exponent +`27 - 80 < 0` whenever `g ≤ p`. + +The written choice 400 still works, and it is larger than 80. At the corner +`ε = β = 1` its first power would have slack 254. Exponent 79 does not work: +at `ε = β = 3/4` the first power equals `1/2`. + +## Proof + +`A^3 = p^{78}` and `A p^2 = p^{28}`, since `3 · 26 = 78` and `26 + 2 = 28`. +Dividing by `L ≥ p^C` subtracts `C`. + +If `C ≥ 80`, then + +```text +ε + β + 78 - C < 2 + 78 - C = 80 - C ≤ 0, +``` + +and the inequality is strict because `ε + β < 2`. The second power satisfies + +```text +ε + 28 - C < 1 + 28 - 80 = -51 < 0. +``` + +If `C ≤ 79`, the pair `ε = β = 3/4` is strictly below 1 and + +```text +4(3/4 + 3/4 + 78 - 79) = 2 > 0, +``` + +so the first power equals `1/2`. Smaller integers are larger still. The second +power is not the binding one: it is negative for every `ε < 1` as soon as +`C ≥ 29`, and it is already positive at `ε = 1/2` when `C = 28`. + +The corner value of the first power is `80 - C`. It is strictly negative at +`C = 80`, and it is at most `-1` for every pair only when `C ≥ 81`. So 80 +does not reproduce the uniform slack that 400 has at `A = p^{48}`. + +For the two side conditions in the same paragraph, `p^{80} / (4 p^{26}) = p^{54} / 4` +and `2^{10} > 4`, so the ratio is greater than 1 for every integer `p ≥ 2`. +For `g ≤ p` the enlargement exponent is `1 + 26 - 80 = -53`. + +The older arithmetic is the same shape: `3 · 48 = 144` and `2 + 144 = 146`, +so `400 - 146 = 254`. + +## Not covered + +- A proof that the agreement distance is `p^{26}` for every prime. This + comparison uses that distance as the value of `A`. +- The tensor error `g p^{10 g} exp(-p^2)`. The volume exponent does not + change that factor. +- Replacing the written core side in the #4100 notes. +- Any new κ. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/gaussian-core-side --check-only +python3.12 -B scripts/research_package.py --package research/gaussian-core-side +``` + +Base `2a13eb1827784206202db90e5dc8327cf8a250db`, priority revision 7, selection +refresh κ = `23/10000`. + +Overlap on 2026-10-22, from the snapshot fetched at 00:47 UTC, matched this +draft, the #4481 handoff, the locality audit that keeps side 400, and the +union-head note that cites the same core side. It did not find another +assignment of 80. A search miss is not a novelty certificate. #4481 is the +Schur margin. HALO is the volume formula. + +## Open next questions + +1. **Does the tensor error still need the factor `p^{10 g}`?** The volume + side can use `C = 80`, while the core error is still written as + `g p^{10 g} exp(-p^2)`. The first step is to replace `p^{10}` by the + inverse ceiling `10 p^2` and check whether `g log p = o(p)` still leaves + the error below `2^{-C p}` for every fixed `C`. + +## Credit + +- The volume formula and the written side 400 are #4100's. +- The agreement distance `p^{26}` is the conditional halo exponent from #4452 + and #4481. +- The question is the open step of #4481. + +Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0. diff --git a/research/gaussian-core-side/SOURCES.json b/research/gaussian-core-side/SOURCES.json new file mode 100644 index 000000000..e05a8e46a --- /dev/null +++ b/research/gaussian-core-side/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + }, + { + "path": "research/unconditional-batched-crt/HALO.md", + "usage": "input", + "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b", + "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc" + } + ] +} diff --git a/research/gaussian-core-side/TASK.json b/research/gaussian-core-side/TASK.json new file mode 100644 index 000000000..0c24d780c --- /dev/null +++ b/research/gaussian-core-side/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": "Name the smallest integer C such that both sparse volume powers stay negative for group exponents below 1 when the agreement distance A is p^{26} and the core side is at least p^C.", + "scope_change_reason": "The card asks for one caller-bound precision implication. This package only compares HALO's two sparse powers under that substitution. It does not retune the tensor error and does not claim a new kappa.", + "bottleneck_link": "The selected frontier is unchanged. The core side is the volume input that HALO compares with the agreement distance.", + "budget_minutes": 60, + "stop_rule": "Stop once 80 is compared with 79 and with the written 400. Do not retune p^{10 g}, 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-core-side", + "author": "James Reed", + "ai_assistance": "Substantial help from Cursor Grok 4.7 on the exponent comparison and the package text.", + "open_questions": [ + { + "question": "Does the core tensor error still need the factor p^{10 g} once the inverse ceiling is 10 p^2?", + "why_it_matters": "The volume side can use core exponent 80, while the written error is still g p^{10 g} exp(-p^2).", + "first_step": "Replace p^{10} by 10 p^2 and check whether g log p = o(p) still puts the error below 2^{-C p} for every fixed C.", + "blocked_by": "The agreement distance p^{26} and the ideal gaps remain hypotheses, so the core side is still conditional." + } + ] +} diff --git a/research/gaussian-core-side/VERIFY.json b/research/gaussian-core-side/VERIFY.json new file mode 100644 index 000000000..a77c00df5 --- /dev/null +++ b/research/gaussian-core-side/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/HALO.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "With A = p^{26} both sparse powers are negative for every group exponent below 1 precisely when the core side exponent is at least 80; 79 fails at 3/4 and the written 400 is larger." + } + ] +} diff --git a/research/gaussian-core-side/verify.py b/research/gaussian-core-side/verify.py new file mode 100644 index 000000000..db9be3233 --- /dev/null +++ b/research/gaussian-core-side/verify.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +"""Smallest core-side exponent once the agreement distance is p^26. + +Every comparison is an integer identity. The ideal gaps stay hypotheses. +""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "gaussian-core-side" + + +def digest(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +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") + gaussian = (ROOT / "research/unconditional-batched-crt/GAUSSIAN.md").read_text( + encoding="utf-8" + ) + selected = json.loads( + (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8") + ) + assert "L=2^ceil(400 log2 p)" in halo + assert "L>4A and gA/L=o(1) for every g<=p" in halo + assert "g p^(10g) exp(-p^2)" in halo + assert "O(V [d/g + d g A^3/L + d A p^2/L] polylog p)." in halo + assert "For A=p^48, L>=p^400" in halo + assert "two sparse powers are epsilon+beta+144-400 and epsilon+48+2-400, both negative." in halo + assert "O(V [d/g + d g A^3/L + d A p^2/L] polylog(p))." in gaussian + assert selected["kappa"] == "23/10000" + + +def powers() -> None: + # A^3 contributes 3*26 = 78, and the p^2 factor contributes 26+2 = 28. + assert 3 * 26 == 78 + assert 26 + 2 == 28 + assert 3 * 48 == 144 + assert 48 + 2 == 50 + # The corner ε = β = 1 would make the first power 80 - C. Strictly below 1, C = 80 is negative. + assert 2 + 78 == 80 + assert 1 + 28 == 29 + assert 29 < 80 + assert 1 + 28 - 80 == -51 + # C = 79 is positive at ε = β = 3/4. Clearing the denominator leaves +2. + assert 3 + 3 + 4 * 78 - 4 * 79 == 2 + assert 3 + 3 + 4 * 78 - 4 * 80 == -2 + # The second power alone already fails at C = 28 for ε = 1/2. + assert 1 + 2 * 28 - 2 * 28 == 1 + # The written 400 still has slack 254 at the same corner, and it is larger than 80. + assert 2 + 144 == 146 + assert 400 - 146 == 254 + assert 400 > 80 + # L >= p^80 also meets L > 4A and gA/L = o(1) for g <= p. + assert 80 - 26 == 54 + assert 2 ** 10 > 4 + assert 54 > 10 + assert 1 + 26 - 80 < 0 + # A uniform slack of 1 below zero needs 81, because the corner reaches 80 - C. + assert 80 - 81 == -1 + + +def main() -> None: + pins_and_phrases() + powers() + print("PASS_GAUSSIAN_CORE_SIDE") + + +if __name__ == "__main__": + main()