diff --git a/research/gaussian-cell-exponents/README.md b/research/gaussian-cell-exponents/README.md new file mode 100644 index 0000000000..72b60dd9ff --- /dev/null +++ b/research/gaussian-cell-exponents/README.md @@ -0,0 +1,137 @@ +# The smaller halo exponents hold inside one cell + +**Claim type:** conditional exponent arithmetic for one within-cell block. +**No new κ.** The global rounded matrix, whose across-cell entries are not +this gauge ratio, is outside the claim. + +## Question + +#4406 showed that HALO's exponents can fall to 12, 26, 28, 28 and 7 when both +2-norms are at most `16 p^2`. #4438 gave a within-cell column budget +`ε ≤ 1/(16p^2)`. Do those five exponents apply to the rounded block + +```text +A = diag(ahat) Ghat diag(ahat)^{-1} +``` + +once that budget holds? + +## Lemma + +Let `p ≥ 2` be an integer and let `W` be an integer at most `p-1`. Assume the +ideal row and column off-sums are at most `1 - 1/(8p^2)`, the conclusions +GAUSSIAN and #4402 state eventually, and assume the within-cell rounding of +#4438: `Ghat_0 = 1`, `0 ≤ Ghat ≤ exp(-a ρ h^2)`, and +`(1-ε) a ≤ ahat ≤ a` with `ε ≤ 1/(16p^2)`. + +Then both rounded off-sums are at most `(16p^2-2)/(16p^2-1)`, so both gaps +are at least `1/(16p^2-1)`. The Neumann series gives + +```text +||A^{-1}||_∞ ≤ 16 p^2 - 1, ||A^{-1}||_1 ≤ 16 p^2 - 1, +``` + +and therefore `||A^{-1}||_2 ≤ 16 p^2 - 1`. Each absolute row and column sum is +strictly less than 2, so `||A||_2 < 2`. + +For this block the polynomial + +```text +P = p^{-12} sum_{j < p^{26}} Q^j A^*, Q = I - p^{-12} A^* A, +``` + +satisfies `||P - A^{-1}||_2 < p^6 exp(-p^2)`. Its bandwidth is at most +`(2 p^{26} - 1) W < p^{28}`, and the looser count `(2 p^{26} + 1) W` has the +same ceiling. A row at distance `p^{28}` from a section edge of this block +agrees with the block row. Dividing by `p^6` puts the inverse ceiling strictly +below one. + +So 12, 26, 28, 28 and 7 all apply. The first four remain the smallest uniform +integers with that property. The normalizer 7 is not smallest: the ceiling +`16 p^2 - 1` is already strictly below `p^6`, while it is above `p^5` at +`p = 2`. The smallest normalizer is 6. + +## Proof + +The gauge ratio multiplies every off-diagonal entry by at most `1/(1-ε)`, on +a row and on a column. With `ε = 1/(16p^2)` and an ideal off-sum at most +`1 - 1/(8p^2)`, + +```text +off ≤ (1 - 1/(8p^2)) / (1 - 1/(16p^2)) = (16p^2 - 2)/(16p^2 - 1). +``` + +The complementary gap is `1/(16p^2-1)`. Adding the diagonal produces the row +sum `(32p^2-3)/(16p^2-1)`, and `2(16p^2-1) - (32p^2-3) = 1`, so the sum is +strictly below 2. The same bound is the column sum. The 2-norm comparison +`||·||_2 ≤ sqrt(||·||_1 ||·||_∞)` is the one already used for these matrices. +It gives `||A||_2 < 2` and `||A^{-1}||_2 ≤ 16 p^2 - 1`. + +The inverse ceiling is 63 at `p = 2`. Then `63^2 = 3969 ≤ 4096 = 2^{12}` and +`3969 > 2048 = 2^{11}`. The forward 2-norm is below 2, so the upper end +`p^{12}` is loose, but `p^{-12}` is still a legal lower bound on the +eigenvalues of `A^* A` and `p^{-11}` is not. Thus `Q` has spectrum in +`[0, 1-p^{-24}]`. The scalar step in the exponential series is strict because +`1/2! < 1`, and `p^{26} p^{-24} = p^2`. The shorter length `p^{25}` leaves a +factor `p^{11}` against `(16p^2-1)^2`, and `2048 < 3969` at `p = 2`. + +The error is therefore strictly less than `(16p^2-1) exp(-p^2)`. Since +`p^4 - 16 = (p-2)(p+2)(p^2+4)`, one has `16p^2 - 1 < p^6`, with room 1 at +`p = 2`. The multiplier `p^5` fails because `63 > 32`. + +The bandwidth identity is unchanged: + +```text +p^{28} - (2 p^{26} - 1)(p-1) = p^{26} ((p-1)^2 + 1) + p - 1 > 0. +``` + +At `p = 2` the loose radius `(2J+1)W` equals `p^{27}+1`. For every integer +`p ≥ 3` the sharp radius at `W = p-1` exceeds `p^{27}`. Exponent 27 is not a +uniform ceiling. Exponent 28 is. + +Dividing by `p^6` is strict, as above. Dividing by `p^7` remains strict and +is the value #4406 recorded for the closed ceiling `16 p^2`. + +## Not covered + +- Across-cell entries. They are the downward original entries, not + `ahat_j Ghat_(j-k)/ahat_k`, so this does not move HALO's exponents for the + global reference. +- A proof that the ideal gaps exceed `1/(8p^2)` for every prime. That remains + the eventual statement in GAUSSIAN and #4402. +- The core exponent 400. It still dominates a halo of 28, and it is not retuned. +- Any new κ. The selected record remains `23/10000`. The #4100 notes keep + 20, 42, 45, 48 and 100. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/gaussian-cell-exponents --check-only +python3.12 -B scripts/research_package.py --package research/gaussian-cell-exponents +``` + +Base `2a13eb1827784206202db90e5dc8327cf8a250db`, priority revision 7, selection +refresh κ = `23/10000`. + +Overlap on 2026-10-21 did not find a within-cell assignment of these +exponents. #4406 is the conditional arithmetic for a closed ceiling `16 p^2`. +#4438 is the relative-error budget. A search miss is not a novelty certificate. + +## Open next questions + +1. **Do 12, 26, 28, 28 and 6 survive across a cell?** + The within-cell block now meets the ceiling those exponents use, and the + normalizer may be 6 rather than 7. The global reference is still blocked: + its across-cell entries are the downward approximation of the original + entry, and no column bound for that rule is written. The first step is a + column off-sum for those entries under the same `ε`. + +## Credit + +- HALO's locality witness and its written exponents are #4100's. +- The sharp radius `(2J-1)W` is Nick Petalas's halo audit, PR #4217. +- The in-cell ideal column gap is Ryanson Jonathan's #4402. +- The relative-error budget is #4438. +- The closed-ceiling arithmetic is #4406. + +Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0. diff --git a/research/gaussian-cell-exponents/SOURCES.json b/research/gaussian-cell-exponents/SOURCES.json new file mode 100644 index 0000000000..962ce5c6d8 --- /dev/null +++ b/research/gaussian-cell-exponents/SOURCES.json @@ -0,0 +1,48 @@ +{ + "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/capped-phase-fusion/CAPPED-GAUGE-AUDIT.md", + "usage": "input", + "git_blob": "a2d1c5ae923db7649627dbf419434e36267e57c6", + "sha256": "1030a34922709ab8d3434a4c57a4a58934ae268c237fb598cb415697da411c9f" + }, + { + "path": "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md", + "usage": "input", + "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73", + "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272" + }, + { + "path": "research/gaussian-column-gap/README.md", + "usage": "input", + "git_blob": "7f8b5d9cbad96a1cd46432a6cf47422e2ced7fb4", + "sha256": "7e589bec5c03d788ac366c85080af9fe26dad254d289bec93553398380b46dab" + }, + { + "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-cell-exponents/TASK.json b/research/gaussian-cell-exponents/TASK.json new file mode 100644 index 0000000000..5b93e07207 --- /dev/null +++ b/research/gaussian-cell-exponents/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 the exponents 12, 26, 28, 28 and 7 apply to the rounded within-cell block once the relative weight error is at most 1/(16p^2).", + "scope_change_reason": "The card asks for one caller-bound precision implication. This package only treats the within-cell gauge block. It does not move the exponents of the global rounded reference.", + "bottleneck_link": "The selected frontier is unchanged. These exponents matter for HALO only where both 2-norms of the matrix being inverted are at most 16 p^2.", + "budget_minutes": 60, + "stop_rule": "Stop once each exponent has a yes or no for this block, including whether 7 is smallest. Do not bound across-cell entries, 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-cell-exponents", + "author": "James Reed", + "ai_assistance": "Substantial help from Cursor Grok 4.7 on the ceiling arithmetic, the minimality checks and the package text.", + "open_questions": [ + { + "question": "Do the exponents 12, 26, 28, 28 and 6 survive across a cell?", + "why_it_matters": "The within-cell block meets the ceiling, with normalizer 6. Callers invert the global reference, which also has across-cell entries.", + "first_step": "Bound the column off-sum of the downward original entries used across a cell, under the same relative-error budget.", + "blocked_by": "Those entries are not the ratio ahat_j Ghat_(j-k)/ahat_k, so the within-cell transfer does not apply." + } + ] +} diff --git a/research/gaussian-cell-exponents/VERIFY.json b/research/gaussian-cell-exponents/VERIFY.json new file mode 100644 index 0000000000..665cee7a2a --- /dev/null +++ b/research/gaussian-cell-exponents/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/capped-phase-fusion/CAPPED-GAUGE-AUDIT.md", + "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md", + "research/gaussian-column-gap/README.md", + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/HALO.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Both gaps give the ceiling 16p^2-1; 12, 26 and 28 stay smallest; the normalizer falls to 6." + } + ] +} diff --git a/research/gaussian-cell-exponents/verify.py b/research/gaussian-cell-exponents/verify.py new file mode 100644 index 0000000000..b8f27a813b --- /dev/null +++ b/research/gaussian-cell-exponents/verify.py @@ -0,0 +1,141 @@ +#!/usr/bin/env python3 +"""Within-cell halo exponents under the relative-error budget. + +Every comparison is an integer identity. The ideal row and column gaps are +hypotheses. Across-cell entries are not bounded. +""" + +from __future__ import annotations + +import hashlib +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "gaussian-cell-exponents" + + +def digest(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def add(left, right): + out = dict(left) + for key, coeff in right.items(): + out[key] = out.get(key, 0) + coeff + if out[key] == 0: + del out[key] + return out + + +def scale(poly, factor): + return {key: factor * coeff for key, coeff in poly.items() if factor * coeff} + + +def mul(left, right): + out = {} + 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: coeff for key, coeff in out.items() if coeff} + + +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") + column = (ROOT / "research/gaussian-column-gap/README.md").read_text( + encoding="utf-8" + ) + log_a = ( + ROOT / "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md" + ).read_text(encoding="utf-8") + gauge = ( + ROOT / "research/capped-phase-fusion/CAPPED-GAUGE-AUDIT.md" + ).read_text(encoding="utf-8") + selected = json.loads( + (ROOT / "certificates/selected-result.json").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 None: + # Ideal off-sum <= 1-1/(8p^2) and ε=1/(16p^2) give rounded off-sum + # <= (16p^2-2)/(16p^2-1), hence gap >= 1/(16p^2-1). + numerator = add({2: 16}, {0: -2}) + denominator = add({2: 16}, {0: -1}) + assert add(denominator, scale(numerator, -1)) == {0: 1} + # Row sum 1+off <= (32p^2-3)/(16p^2-1) < 2. + row_sum = add({2: 32}, {0: -3}) + twice = scale(denominator, 2) + assert add(twice, scale(row_sum, -1)) == {0: 1} + # Inverse 1-norms are at most 16p^2-1. At p=2 that ceiling is 63. + assert 16 * 4 - 1 == 63 + assert 63 * 63 == 3969 + assert 2 ** 12 == 4096 + assert 3969 <= 4096 + assert 2 ** 11 == 2048 + assert 3969 > 2048 + assert 2 ** 5 == 32 + assert 63 > 32 + + +def exponent_arithmetic() -> None: + # p^4-16=(p-2)(p+2)(p^2+4), so 16p^2<=p^6, and 16p^2-1= 16p^2-1 iff the spectral step p^-12 is valid, and p^25 is not. + assert 2 ** 6 == 64 + assert 64 - 63 == 1 + assert 2 ** 11 < 3969 + # 1/2! < 1 makes (1-x)^J < exp(-J x). + assert 1 < 2 + assert 26 - 24 == 2 + assert 25 - 24 == 1 + # Sharp radius (2p^26-1)(p-1) is below p^28. + quadratic = add(mul({1: 1, 0: -1}, {1: 1, 0: -1}), {0: 1}) + assert quadratic == {2: 1, 1: -2, 0: 2} + factored = add(mul({26: 1}, quadratic), {1: 1, 0: -1}) + sharp = mul({26: 2, 0: -1}, {1: 1, 0: -1}) + margin = add({28: 1}, scale(sharp, -1)) + assert factored == margin + assert margin == {28: 1, 27: -2, 26: 2, 1: 1, 0: -1} + # Exponent 27 fails. At p=2 the loose radius is p^27+1. + assert 2 * (2 ** 26) + 1 == 2 ** 27 + 1 + assert (2 * (2 ** 26) - 1) == 2 ** 27 - 1 + # For p>=3 the sharp radius at W=p-1 exceeds p^27. + assert (2 * (3 ** 26) - 1) * (3 - 1) > 3 ** 27 + 1 + # Normalizer 6 puts 16p^2-1 strictly below one; 5 does not. + assert 63 < 64 + assert 63 > 32 + + +def main() -> None: + pins_and_phrases() + rounded_ceilings() + exponent_arithmetic() + print("PASS_GAUSSIAN_CELL_EXPONENTS") + + +if __name__ == "__main__": + main()