Lower the core side exponent from 400 to 80 (no new κ)

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.

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

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

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

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()