HALO exponents 20, 42, 45, 48 and the normalizer 100 can fall under the ceiling 16 p^2 (no new κ)

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.

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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."
+    }
+  ]
+}