Absorb g copies of the heavy slice by the factor-5 gate (no new κ)

research/gaussian-slice-five-copies/README.md

@@ -0,0 +1,140 @@
+# The factor-5 gate absorbs g copies of the heavy slice
+
+**Claim type:** an explicit absorption bound for one tensor sum.
+**No new κ.** The trailing bound `p^{10}`, the section error, and the
+ceiling `9 p^2` stay hypotheses. The selected record is `60403/20000000`.
+The coefficient-9 monomials keep the published gate `16 g L ≤ p`.
+
+## Question
+
+#4669 puts one heavy slice below `2^{-C p}` under `5 g L ≤ p`. It leaves
+the `g` copies open. Those copies add one `L`. The one-slice fifths
+spend `80 p`, and `8 L ≤ p` turns the new term `40 L` into `5 p`. The
+named step is to test `20 p^2 - 85 p - 80` at `p = 64`.
+
+This `5` is the coefficient of `g L`. It is not a three-bit majorant of
+the ceiling `9`. #4495 still rejects three bits for that ceiling, because
+`9 > 8`, and it still uses four bits because `9 < 16`.
+
+## Lemma
+
+Let `p ≥ 2`, `g ≥ 1`, `K ≥ 0` and `C ≥ 0` be integers, and let
+`L = ceil(log2 p)`. If
+
+```text
+p ≥ max(64, 4K + 2C)    and    5 g L ≤ p,
+```
+
+then `g` copies of
+
+```text
+(p^{10})^{g-1} p^6 (1 + p^4) exp(K p - p^2)
+```
+
+are strictly below `2^{-C p}`. The exponent is at most `-C p - 1`.
+
+The gate is wider than the factor-6 gate. At `p = 70` and `g = 2`,
+`L = 7`, so `5 g L = 70 ≤ 70` while `6 g L = 84 > 70`. The copies
+exponent there is `-4752`.
+
+At `p = 2` and `g = 2` the hypothesis fails, and the two copies are larger
+than `1`.
+
+## Proof
+
+#4669 puts one slice strictly below `2^{E_0}` for
+
+```text
+E_0 = 10 g L + 1 + 2 K p - p^2.
+```
+
+The same gate forces `g < 2^L`. Indeed `p ≤ 2^L` and `5 L > 1`, so
+`5 g L ≤ p` implies `g < 2^L`. Multiplying by `g` therefore adds one
+`L`. The copies are strictly below `2^E` for
+
+```text
+E = 10 g L + L + 1 + 2 K p - p^2.
+```
+
+Clear `40 (E + C p)`, five times `8 (E + C p)`. As in the one-slice
+argument, `400 g L ≤ 80 p` and the linear term contributes at most
+`20 p^2`. The new piece is `40 L`. For every integer `p ≥ 64`,
+`8 L ≤ p`, so `40 L = 5 · 8 L ≤ 5 p`. The base of that comparison is
+`8 · 7 = 56 ≤ 64 = 2^6`. If `8 (m + 1) ≤ 2^m`, then
+
+```text
+8 (m + 2) = 8 (m + 1) + 8 ≤ 2^m + 8 ≤ 2^{m + 1},
+```
+
+because `8 ≤ 2^6`. Thus `8 (m + 1) ≤ 2^m` for every integer `m ≥ 6`.
+When `2^m ≤ p < 2^{m + 1}`, the level is `m` at the power of two and
+`m + 1` after it, and both are at most `p`.
+
+`40 (E + C p)` is therefore at most
+
+```text
+80 p + 5 p + 40 - 20 p^2 = -(20 p^2 - 85 p - 40).
+```
+
+The polynomial `20 p^2 - 85 p - 80` equals `76400` at `p = 64` and
+then increases by `40 p - 65`. Thus `20 p^2 - 85 p - 40 ≥ 40` for every
+integer `p ≥ 64`, so `40 (E + C p) ≤ -40` and `E ≤ -C p - 1`.
+
+At `p = 2` and `g = 2`, `5 g L = 10 > 2` and the formal exponent is
+`18`. The series of `e` through `1/6!` is `13699/5040`. The later ratios
+are at most `1/8`, so the tail is strictly below `8/(7 · 5040)`. The gap
+up to `3` is `1421/5040`, and `8 < 1421 · 7`, so `e < 3` and `exp(4) < 81`.
+One slice at this point has polynomial part `2^{10} · 1088`, so two copies
+have polynomial part `2 · 2^{10} · 1088 > 81`. The copies are larger than `1`.
+
+## Not covered
+
+- A gate factor smaller than `5`. The one-slice exponent still spends
+  `10 g L`. The coefficient-9 monomials still use `16`.
+- A proof that `||H^{-1}||_2 ≤ p^{10}`. HALO assumes it.
+- The section error `p^6 exp(-p^2)` and the leading ceiling `9 p^2`.
+- Editing the #4100 notes, or the #4495 gate.
+- Any new κ.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/gaussian-slice-five-copies --check-only
+python3.12 -B scripts/research_package.py --package research/gaussian-slice-five-copies
+```
+
+Base `b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, priority revision 7.
+Upstream was fetched at 2026-10-22T15:03:53Z and was that commit. The
+pre-submit fetch at 2026-10-22T15:05:33Z was the same commit. The pinned
+blobs for the selected record, the catalogue, both source READMEs, and
+HALO.md match that main. The selection is κ = `60403/20000000`.
+
+Overlap snapshot: open PRs fetched 2026-10-22T15:04:30Z (440 records) and
+discussions fetched 2026-10-22T15:05:24Z (3597 records). Terms
+`20 p^2 - 85 p - 80`, `slice-five-copies`, and `4752` reported 55 matches
+and showed 8. The first two were this README and this TASK. The six shown
+discussion hits contain the digits `4752` inside hashes, a timestamp, or
+an unrelated fixture `y=4752`. A second search of the same cache, offline,
+dropped `4752`. It returned this README, this TASK, and the #4669 DONE
+(discussioncomment-19126275). That note leaves these copies open and names
+the test at `p = 64`. The handoff thread, reread at the pre-submit fetch,
+still ends at that #4669 DONE. The open-PR list at that time still starts
+at #4669. No matches is not a novelty certificate.
+
+## Open next questions
+
+1. **Does `4 g L ≤ p` already absorb one heavy slice?** The exponent
+   spends `10 g L`. The first step is the fourths identity
+   `320 g L = 80 · 4 g L`, then the test of `16 p^2 - 80 p - 64` at
+   `p = 64`. Do not change the coefficient-9 monomial gate.
+
+## Credit
+
+- The factor-5 slice, and this question, are #4669's.
+- The factor-6 copies are #4668's.
+- The unequal factor `1 + p^4` is #4524's.
+- The published gate `16 g L ≤ p` is #4495's. It is unchanged.
+- The ceiling `9 p^2` is #4493's.
+- The written tail `p^{10} exp(-p^2)` is #4100's.
+
+Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0.

