Absorb the face factor 2 on the coefficient-9 approximant (no new κ)

research/gaussian-tensor-nine-faces/README.md

@@ -0,0 +1,143 @@
+# The face factor 2 spends one bit of the coefficient-9 slack
+
+**Claim type:** an explicit absorption bound for one constant factor.
+**No new κ.** The section ceiling `9 p^2` and the section error
+`p^6 exp(-p^2)` stay hypotheses. The selected record remains `23/10000`.
+
+## Question
+
+#4497 absorbs
+
+```text
+g (9 p^2 + p^6 exp(-p^2))^{g-1} p^6 exp(K p - p^2)
+```
+
+under the gate `p ≥ max(64, 4K + 2C)` and `16 g ceil(log2 p) ≤ p`, with
+exponent at most `-C p - 4`. Does the extra factor of 2 still leave the
+monomial below `2^{-C p}`?
+
+## 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    16 g L ≤ p,
+```
+
+then
+
+```text
+2 g (9 p^2 + p^6 exp(-p^2))^{g-1} p^6 exp(K p - p^2) < 2^{-C p}.
+```
+
+The case `K = 0` is the monomial in the question. The factor 2 contributes
+one bit. The exponent is at most `-C p - 3`. Whenever `g log p = o(p)`,
+every fixed pair `K, C` satisfies the gate for all large `p`.
+
+This comparison does not identify HALO's `2g` rectangles with the tensor
+error. It charges the constant 2 against slack that is already present.
+At `g = p^2` the same error is greater than 1 for every integer `p ≥ 2`.
+
+## Proof
+
+The series `1 + 1 + 1/2 = 5/2 > 2` gives `e > 2`, so `exp(-p^2) < 2^{-p^2}`.
+For `k ≥ 2`, `k! ≥ 2^{k-1}`: the values at 2, 3 and 4 are `2`, `6` and `24`,
+and the step uses `k + 1 ≥ 2`. The tail of `e` is then at most the geometric
+series of ratio `1/2`, so `e < 3 < 4` and `exp(K p) ≤ 2^{2 K p}`, with
+equality only at `K = 0`.
+
+For every integer `p ≥ 64`, `8 L ≤ p`. The base is `8 · 7 = 56 ≤ 64` at
+`p = 2^6`, and `8 ≤ 64`. If `8(m + 1) ≤ 2^m`, then
+`8(m + 2) ≤ 2^m + 8 ≤ 2^{m+1}`. On each dyadic interval the largest ratio of
+`L` to `p` is at the left endpoint. From `8 L ≤ p`, `48 L = 6 · 8 L ≤ 6 p`.
+The quadratic `4 p^2 - 3 p - 4` equals 6 at `p = 2` and increases by `8 p + 1`
+at the next integer, so `6 p ≤ 8(p^2 - 1)`. Hence `6 L ≤ p^2 - 1`. Since
+`p ≤ 2^L`, `p^6 ≤ 2^{6 L} ≤ 2^{p^2 - 1}`, and
+
+```text
+p^6 exp(-p^2) < p^6 2^{-p^2} ≤ 1/2.
+```
+
+Thus `9 p^2 + p^6 exp(-p^2) < 9 p^2 + 1 < 16 p^2`, because `1 < 7 p^2`
+for every integer `p ≥ 2`. At `g = 1` the power `g - 1` is zero. For
+`g ≥ 2` the approximant base is strictly smaller than `16 p^2`, so
+
+```text
+2 g (9 p^2 + p^6 exp(-p^2))^{g-1} p^6 exp(K p - p^2)
+  < 2 · g 2^{4g-4} p^{2g+4} 2^{2 K p - p^2}.
+```
+
+The gate forces `g < 2^L`, because `L ≥ 1` and `g ≤ p/(16 L) ≤ p/16`.
+Since `2 = 2^1`, the product is strictly less than
+
+```text
+2^{1 + 2 g L + 4 g + 5 L - 4 + 2 K p - p^2}.
+```
+
+Clear the eighths of the exponent without the new bit. The four pieces
+scale as `8 · 2 g L = 16 g L ≤ p`, `8 · 4 g = 2 · 16 g ≤ 2 p`,
+`8 · 5 L = 5 · 8 L ≤ 5 p`, and `8 (2 K + C) p ≤ 4 p^2` once
+`p ≥ 4 K + 2 C`, because `8(2 K + C) = 4(4 K + 2 C)`. The constant `-4`
+contributes `-32`. The sum is at most `-4(p^2 - 2 p + 8)`. The coefficients
+of `p` are `1 + 2 + 5 = 8`. At `p = 2` the polynomial equals 8, and the step
+to the next integer is `2 p - 1`. It is therefore at least 8, so eight times
+the shifted exponent is at most `-32`. The exponent without the face factor
+is at most `-C p - 4`. One bit lowers the remaining slack from 4 to 3, and
+the exponent above is at most `-C p - 3`.
+
+If `g log p = o(p)`, then `g log2 p ≤ p/32` for large `p`. For `p ≥ 3`,
+`L ≤ 2 log2 p`, so the gate holds eventually, and every fixed `K` and `C`
+satisfy `p ≥ 4 K + 2 C` as well.
+
+At `g = p^2` the product is twice a quantity larger than
+`g (9 p^2)^{g-1} p^6 exp(-p^2)`. The smaller monomial equals
+`g (9 p^2)^g exp(-p^2) · p^4 / 9`, and
+`(9 p^2)^{p^2} > 4^{p^2} > exp(p^2)` because `9 p^2 ≥ 36 > 4` and `e < 4`,
+while `p^4 / 9 > 1` because `p^4 ≥ 16 > 9`. That product is greater than 1,
+so the face-factor monomial is greater than 1 as well.
+
+## Not covered
+
+- A proof that the tensor difference is at most this monomial.
+- A proof that a section inverse is at most `9 p^2`, or that a section
+  error is less than `p^6 exp(-p^2)`.
+- Editing the #4100 notes. They still say `g p^{10 g} exp(-p^2)`.
+- Any new κ.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/gaussian-tensor-nine-faces --check-only
+python3.12 -B scripts/research_package.py --package research/gaussian-tensor-nine-faces
+```
+
+Base `2a13eb1827784206202db90e5dc8327cf8a250db`, priority revision 7, selection
+refresh κ = `23/10000`. Upstream was fetched at 2026-10-22T02:42:08Z and was
+still that commit.
+
+Overlap snapshot: open PRs fetched 2026-10-22T02:42:49Z (356 records) and
+discussions fetched 2026-10-22T02:43:31Z (3381 records). A search for
+`face factor 2`, `slack of 4` and `9 p^2 + p^6` returned this draft, #4497,
+which leaves the factor open, #4487, which spends the same bit on the
+coefficient 10, and the predecessor fold #4496. A search miss is not a
+novelty certificate. #4497 is the predecessor budget. HALO is the written
+error.
+
+## Open next questions
+
+1. **Is one axis of the tensor difference at most two section errors?** The
+   scalar factor 2 is not that identification. The first step is to expand
+   one axis under the hypotheses `||B_i|| ≤ 9 p^2`,
+   `||C_i|| ≤ 9 p^2 + ε` and `||B_i - C_i|| < 2 ε`, with
+   `ε = p^6 exp(-p^2)`.
+
+## Credit
+
+- The one-bit charge against slack 4 is the route of #4487.
+- The approximant budget with coefficient 9 is #4497.
+- The section error `p^6 exp(-p^2)` is the within-cell bound of #4452.
+- HALO's sentence `These 2g sets are disjoint rectangles.` is a volume
+  partition. The written error `g p^{10 g} exp(-p^2)` is #4100's.
+
+Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0.

