Split one axis through the section polynomial (no new κ)

research/gaussian-tensor-bridge/README.md

@@ -0,0 +1,86 @@
+# One axis splits through the section polynomial
+
+**Claim type:** the triangle inequality on one axis.
+**No new κ.** Each section error and the inverse ceiling stay hypotheses.
+The selected record remains `23/10000`.
+
+## Question
+
+#4488 uses three bounds on one axis: `||B|| ≤ 10 p^2`,
+`||C|| ≤ 10 p^2 + ε`, and `||B - C|| < 2 ε`, with
+`ε = p^6 exp(-p^2)`. The named step is to split `B - C` through the section
+polynomial.
+
+## Lemma
+
+Let `B`, `C` and `P` be vectors in a normed space, and let `ε > 0`. Then
+
+```text
+B - C = (B - P) + (P - C),
+||B - C|| ≤ ||B - P|| + ||P - C||,
+||P|| ≤ ||B|| + ||P - B||.
+```
+
+If `||B - P|| < ε` and `||C - P|| < ε`, then `||B - C|| < 2 ε`.
+If `||B|| ≤ 10 p^2` and `||P - B|| < ε`, then `||P|| < 10 p^2 + ε`.
+
+Thus the pair `(B, P)` meets the difference and approximant hypotheses of
+#4488 once the inverse ceiling and one section error are known. The pair of
+inverses `(B, C)` meets `||B - C|| < 2 ε` once both are within `ε` of the
+same polynomial. The ceiling `||B|| ≤ 10 p^2` is not derived here. The factor
+2 is this sum of two errors. HALO's `2g` rectangles remain a volume partition.
+
+## Proof
+
+The first display is the definition of `P`. The norm axioms give the two
+inequalities. If `x < ε` and `y < ε`, then `x + y < 2 ε`. The integer shadow
+replaces a strict cap `ε` by the previous integer: two copies of `m = 3` sum
+to `6`, and `6 < 2 · 4`. The same addition is the factor `1 + 1 = 2`.
+
+The polynomial norm is the second triangle. With ceiling `10` and error `2`,
+`|6| ≤ 10 + 2`. Removing the error from the ceiling fails: `|13 - 10| = 3`
+while `|13| > 10 + 1`.
+
+The scalar check `(8 - 5) = (8 - 6) + (6 - 5)` is the one-dimensional case.
+
+## Not covered
+
+- A proof that `||B - P|| < p^6 exp(-p^2)`, or that `||C - P||` is that small.
+- A proof that `||B|| ≤ 10 p^2`.
+- The tensor sum and the gate below `2^{-C p}`.
+- 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-bridge --check-only
+python3.12 -B scripts/research_package.py --package research/gaussian-tensor-bridge
+```
+
+Base `2a13eb1827784206202db90e5dc8327cf8a250db`, priority revision 7, selection
+refresh κ = `23/10000`.
+
+Overlap on 2026-10-22 (open PRs fetched 2026-10-22T01:25:31Z, 343 records;
+discussions fetched 2026-10-22T01:26:17Z, 3367 records) names this draft, #4488
+(the telescope, which leaves the three bounds open), and the locality audit.
+That audit already writes `||H_sec^{-1} - P_sec|| + ||P - H^{-1}|| <= 2 p^{10}
+exp(-p^2)`. It does not separate the triangle at `ε = p^6 exp(-p^2)` or the
+polynomial norm under the ceiling `10 p^2`. A search miss is not a novelty
+certificate. #4488 is the telescope. HALO is the tensor sentence.
+
+## Open next questions
+
+1. **Is one section error below `p^6 exp(-p^2)` on a core axis?** The bridge
+   consumes `||B - P|| < ε` as a hypothesis. The first step is to match one
+   core row with the within-cell gauge of #4452.
+
+## Credit
+
+- The tensor sentence is #4100's.
+- The locality audit already adds two `p^{10}` errors on a core axis.
+- The ceiling `10 p^2` is Ryanson Jonathan's #4462, as carried through #4481.
+- The section error `p^6 exp(-p^2)` is the within-cell bound of #4452.
+- The three axis hypotheses are #4488's.
+
+Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0.

research/gaussian-tensor-bridge/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-bridge/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": "Split one axis difference through the section polynomial and deduce ||B - C|| < 2ε together with ||P|| < 10 p^2 + ε.",
+  "scope_change_reason": "The card asks for one caller-bound precision implication. This package only applies the triangle inequality. It does not prove a section error or the inverse ceiling, and it does not claim a new kappa.",
+  "bottleneck_link": "The selected frontier is unchanged. This is the polynomial split left open by the one-axis telescope.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the two triangles are recorded. Do not prove a section error, do not prove the inverse ceiling, 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-bridge",
+  "author": "James Reed",
+  "ai_assistance": "Substantial help from Cursor Grok 4.7 on the triangle split and the package text.",
+  "open_questions": [
+    {
+      "question": "Is ||B - P|| < p^6 exp(-p^2) for the section inverse and the section polynomial on one core axis?",
+      "why_it_matters": "The bridge turns two such errors into ||B - C|| < 2ε and turns one of them, plus the inverse ceiling, into the approximant norm.",
+      "first_step": "Match one core row with the within-cell gauge used for the p^6 exp(-p^2) bound.",
+      "blocked_by": "That section error remains conditional on the ideal row gap."
+    }
+  ]
+}

research/gaussian-tensor-bridge/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": "B - C equals (B - P) + (P - C); two integer errors of size 3 sum to less than 2*4; the polynomial norm is the ceiling plus the error, and dropping the error fails at |13| > 10 + 1."
+    }
+  ]
+}

research/gaussian-tensor-bridge/verify.py

@@ -0,0 +1,60 @@
+#!/usr/bin/env python3
+"""Split one axis through the section polynomial.
+
+Every comparison is an integer identity. Each section error and the inverse
+ceiling stay hypotheses.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import json
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+PACKAGE = ROOT / "research" / "gaussian-tensor-bridge"
+
+
+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")
+    selected = json.loads(
+        (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")
+    )
+    assert "tensor product of the section inverses" in halo
+    assert "g p^(10g) exp(-p^2)," in halo
+    assert selected["kappa"] == "23/10000"
+
+
+def bridge() -> None:
+    # (B - C) = (B - P) + (P - C), and the norm adds the two pieces.
+    assert (8 - 5) == (8 - 6) + (6 - 5)
+    assert abs(8 - 5) <= abs(8 - 6) + abs(6 - 5)
+    # Two errors each at most m = 3 sum to 2m, which is below 2(m+1).
+    assert 3 + 3 == 6
+    assert 2 * (4 - 1) < 2 * 4
+    assert 6 < 2 * 4
+    assert 1 + 1 == 2
+    # ||P|| <= ||B|| + ||P - B||. A ceiling of 10 plus the error covers P.
+    assert abs(6) <= abs(8) + abs(6 - 8)
+    assert abs(6) <= 10 + abs(6 - 8)
+    # Dropping the error from the ceiling fails: |13 - 10| = 3 and |13| > 10 + 1.
+    assert abs(13 - 10) == 3
+    assert abs(13) > 10 + 1
+
+
+def main() -> None:
+    pins_and_phrases()
+    bridge()
+    print("PASS_GAUSSIAN_TENSOR_BRIDGE")
+
+
+if __name__ == "__main__":
+    main()