Core-row operator lift: HALO's tensor bound needs no off-core polynomial estimate (answers #4515; no new κ)

research/core-row-operator-lift/README.md

@@ -0,0 +1,82 @@
+# The core-row operator lift: HALO's tensor bound needs no off-core polynomial estimate
+
+**Claim type:** a written lemma with exact rational controls. **No new κ.** It answers the open question of
+jwr404's [#4515](https://github.com/CrocSwap/integer-mult-bounds/pull/4515). #4515 shows that the
+shared-row sum does not lift to the full operator norm `‖B − C‖₂ < 2ε`. It leaves open a bound on
+`‖P_sec − P_global‖₂` off the rows at distance `A = ⌈p^{48}⌉`.
+
+That bound is not needed. HALO only keeps core outputs ("Keep outputs at distance A from every face"),
+so the right statement is restricted to those rows, and there it holds.
+
+## Lemma
+
+For axis `i`, define:
+
+- `Π_i`: the coordinate projection onto the rows HALO keeps;
+- `B_i`: the section inverse, extended by zero outside the section;
+- `C_i`: the global inverse;
+- `P_sec`, `P_glob`: the section and global Neumann polynomials.
+
+Assume, as in #4491/#4452 and HALO:
+
+1. `‖B_i − P_sec‖₂ < ε` and `‖P_glob − C_i‖₂ < ε`.
+2. `Π_i P_sec = Π_i P_glob`. This is HALO's sentence that a row at distance `A` "is therefore EXACTLY the
+   corresponding row of the global `P_i`".
+3. `‖B_i‖₂, ‖C_i‖₂ ≤ M`, for example `M = 9p²` from #4493, or the global ceiling of #4462.
+
+Then:
+
+    ‖Π_i(B_i − C_i)‖₂ < 2ε,
+    ‖⊗_i Π_i B_i − ⊗_i Π_i C_i‖₂ < 2g·M^{g−1}·ε,    with ⊗_i Π_i B_i = (⊗_i Π_i)(⊗_i B_i).
+
+**Proof.**
+
+- **One axis.** `Π(B − C) = Π(B − P_sec) + Π(P_glob − C)` by (2). Also `‖ΠX‖₂ ≤ ‖X‖₂`, since
+  `XᵀX − (ΠX)ᵀ(ΠX) = ((I−Π)X)ᵀ((I−Π)X)` is a Gram matrix and hence positive semidefinite.
+- **Tensors.** Telescope `⊗ΠB − ⊗ΠC = Σ_k ΠC_1 ⊗ … ⊗ Π(B_k − C_k) ⊗ … ⊗ ΠB_g`, use multiplicativity of
+  the 2-norm under `⊗`, and use `‖Π_iB_i‖, ‖Π_iC_i‖ ≤ M`.
+- **The kept outputs.** The core box is a product of per-axis intervals, so the kept outputs are exactly
+  the range of `⊗Π_i`, and the mixed-product rule applies. ∎
+
+This bound is slightly sharper than #4508's `2g(9p² + ε)^{g−1}ε`, because no approximant norm enters. The
+off-core rows of `P_sec − P_glob` never appear.
+
+## Exact controls (`verify.py`)
+
+- The Gram certificate and the restricted two-error split, on 40 random rational 6×6 cases.
+- The mixed-product rule and the **exact** restricted telescope, for `g = 2` and `3`.
+- #4515's examples:
+  - `[[3,0],[0,9]]` has a small first row but a column of length 9. Restricted to the kept row, its norm
+    is 3.
+  - `[[0,0],[0,2]]` vanishes on the kept row. The restricted sum is `3 + 0 + 3 = 6 < 8`, against the
+    unrestricted `3 + 2 + 3 = 8`.
+- HALO's phrases are pinned.
+
+## Not covered
+
+- The ideal-gap gauges, which stay hypotheses.
+- The global ceiling `‖C_i‖ ≤ M`, which is taken from #4462/#4493 as a hypothesis.
+- Any new κ.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/core-row-operator-lift --check-only
+python3.12 -B scripts/research_package.py --package research/core-row-operator-lift
+```
+
+The verifier prints `PASS_CORE_ROW_OPERATOR_LIFT`, using only the standard library.
+
+## Open next questions
+
+1. **Plug the restricted bound into #4506's `2^{−Cp}` comparison with `M = 9p²`.**
+   - *First step:* replace `(9p² + ε)^{g−1}` by `(9p²)^{g−1}` in #4506's inequality, and recheck the
+     four-bit gate.
+
+## Credit
+
+- The chain and the question are James Reed's (jwr404: #4488 through #4515).
+- HALO's locality argument is from the #4100 notes.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/core-row-operator-lift/SOURCES.json

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

research/core-row-operator-lift/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": "Restricted (core-row) operator lift for HALO's tensor bound, answering #4515.",
+  "scope_change_reason": "Open question of #4515.",
+  "bottleneck_link": "Side result on the #4100 precision/conditioning obligation.",
+  "budget_minutes": 30,
+  "stop_rule": "Stop at the lemma and exact controls.",
+  "outcome": "completed",
+  "evidence": "||Pi_i(B_i-C_i)|| < 2 eps and ||(x)Pi B - (x)Pi C|| < 2 g M^(g-1) eps without any off-core polynomial bound; exact controls pass.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Plug the restricted bound into #4506's comparison with M = 9p^2.",
+      "why_it_matters": "Removes the +eps in the approximant base.",
+      "first_step": "Replace (9p^2+eps)^(g-1) by (9p^2)^(g-1) and recheck the gate.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/core-row-operator-lift/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/unconditional-batched-crt/HALO.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Restricted core-row lift: Gram certificate ||Pi X|| <= ||X||, two-error split under Pi P_sec = Pi P_glob, mixed-product rule and exact restricted telescope (g=2,3), #4515's examples; HALO phrases pinned."
+    }
+  ]
+}

research/core-row-operator-lift/verify.py

@@ -0,0 +1,112 @@
+#!/usr/bin/env python3
+"""The core-row (restricted) operator lift behind HALO's tensor bound, with exact rational controls.
+
+Lemma (README). Let Pi_i be the coordinate projection onto the rows of axis i kept by HALO (distance >= A from the
+section faces), B_i the section inverse (zero outside the section), C_i the global inverse, P_sec and P_glob the
+section and global Neumann polynomials. If ||B_i - P_sec|| < eps, ||P_glob - C_i|| < eps and Pi_i P_sec = Pi_i P_glob
+(HALO's row identity), then ||Pi_i (B_i - C_i)|| < 2 eps; and with ||Pi_i B_i||, ||Pi_i C_i|| <= M,
+    ||(x)_i Pi_i B_i - (x)_i Pi_i C_i|| < 2 g M^(g-1) eps,   and (x)_i Pi_i B_i = ((x)_i Pi_i)((x)_i B_i).
+This verifier checks exactly (Fractions): the Gram identity X^T X - (Pi X)^T (Pi X) = ((I-Pi) X)^T ((I-Pi) X), which
+certifies ||Pi X||_2 <= ||X||_2; the row identity Pi(B - C) = Pi(B - P_sec) + Pi(P_glob - C) when Pi P_sec = Pi P_glob;
+the mixed-product rule and the exact restricted telescope for g = 2, 3 on random rational matrices; and #4515's two
+examples, where the unrestricted lift fails but the restricted rows obey the bound. Pinned HALO phrases.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from fractions import Fraction as F
+import hashlib
+import json
+from pathlib import Path
+import random
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def mm(A, B):
+    return [[sum(A[i][k] * B[k][j] for k in range(len(B))) for j in range(len(B[0]))] for i in range(len(A))]
+
+
+def tr(A):
+    return [list(r) for r in zip(*A)]
+
+
+def sub(A, B):
+    return [[a - b for a, b in zip(ra, rb)] for ra, rb in zip(A, B)]
+
+
+def addm(A, B):
+    return [[a + b for a, b in zip(ra, rb)] for ra, rb in zip(A, B)]
+
+
+def kron(A, B):
+    return [[a * b for a in ra for b in rb] for ra in A for rb in B]
+
+
+def proj(n, keep):
+    return [[F(int(i == j and i in keep)) for j in range(n)] for i in range(n)]
+
+
+def rnd(rng, r, c):
+    return [[F(rng.randint(-9, 9), rng.randint(1, 5)) for _ in range(c)] for _ in range(r)]
+
+
+def main():
+    for row in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"]:
+        need(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], row["path"])
+    halo = (ROOT / "research/unconditional-batched-crt/HALO.md").read_text(encoding="utf-8")
+    for phrase in ("therefore EXACTLY the corresponding row of the global P_i", "Keep outputs at distance A",
+                   "from every face. Their difference from the full inverse tensor is at most"):
+        need(phrase in halo, "HALO phrase: " + phrase)
+    rng = random.Random(4515)
+    n = 6
+    for _ in range(40):
+        keep = set(rng.sample(range(n), 3))
+        Pi, I = proj(n, keep), proj(n, set(range(n)))
+        X = rnd(rng, n, n)
+        PX, RX = mm(Pi, X), mm(sub(I, Pi), X)
+        need(sub(mm(tr(X), X), mm(tr(PX), PX)) == mm(tr(RX), RX), "Gram certificate for ||Pi X|| <= ||X||")
+        B, C, Psec, Pglob = (rnd(rng, n, n) for _ in range(4))
+        Psec = addm(mm(Pi, Pglob), mm(sub(I, Pi), Psec))  # enforce Pi P_sec = Pi P_glob
+        need(mm(Pi, Psec) == mm(Pi, Pglob), "row identity on kept rows")
+        need(mm(Pi, sub(B, C)) == addm(mm(Pi, sub(B, Psec)), mm(Pi, sub(Pglob, C))), "restricted two-error split")
+    for g in (2, 3):
+        dims = [3] * g
+        Bs = [rnd(rng, d, d) for d in dims]
+        Cs = [rnd(rng, d, d) for d in dims]
+        Ps = [proj(d, set(rng.sample(range(d), 2))) for d in dims]
+        PB = [mm(P, B) for P, B in zip(Ps, Bs)]
+        PC = [mm(P, C) for P, C in zip(Ps, Cs)]
+
+        def kr(ms):
+            out = ms[0]
+            for m in ms[1:]:
+                out = kron(out, m)
+            return out
+
+        need(mm(kr(Ps), kr(Bs)) == kr(PB), f"g={g}: mixed-product rule")
+        total = None
+        for k in range(g):
+            term = kr(PC[:k] + [sub(PB[k], PC[k])] + PB[k + 1:])
+            total = term if total is None else addm(total, term)
+        need(sub(kr(PB), kr(PC)) == total, f"g={g}: exact restricted telescope")
+    # #4515's examples: unrestricted lift fails, restricted rows behave
+    M = [[F(3), F(0)], [F(0), F(9)]]
+    e1 = proj(2, {0})
+    need(sum(x * x for x in M[0]) < 64 and sum(M[i][1] ** 2 for i in range(2)) > 64, "#4515 example 1: small row, large column")
+    PM = mm(e1, M)
+    need(max(sum(PM[i][j] ** 2 for i in range(2)) for j in range(2)) == 9 < 64, "restricted to the small row the norm is 3")
+    D = [[F(0), F(0)], [F(0), F(2)]]
+    need(mm(e1, D) == [[0, 0], [0, 0]], "#4515 example 2: the extra term vanishes on the kept row")
+    need(3 + 0 + 3 < 2 * 4 and not 3 + 2 + 3 < 2 * 4, "restricted sum 6 < 8, unrestricted 8 is not")
+    print(json.dumps({"status": "PASS_CORE_ROW_OPERATOR_LIFT", "gram_cases": 40, "telescope_g": [2, 3],
+                      "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())