research/gaussian-tensor-nine-faces/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/HALO.md",
+      "usage": "input",
+      "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b",
+      "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc"
+    }
+  ]
+}

research/gaussian-tensor-nine-faces/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 face factor 2 still leaves 2 g (9 p^2 + p^6 exp(-p^2))^{g-1} p^6 exp(K p - p^2) below 2^{-C p}, by charging one bit against the slack of 4.",
+  "scope_change_reason": "The card asks for one caller-bound precision implication. This package only charges that constant factor. It does not identify the tensor difference and does not claim a new kappa.",
+  "bottleneck_link": "The selected frontier is unchanged. This is the face factor left open by the coefficient-9 approximant.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the factor 2 is charged against the slack of 4. Do not expand a tensor axis, do not prove the ideal gaps, 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-tensor-nine-faces",
+  "author": "James Reed",
+  "ai_assistance": "Substantial help from Cursor Grok 4.7 on the one-bit charge and the package text.",
+  "open_questions": [
+    {
+      "question": "Is one axis of the tensor difference at most two section errors when the ceiling is 9 p^2?",
+      "why_it_matters": "The scalar factor 2 is charged above, and the tensor difference is still a separate identification.",
+      "first_step": "Expand one axis under ||B_i|| <= 9 p^2, ||C_i|| <= 9 p^2 + epsilon and ||B_i - C_i|| < 2 epsilon, with epsilon = p^6 exp(-p^2).",
+      "blocked_by": "Those three norm hypotheses remain open until the ideal gaps are proved. HALO's 2g rectangles are a volume partition, not this factor."
+    }
+  ]
+}

