Record that the written global tail is p^10 exp(-p^2) (no new κ)

research/gaussian-global-tail/README.md

@@ -0,0 +1,116 @@
+# The written global tail is p^{10} exp(-p^2)
+
+**Claim type:** a comparison of three tail statements.
+**No new κ.** The ideal-gap gauge stays a hypothesis. The selected record
+remains `23/10000`.
+
+## Question
+
+#4520 asks whether `||P_glob - C_i||_2` is below `p^6 exp(-p^2)`, or only
+the written `p^{10} exp(-p^2)`. The named step is to compare the identity
+`P - H^{-1} = -Q^J H^{-1}` with the within-cell `p^6` bound, and not to put
+`p^{10}` into the gate yet.
+
+## Lemma
+
+Under HALO's written hypotheses, the global majorant is
+`p^{10} exp(-p^2)`. It is not the within-cell bound `p^6 exp(-p^2)`.
+
+1. **The identity keeps the inverse factor.** The locality audit records
+
+```text
+P - H^{-1} = -Q^J H^{-1},
+||P - H^{-1}||_2 ≤ (1 - p^{-40})^J p^{10} ≤ p^{10} exp(-p^2).
+```
+
+For an integer `p`, `J = ceil(p^{42}) = p^{42}`, so `J p^{-40} = p^2`.
+That power fills the `exp(-p^2)` slot. It does not cancel any power of the
+inverse factor. HALO states the same majorant,
+`||P_i - H_i^{-1}||_2 ≤ p^{10} exp(-p^2)`.
+
+2. **The written majorant is larger than `p^6 exp(-p^2)` by `p^4`.**
+Since `10 - 6 = 4` and `p^4 ≥ 16 > 1` for every integer `p ≥ 2`,
+
+```text
+p^{10} exp(-p^2) = p^4 · p^6 exp(-p^2) > p^6 exp(-p^2).
+```
+
+The truncation exponent `2` and the leftover exponent `4` are different.
+The series length does not turn the written majorant into the smaller one.
+
+3. **The within-cell `p^6` bound is a different polynomial.** #4452 proves
+`||P - A^{-1}||_2 < p^6 exp(-p^2)` for
+`P = p^{-11} sum_{j < p^{24}} Q^j A^*` inside one cell, under the ideal-gap
+gauge. That package does not move the global reference.
+
+4. **The conditional `p^6` bound is not the written hypothesis.** #4406
+proves `||P - H^{-1}||_2 < p^6 exp(-p^2)` for
+`P = p^{-12} sum_{j < p^{26}} Q^j H^*`, and only if
+`||H^{-1}||_2 ≤ 16 p^2`. It does not prove that ceiling for the rounded
+reference. At `p = 2`, `16 p^2 = p^6`. For `p ≥ 3`, `16 p^2 < p^6`.
+Equality at `p = 2` means the ceiling `16 p^2` is not by itself a strict
+`p^6` bound.
+
+This package does not put `p^{10}` into the #4520 gate.
+
+## Proof
+
+The audit derives the displayed identity from
+`p^{-20} (I - Q)^{-1} H^* = H^{-1}` and commutation of `Q` with `H^* H`.
+The factor `p^{10}` is the hypothesis `||H^{-1}||_2 ≤ p^{10}`. Multiplying
+by `(1 - p^{-40})^J` and using `J p^{-40} = p^2` produces the written
+majorant. Replacing `p^{10}` by `p^6` in that product would require
+`||H^{-1}||_2 ≤ p^6`, which is not HALO's hypothesis.
+
+The integer comparison is `2^{10} = 2^6 · 2^4` and `2^4 > 1`. The same
+gap is `p^4` at every larger integer `p`. The conditional ceiling meets
+`p^6` at `p = 2` and is smaller at `p = 3`, where `16 · 9 < 3^6`.
+
+## Not covered
+
+- A proof that `||H^{-1}||_2 ≤ p^{10}` or `||H^{-1}||_2 ≤ 16 p^2` for the
+  rounded reference. Both remain hypotheses of the packages that use them.
+- The ideal-gap gauge behind the within-cell bound.
+- Absorbing `p^{10}` in the restricted gate.
+- Editing the #4100 notes. They still say `p^{10} exp(-p^2)`.
+- Any new κ.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/gaussian-global-tail --check-only
+python3.12 -B scripts/research_package.py --package research/gaussian-global-tail
+```
+
+Base `f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc`, priority revision 7, selection
+refresh κ = `23/10000`. Upstream was fetched at 2026-10-22T03:23:31Z and was
+that commit.
+
+Overlap snapshot: open PRs fetched 2026-10-22T03:25:01Z (308 records) and
+discussions fetched 2026-10-22T03:25:44Z (3401 records). A search for
+`global tail`, `does not move the global reference` and `p^10 exp(-p^2)`
+returned #4520, which asks this question, the locality audit, and #4452.
+The other hits use "global tail" for unrelated transforms. No result
+replaces HALO's `p^{10}` majorant by the within-cell `p^6` bound. A search
+miss is not a novelty certificate. The audit is the identity. #4452 is the
+within-cell bound. HALO is the written tail.
+
+## Open next questions
+
+1. **Does the restricted gate absorb one section error `p^6 exp(-p^2)` and
+   one global tail `p^{10} exp(-p^2)`?** The two errors are not the same
+   `ε`. Their sum is `p^6 (1 + p^4) exp(-p^2)`, not `2 p^6 exp(-p^2)`. The
+   first step is to place the factor `1 + p^4` in the exponent and clear
+   the eighths. HALO already assumes `||H^{-1}||_2 ≤ p^{10}`; this question
+   does not ask for a proof of that assumption.
+
+## Credit
+
+- The identity and the factor `p^{10}` are the locality audit's, applied to
+  HALO's polynomial.
+- The within-cell `p^6` bound, and the refusal to move the global reference,
+  are #4452's.
+- The conditional `p^6` bound under `||H^{-1}||_2 ≤ 16 p^2` is #4406's.
+- The question is #4520's.
+
+Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0.

research/gaussian-global-tail/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc",
+  "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/gaussian-delta-exponents/README.md",
+      "usage": "input",
+      "git_blob": "6e5f1cc5b77a2ddefaf6f3aba658535e506b3346",
+      "sha256": "e7c954e592a34df777a6e888c72b3fdf6968abf8cf7b3419fa447ee716142989"
+    },
+    {
+      "path": "research/gaussian-halo-exponents/README.md",
+      "usage": "input",
+      "git_blob": "4f70baafa951df301b4d8e92fe0aff1fd58b2f6e",
+      "sha256": "5d6c75806e51605c56c8dd29a58b5e5f9b6e6e475d4a1598d55ca341db171f5d"
+    },
+    {
+      "path": "research/halo-locality-witness-audit/README.md",
+      "usage": "input",
+      "git_blob": "03b244baf61b427edbccd29698a05583b5405dd6",
+      "sha256": "fc87657cb3e89a74b9462483cc15713f0122256a623fefa65c887e2118f81276"
+    },
+    {
+      "path": "research/unconditional-batched-crt/HALO.md",
+      "usage": "input",
+      "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b",
+      "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc"
+    }
+  ]
+}

research/gaussian-global-tail/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc",
+  "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": "Compare HALO's global identity P - H^{-1} = -Q^J H^{-1} with the within-cell p^6 bound, and record that the written global majorant stays p^{10} exp(-p^2).",
+  "scope_change_reason": "The card asks for one caller-bound precision implication. This package only identifies which tail the written hypotheses prove. It does not put p^{10} into the gate, does not prove the rounded inverse bound, and does not claim a new kappa.",
+  "bottleneck_link": "The selected frontier is unchanged. This is the global-tail question left open by the restricted monomial.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the written global majorant is separated from the within-cell p^6 bound. Do not absorb p^{10} in the gate, do not prove ||H^{-1}||_2 <= 16 p^2, 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-global-tail",
+  "author": "James Reed",
+  "ai_assistance": "Substantial help from Cursor Grok 4.7 on the tail comparison and the package text.",
+  "open_questions": [
+    {
+      "question": "Does the restricted gate absorb one section error p^6 exp(-p^2) and one global tail p^{10} exp(-p^2)?",
+      "why_it_matters": "The two errors are not the same epsilon. Their sum is p^6(1 + p^4) exp(-p^2), not 2 p^6 exp(-p^2).",
+      "first_step": "Place the factor 1 + p^4 in the exponent of the restricted monomial and clear the eighths. Do not prove ||H^{-1}||_2 <= p^{10}; HALO already assumes it.",
+      "blocked_by": "The section p^6 bound still needs the ideal-gap gauge, and the conditional p^6 ceiling needs ||H^{-1}||_2 <= 16 p^2 for the rounded reference."
+    }
+  ]
+}

research/gaussian-global-tail/VERIFY.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "research/gaussian-delta-exponents/README.md",
+    "research/gaussian-halo-exponents/README.md",
+    "research/halo-locality-witness-audit/README.md",
+    "research/unconditional-batched-crt/HALO.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "HALO's truncation uses p^{42} against p^{-40}, which supplies the exp(-p^2) slot and leaves the inverse factor p^{10}. That factor exceeds p^6 by p^4. The within-cell p^6 bound does not move the global reference, and the conditional p^6 bound needs an unproved ceiling of 16 p^2."
+    }
+  ]
+}

research/gaussian-global-tail/verify.py

@@ -0,0 +1,64 @@
+#!/usr/bin/env python3
+"""Separate HALO's written global tail from the within-cell p^6 bound.
+
+Every comparison is an integer identity. The ideal-gap gauge stays a hypothesis.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import json
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+PACKAGE = ROOT / "research" / "gaussian-global-tail"
+
+
+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")
+    audit = (ROOT / "research/halo-locality-witness-audit/README.md").read_text(encoding="utf-8")
+    cell = (ROOT / "research/gaussian-delta-exponents/README.md").read_text(encoding="utf-8")
+    conditional = (ROOT / "research/gaussian-halo-exponents/README.md").read_text(encoding="utf-8")
+    selected = json.loads(
+        (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")
+    )
+    assert "||P_i-H_i^-1||_2 <= p^10 exp(-p^2)." in halo
+    assert "P - H^-1 = -Q^J H^-1." in audit
+    assert "(1-p^-40)^J p^10 <= exp(-J p^-40) p^10 <= p^10 exp(-p^2)." in audit
+    assert "||P - A^{-1}||_2 < p^6 exp(-p^2)" in cell
+    assert "does not move the global reference." in cell
+    assert "||P - H^-1||_2 < p^6 exp(-p^2)," in conditional
+    assert "It does not prove `||H^-1||_2 <= 16 p^2` for the rounded reference." in conditional
+    assert selected["kappa"] == "23/10000"
+
+
+def tail_gap() -> None:
+    # J = p^{42} against p^{-40} fills exactly the exp(-p^2) slot.
+    assert 42 - 40 == 2
+    # The written inverse factor is larger than p^6 by p^4.
+    assert 10 - 6 == 4
+    assert 2 != 4
+    assert 2**4 == 16
+    assert 16 > 1
+    assert 2**10 == 2**6 * 2**4
+    # At p = 2 the conditional ceiling 16 p^2 equals p^6. It is smaller later.
+    assert 16 * 2**2 == 2**6
+    assert 16 * 3**2 < 3**6
+
+
+def main() -> None:
+    pins_and_phrases()
+    tail_gap()
+    print("PASS_GAUSSIAN_GLOBAL_TAIL")
+
+
+if __name__ == "__main__":
+    main()