research/gaussian-slice-five-copies/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/gaussian-neumann-nine/README.md",
+      "usage": "input",
+      "git_blob": "54a8ce117a233e54e5057fd1edfa378e59527592",
+      "sha256": "189a0fb9ede1649ffea24ea22605a573366170e172ac563dd001c68d65b966ac"
+    },
+    {
+      "path": "research/gaussian-tensor-nine/README.md",
+      "usage": "input",
+      "git_blob": "96c9f03626d145bf38a9d4850f0aba4b05c0279c",
+      "sha256": "a71bc77ba9885e1c5f231ad3b89d01da7860aae53b08ac87b4abca507fec8b82"
+    },
+    {
+      "path": "research/unconditional-batched-crt/HALO.md",
+      "usage": "input",
+      "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b",
+      "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc"
+    }
+  ]
+}

research/gaussian-slice-five-copies/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "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": "Show that 5 g ceil(log2 p) <= p and p >= max(64, 4K + 2C) put g copies of the heavy slice strictly below 2^{-C p}.",
+  "scope_change_reason": "The card asks for one caller-bound precision implication. This package only clears that scalar sum under the factor-5 gate. It does not replace the coefficient-9 monomial gate, does not prove ||H^{-1}||_2 <= p^{10}, and does not claim a new kappa.",
+  "bottleneck_link": "The selected frontier is unchanged. This is the g-copies question left open by the factor-5 slice.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the g copies are below 2^{-C p} under 5 g L <= p. Do not lower the factor from 5 to 4, do not change the coefficient-9 monomial gate, do not prove the inverse bound, and do not claim a new kappa.",
+  "outcome": "completed",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/gaussian-slice-five-copies",
+  "author": "James Reed",
+  "ai_assistance": "Substantial help from Cursor Grok 4.7 on the factor-5 copies exponent and the package text.",
+  "open_questions": [
+    {
+      "question": "Does 4 g ceil(log2 p) <= p already absorb one heavy slice?",
+      "why_it_matters": "The exponent spends 10 g L. A factor of 4 would be a wider gate for this slice. The coefficient-9 monomials still use 16.",
+      "first_step": "Use the fourths identity 320 g L = 80 * 4 g L and test 16 p^2 - 80 p - 64 at p = 64. Do not change the coefficient-9 monomial gate.",
+      "blocked_by": "The trailing p^{10} factor and the section error remain hypotheses."
+    }
+  ]
+}