research/gaussian-tensor-nine-faces/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "research/unconditional-batched-crt/HALO.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The coefficient-9 approximant exponent is at most -C p - 4, and the face factor 2 spends one bit, leaving 2 g (9 p^2 + p^6 exp(-p^2))^{g-1} p^6 exp(K p - p^2) below 2^{-C p} with exponent at most -C p - 3."
+    }
+  ]
+}

research/gaussian-tensor-nine-faces/verify.py

@@ -0,0 +1,122 @@
+#!/usr/bin/env python3
+"""The face factor 2 spends one bit of the coefficient-9 approximant slack.
+
+Every comparison is an integer identity. The section ceiling and the section
+error are hypotheses.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import json
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+PACKAGE = ROOT / "research" / "gaussian-tensor-nine-faces"
+
+
+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"]
+    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 "g p^(10g) exp(-p^2)," in halo
+    assert "These 2g sets are disjoint rectangles." in halo
+    assert "exp(O(p)) leaves this below 2^-Cp for every fixed C eventually, provided" in halo
+    assert "g log p=o(p)." in halo
+    assert selected["kappa"] == "23/10000"
+
+
+def series_bounds() -> None:
+    # e > 1 + 1 + 1/2 = 5/2 > 2, and e < 3 < 4.
+    assert 5 > 4
+    assert 3 < 4
+    assert 2 >= 2
+    assert 6 >= 4
+    assert 24 >= 8
+    assert 3 >= 2
+    # 9 p^2 + 1 < 16 p^2. The face factor is the next power of two.
+    assert 7 * 4 > 1
+    assert 9 < 16
+    assert 2**4 == 16
+    assert 2**1 == 2
+    assert 4 - 1 == 3
+    assert 4 * 1 - 4 == 0
+
+
+def section_error_room() -> None:
+    # 8 L <= p implies 48 L <= 6 p, and 6 p <= 8(p^2 - 1) for every integer p >= 2.
+    assert 6 * 8 == 48
+    assert 8 * (2**2 - 1) - 6 * 2 == 2 * (4 * 2**2 - 3 * 2 - 4)
+    assert 4 * 2**2 - 3 * 2 - 4 == 6
+    assert (4 * 3**2 - 3 * 3 - 4) - (4 * 2**2 - 3 * 2 - 4) == 8 * 2 + 1
+    assert ceil_log2(128) == 7
+    assert 6 * 7 <= 128**2 - 1
+    assert 2 * (2**3) == 2**4
+
+
+def log_induction() -> None:
+    # For m >= 6, 8(m+1) <= 2^m, so 8 ceil(log2 p) <= p for every integer p >= 64.
+    assert 8 * 7 <= 64
+    assert 8 <= 64
+    assert 2**6 + 8 <= 2**7
+    assert ceil_log2(2) == 1
+    assert ceil_log2(64) == 6
+    assert ceil_log2(65) == 7
+    assert ceil_log2(128) == 7
+    assert 8 * ceil_log2(128) <= 128
+
+
+def budget() -> None:
+    assert 8 * 2 == 16
+    assert 8 * 4 == 2 * 16
+    assert 8 * 5 == 5 * 8
+    assert 1 + 2 + 5 == 8
+    assert 4 * (4 * 3 + 2 * 5) == 8 * (2 * 3 + 5)
+    prime = 7
+    bare = prime + 2 * prime + 5 * prime + 4 * prime * prime - 32 - 8 * prime * prime
+    assert bare == -4 * (prime * prime - 2 * prime + 8)
+    assert 2**2 - 2 * 2 + 8 == 8
+    assert (3**2 - 2 * 3 + 8) - (2**2 - 2 * 2 + 8) == 2 * 2 - 1
+    # Slack 4 becomes 3 after one bit. Eight times those shifts are -32 and -24.
+    assert 8 * 4 == 32
+    assert 8 * 3 == 24
+    width = 128
+    level = ceil_log2(width)
+    groups = 1
+    assert 16 * groups * level <= width
+    slack = 1 + 2 * groups * level + 4 * groups + 5 * level - 4 - width * width
+    assert slack <= -3
+    # g = p^2 still leaves the smaller inverse-ceiling monomial above 1.
+    assert 9 * 4 > 4
+    assert 2**4 > 9
+
+
+def main() -> None:
+    pins_and_phrases()
+    series_bounds()
+    section_error_room()
+    log_induction()
+    budget()
+    print("PASS_GAUSSIAN_TENSOR_NINE_FACES")
+
+
+if __name__ == "__main__":
+    main()