From b1fa86ecc00307058cfd324f9d87042c5d951264 Mon Sep 17 00:00:00 2001 From: James Reed Date: Wed, 21 Oct 2026 09:51:10 -0700 Subject: [PATCH] Record the smaller halo exponents available under the ceiling 16 p^2. Co-authored-by: Cursor --- research/gaussian-halo-exponents/README.md | 123 ++++++++++++++ research/gaussian-halo-exponents/SOURCES.json | 42 +++++ research/gaussian-halo-exponents/TASK.json | 74 +++++++++ research/gaussian-halo-exponents/VERIFY.json | 24 +++ research/gaussian-halo-exponents/verify.py | 153 ++++++++++++++++++ 5 files changed, 416 insertions(+) create mode 100644 research/gaussian-halo-exponents/README.md create mode 100644 research/gaussian-halo-exponents/SOURCES.json create mode 100644 research/gaussian-halo-exponents/TASK.json create mode 100644 research/gaussian-halo-exponents/VERIFY.json create mode 100644 research/gaussian-halo-exponents/verify.py diff --git a/research/gaussian-halo-exponents/README.md b/research/gaussian-halo-exponents/README.md new file mode 100644 index 0000000000..4f70baafa9 --- /dev/null +++ b/research/gaussian-halo-exponents/README.md @@ -0,0 +1,123 @@ +# HALO's exponents can fall under the ceiling 16 p^2 + +**Conditional exponent arithmetic for #4100's locality witness. No new κ.** +This answers the open question of #4403. It does not prove the ceiling for +`GAUSSIAN.md`'s rounded reference `H`, and it does not edit the #4100 notes. + +## Question + +#4403 showed that the written `p^10` guards need not increase. The remaining +arithmetic question is the other direction. Suppose, for an integer `p >= 2`, + +```text +||H||_2 <= 16 p^2, ||H^-1||_2 <= 16 p^2, +``` + +and the physical bandwidth `W` is an integer at most `p-1`. Which of HALO's +exponents 20, 42, 45 and 48, and GAUSSIAN's normalizer 100, can decrease +while the error and the row-exactness conclusions stay in force? + +The ceiling `16 p^2` is `1/sqrt(delta delta_col)` when both gaps are at least +`1/(16 p^2)`. That gap for the rounded matrix is not proved here. + +## Result + +The same polynomial `P = p^-12 sum_{j < p^26} Q^j H*`, with +`Q = I - p^-12 H* H`, satisfies + +```text +||P - H^-1||_2 < p^6 exp(-p^2), +``` + +and every row whose distance to a section edge is at least `p^28` equals the +global row. The normalizer `p^7`, or the dyadic factor `2^ceil(7 log2 p)`, +puts a factor at most `16 p^2` strictly below one. + +| Written exponent | Smallest uniform replacement | Why it is smallest | +| --- | ---: | --- | +| 20, the spectral endpoint | 12 | `(16 p^2)^2 = 256 p^4 <= p^12`, and `256 p^4 > p^11` at `p = 2` | +| 40, the gap inside `Q` | 24 | `p^-12 * p^-12 = p^-24`, and the `p = 2` case is equality | +| 42, the length `J` | 26 | `p^26 p^-24 = p^2`, while `p^25` leaves only `p` | +| 10, the error multiplier | 6 | `16 p^2 <= p^6`, and `16 p^2 > p^5` at `p = 2` | +| 45, the bandwidth | 28 | `(2J-1)W` and `(2J+1)W` are both below `p^28` and not below `p^27` | +| 48, the halo distance | 28 | `p^28` already exceeds the sharp radius `(2J-1)W` | +| 100, the normalizer | 7 | `p^7 > 16 p^2`, while `p^6 = 16 p^2` at `p = 2` | + +So 20, 42, 45, 48 and 100 can all decrease. The replacements are 12, 26, 28, +28 and 7. + +## Proof + +`16 p^2 <= p^6` because `p^4 - 16 = (p-2)(p+2)(p^2+4)`, which is zero at +`p = 2` and positive after that. Squaring gives the spectral interval +`[p^-12, p^12]` for `H* H`. The scalar `p^-12` is therefore an admissible +step: `Q` is Hermitian with eigenvalues in `[0, 1-p^-24]`. + +The truncation identity in the halo audit is unchanged in shape, + +```text +P - H^-1 = -Q^J H^-1. +``` + +Hence the error is at most `(1-p^-24)^J` times `16 p^2`. For `x` in `(0, 1)`, +`exp(x) = sum x^k/k! <= sum x^k = 1/(1-x)`, so `(1-x)^J <= exp(-J x)`. +At `J = p^26` the product `J p^-24` equals `p^2`, and `1/2! < 1` makes the +exponential comparison strict. The multiplier `16 p^2` is at most `p^6`. + +`H*` has bandwidth `W` and `Q` has bandwidth `2W`, so `Q^j H*` has bandwidth +`(2j+1)W`. The longest term is `j = J-1`, radius `(2J-1)W`. This is the sharp +radius from the halo audit. With `J = p^26` and `W <= p-1`, + +```text +p^28 - (2 p^26 - 1)(p-1) = p^26 ((p-1)^2 + 1) + p - 1 > 0. +``` + +The looser HALO expression `(2J+1)W` has the same uniform ceiling. For every +integer `p >= 3` the sharp radius is at least `p^27 + 1`, and at `p = 2` the +looser expression is `p^27 + 1`. Exponent 27 is therefore not enough. +`A = p^28` lies strictly beyond the radius, which is the row-exactness claim. + +Dividing by `p^7` is strict because `p^5 >= 32 > 16`. Dividing by `p^6` leaves +the `p = 2` corner at one, not below one. Any dyadic factor at least `p^7` +has the same strictness. That is `2^ceil(7 log2 p)`. + +The written core exponent 400 still dominates `4A`. It can itself fall to 86: +`p^86 > 4 p^28`, and for every `epsilon, beta < 1` both +`epsilon + beta + 84 - 86` and `epsilon + 30 - 86` stay negative. Exponent 85 +does not, since `epsilon + beta + 84 - 85` is positive for `epsilon = beta = 3/4`. +FINE-PRIME's core exponent 128 likewise still covers a halo exponent of 28. +This package does not retune the core. + +## What this does not say + +- It does not prove `||H^-1||_2 <= 16 p^2` for the rounded reference. Phase + cuts, truncation and rounding remain open, as in #4402. +- The #4100 notes keep 20, 42, 45, 48 and 100. Those values remain sufficient. + The smaller ones are available only under the stronger ceiling. +- The selected κ is unchanged: + `836330098538459/500000000000000000`. +- Upstream pin: main `12fa8c5c844be21bfefb38a19503fbd867a11244`, priority + revision 7, checked 2026-10-21T16:44:38Z. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/gaussian-halo-exponents +``` + +## Open next questions + +Do these smaller exponents hold for `GAUSSIAN.md`'s rounded reference `H`? +Only a column gap after phase cuts, truncation and rounding would put +`||H^-1||_2` under `16 p^2`. Until that transfer exists, HALO's written +exponents stay the ones the construction may use. + +## Credit + +The locality witness and its exponents are #4100's. The sharp radius +`(2J-1)W` is the halo audit's, PR #4217 (Nick Petalas). The ceiling +`16 p^2` is the conditional bound from #4403, which answered #4402's +guard question. The kernel comes from PR1673 (Vlado Vojdanovski). + +Prepared by James Reed with substantial Cursor Grok 4.7 assistance. No +independent human review. Apache-2.0. diff --git a/research/gaussian-halo-exponents/SOURCES.json b/research/gaussian-halo-exponents/SOURCES.json new file mode 100644 index 0000000000..9d39b6ebb5 --- /dev/null +++ b/research/gaussian-halo-exponents/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "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" + }, + { + "path": "research/unconditional-batched-crt/PROOF.md", + "usage": "input", + "git_blob": "406eb561cc8d6041ea3fba1a849653b654f2198c", + "sha256": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060" + }, + { + "path": "research/unconditional-batched-crt/vendor/FINE-PRIME.md", + "usage": "input", + "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3", + "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce" + } + ] +} diff --git a/research/gaussian-halo-exponents/TASK.json b/research/gaussian-halo-exponents/TASK.json new file mode 100644 index 0000000000..2e574e4cbb --- /dev/null +++ b/research/gaussian-halo-exponents/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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": "Under the hypothesis that both 2-norms are at most 16 p^2, find which of HALO's exponents 20, 42, 45 and 48, and GAUSSIAN's normalizer 100, can decrease while the error and row-exactness conclusions remain in force.", + "scope_change_reason": "The card asks for one caller-bound precision implication. This package only recomputes HALO's polynomial-locality exponents under the stronger ceiling. It does not prove that ceiling for the rounded matrix H.", + "bottleneck_link": "The selected frontier is unchanged. Smaller halo exponents would matter only after the column-gap ceiling transfers to the rounded reference.", + "budget_minutes": 60, + "stop_rule": "Stop once each asked exponent has a smallest uniform replacement. Do not prove the column gap for H, 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-halo-exponents", + "author": "James Reed", + "ai_assistance": "Substantial help from Cursor Grok 4.7 on the exponent arithmetic, the minimality checks and the package text.", + "open_questions": [ + { + "question": "Do the smaller exponents 12, 26, 28, 28 and 7 hold for GAUSSIAN.md's rounded reference H?", + "why_it_matters": "HALO may use them only when both 2-norms of that rounded matrix are at most 16 p^2. The written exponents stay sufficient without that transfer.", + "first_step": "Bound the column sums of the rounded reference across a phase cut, then repeat the row-side truncation and rounding argument for columns.", + "blocked_by": "The exact cross-cut entry definition in the PR1673/PR1758 sources, the same blocker #4402 recorded." + } + ] +} diff --git a/research/gaussian-halo-exponents/VERIFY.json b/research/gaussian-halo-exponents/VERIFY.json new file mode 100644 index 0000000000..bf1ea93de4 --- /dev/null +++ b/research/gaussian-halo-exponents/VERIFY.json @@ -0,0 +1,24 @@ +{ + "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", + "research/unconditional-batched-crt/PROOF.md", + "research/unconditional-batched-crt/vendor/FINE-PRIME.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Old exponents still present; 12, 26, 28 and 7 suffice; 11, 25, 27 and 6 do not." + } + ] +} diff --git a/research/gaussian-halo-exponents/verify.py b/research/gaussian-halo-exponents/verify.py new file mode 100644 index 0000000000..f1f34121eb --- /dev/null +++ b/research/gaussian-halo-exponents/verify.py @@ -0,0 +1,153 @@ +#!/usr/bin/env python3 +"""Smallest uniform halo exponents under the ceiling 16 p^2. + +The argument is HALO.md's, with p^10 replaced by 16 p^2. Every comparison +is an integer identity. It does not prove that ceiling for the rounded +matrix H. +""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "gaussian-halo-exponents" +NOTES = ROOT / "research" / "unconditional-batched-crt" + + +def digest(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def pins_match() -> 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"] + + +def notes_still_use_the_old_exponents() -> None: + halo = (NOTES / "HALO.md").read_text(encoding="utf-8") + gaussian = (NOTES / "GAUSSIAN.md").read_text(encoding="utf-8") + fine = (NOTES / "vendor" / "FINE-PRIME.md").read_text(encoding="utf-8") + proof = (NOTES / "PROOF.md").read_text(encoding="utf-8") + assert "2-norm at most p^10 and inverse\n2-norm at most p^10" in halo + assert "Q_i=I-p^-20 H_i^* H_i and J=ceil(p^42)" in halo + assert "bandwidth <=(2J+1)W=p^400" in halo + assert "bandwidth dict[int, int]: + out: dict[int, int] = {} + for degree, coeff in left.items(): + for other, factor in right.items(): + key = degree + other + out[key] = out.get(key, 0) + coeff * factor + return {key: value for key, value in out.items() if value} + + +def exponents() -> None: + # 16 p^2 <= p^6, with equality at p=2, because p^4 - 16 = (p^2-4)(p^2+4) + # and p^2-4 = (p-2)(p+2). + assert sparse_mul({2: 1, 0: -4}, {2: 1, 0: 4}) == {4: 1, 0: -16} + assert sparse_mul({1: 1, 0: -2}, {1: 1, 0: 2}) == {2: 1, 0: -4} + # p=2 makes every factor on the right of (p-2) zero, so equality. + # p^5 does not cover 16 p^2: 64 > 32. + assert 16 * 2 * 2 == 64 > 32 == 2**5 + # Strict normalizer: p^7 - 16 p^2 = p^2 (p^5 - 16) and p^5 >= 32 > 16. + assert 2**5 == 32 > 16 + # p^6 meets 16 p^2 at p=2, so division by p^6 is not strictly below one. + assert 2**6 == 64 == 16 * 2 * 2 + + # Spectral exponent. (16 p^2)^2 = 256 p^4 <= p^12 iff p^8 >= 256. + # p^8 - 256 = (p^4 - 16)(p^4 + 16), and p^4 - 16 >= 0 as above. + assert sparse_mul({4: 1, 0: -16}, {4: 1, 0: 16}) == {8: 1, 0: -256} + assert 256 == 2**8 + # Exponent 11 fails at p=2: p^7 = 128 < 256. + assert 2**7 == 128 < 256 + + # Q = I - p^-12 H* H then has spectrum in [0, 1 - p^-24]. + # J = p^26 gives J p^-24 = p^2, so (1 - p^-24)^J <= exp(-p^2) + # by exp(x) = sum x^k/k! <= sum x^k = 1/(1-x) for x in (0, 1). + assert 26 - 24 == 2 + assert 25 - 24 == 1 + # The series bound is strict for x>0 because 1/2! < 1. + assert 1 / 2 < 1 + + # Sharp radius (2 p^26 - 1)(p - 1) = 2 p^27 - 2 p^26 - p + 1. + sharp = sparse_mul({26: 2, 0: -1}, {1: 1, 0: -1}) + assert sharp == {27: 2, 26: -2, 1: -1, 0: 1} + # p^28 - sharp = p^26 ((p-1)^2 + 1) + p - 1. + quadratic = sparse_mul({1: 1, 0: -1}, {1: 1, 0: -1}) + quadratic[0] = quadratic.get(0, 0) + 1 + assert quadratic == {2: 1, 1: -2, 0: 2} + margin = sparse_mul({26: 1}, quadratic) + margin[1] = margin.get(1, 0) + 1 + margin[0] = margin.get(0, 0) - 1 + assert margin == {28: 1, 27: -2, 26: 2, 1: 1, 0: -1} + # (p-1)^2 + 1 >= 2 for integer p >= 2, so the margin is at least + # 2 p^26 + p - 1 > 0. Exponent 28 covers the sharp radius. + # Exponent 27 does not for p >= 3: sharp - p^27 = p^26 (p-2) - p + 1 + # >= p^26 - p + 1 >= 1. + excess = dict(sharp) + excess[27] = excess.get(27, 0) - 1 + assert excess == {27: 1, 26: -2, 1: -1, 0: 1} + reduced = sparse_mul({26: 1}, {1: 1, 0: -2}) + reduced[1] = reduced.get(1, 0) - 1 + reduced[0] = reduced.get(0, 0) + 1 + assert reduced == excess + + # HALO's looser (2 p^26 + 1)(p - 1) is still below p^28, and above p^27 + # already at p=2. + loose = sparse_mul({26: 2, 0: 1}, {1: 1, 0: -1}) + assert loose == {27: 2, 26: -2, 1: 1, 0: -1} + loose_margin = {28: 1} + for degree, coeff in loose.items(): + loose_margin[degree] = loose_margin.get(degree, 0) - coeff + assert loose_margin == {28: 1, 27: -2, 26: 2, 1: -1, 0: 1} + loose_excess = dict(loose) + loose_excess[27] = loose_excess.get(27, 0) - 1 + assert loose_excess == {27: 1, 26: -2, 1: 1, 0: -1} + # At p=2 this excess is 2^26 * 0 + 2 - 1 = 1, so the loose radius + # bound is p^27 + 1. + assert 2**26 * 0 + 2 - 1 == 1 + + # Core exponent 86 keeps L >= p^86 > 4 p^28 and both sparse powers + # negative for every epsilon, beta < 1. Exponent 85 does not. + assert 86 - 28 >= 1 and 2**58 > 4 + assert 84 - 86 == -2 # epsilon + beta + 84 - 86 < 0 + assert 85 - 84 == 1 # epsilon + beta - 1 can be positive + assert 28 + 2 - 86 < 0 + + +def main() -> None: + pins_match() + notes_still_use_the_old_exponents() + exponents() + print("halo exponents 20,42,45,48,100 can fall to 12,26,28,28,7") + + +if __name__ == "__main__": + main()