research/gaussian-slice-five-copies/VERIFY.json

@@ -0,0 +1,23 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "research/gaussian-neumann-nine/README.md",
+    "research/gaussian-tensor-nine/README.md",
+    "research/unconditional-batched-crt/HALO.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Under 5 g L <= p and p >= 64 the copies exponent is at most -C p - 1. At p = 70 and g = 2 this gate holds and the factor-6 gate fails. At p = 2 and g = 2 the copies exceed 1."
+    }
+  ]
+}

research/gaussian-slice-five-copies/verify.py

@@ -0,0 +1,111 @@
+#!/usr/bin/env python3
+"""Absorb g copies of the heavy slice by the factor-5 gate.
+
+Every comparison is an integer identity. The inverse bound stays a hypothesis.
+The coefficient-9 monomial gate stays at 16.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import json
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+PACKAGE = ROOT / "research" / "gaussian-slice-five-copies"
+
+
+def digest(path: Path) -> str:
+    return hashlib.sha256(path.read_bytes()).hexdigest()
+
+
+def ceil_log2(value: int) -> int:
+    level = 0
+    power = 1
+    while power < value:
+        power *= 2
+        level += 1
+    return level
+
+
+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"]
+    gate = (ROOT / "research/gaussian-tensor-nine/README.md").read_text(encoding="utf-8")
+    nine = (ROOT / "research/gaussian-neumann-nine/README.md").read_text(encoding="utf-8")
+    halo = (ROOT / "research/unconditional-batched-crt/HALO.md").read_text(encoding="utf-8")
+    selected = json.loads(
+        (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")
+    )
+    assert "16 g L ≤ p" in gate
+    assert "9 < 16" in gate
+    assert "9 > 8" in gate
+    assert "8 p^2 < U < 9 p^2." in nine
+    assert "||P_i-H_i^-1||_2 <= p^10 exp(-p^2)." in halo
+    assert selected["kappa"] == "60403/20000000"
+
+
+def budget() -> None:
+    # Fifths spend 80 p. Copies replace 40 L by 5 p once 8 L <= p.
+    assert 80 * 5 == 400
+    assert 5 * 8 == 40
+    assert 40 == 5 * 8
+    assert 80 + 5 == 85
+    assert 40 * (2 * 3 + 5) == 20 * (4 * 3 + 2 * 5)
+    # 5 L > 1, so the gate forces g < 2^L.
+    assert 5 > 1
+    # 8 (m + 1) <= 2^m for m >= 6, and the step preserves a doubling.
+    assert 8 * 7 <= 2**6
+    assert 8 <= 2**6
+    assert 2**6 + 8 <= 2**7
+    assert ceil_log2(64) == 6
+    assert ceil_log2(65) == 7
+    assert 8 * 6 <= 64
+    assert 8 * 7 <= 65
+    # 20 p^2 - 85 p - 80 is positive at p = 64 and increases by 40 p - 65.
+    assert 20 * 64 * 64 - 85 * 64 - 80 == 76400
+    assert 76400 > 0
+    assert (20 * 65 * 65 - 85 * 65 - 80) - 76400 == 40 * 64 - 65
+
+
+def witness() -> None:
+    # Two axes at p = 70 meet factor 5 and miss factor 6.
+    level = ceil_log2(70)
+    assert level == 7
+    assert 5 * 2 * level <= 70
+    assert 6 * 2 * level > 70
+    assert 2 < 2**level
+    one = 10 * 2 * level + 1 - 70 * 70
+    copies = one + level
+    assert one == -4759
+    assert copies == -4752
+    assert copies <= -1
+
+
+def outside() -> None:
+    # At p = 2 and g = 2 the factor-5 hypothesis fails.
+    assert ceil_log2(2) == 1
+    assert 5 * 2 * 1 > 2
+    assert 10 * 2 * 1 + 1 + 1 - 2 * 2 == 18
+    # e < 3, so two copies of the p = 2 slice exceed 1.
+    total = 5040 + 5040 + 2520 + 840 + 210 + 42 + 7
+    assert total == 13699
+    assert 3 * 5040 - total == 1421
+    assert 8 < 1421 * 7
+    assert 3**4 == 81
+    assert 2**6 * (1 + 2**4) == 1088
+    assert 2 * (2**10) * 1088 > 81
+
+
+def main() -> None:
+    pins_and_phrases()
+    budget()
+    witness()
+    outside()
+    print("PASS_GAUSSIAN_SLICE_FIVE_COPIES")
+
+
+if __name__ == "__main__":
+    main()