Transfer the δ halo exponents 11, 24, 26, 26, 6 across cells; robust to the 'rounded' reading (no new κ)

research/delta-cross-cell-transfer/README.md

@@ -0,0 +1,105 @@
+# The δ halo exponents 11, 24, 26, 26 and 6 transfer across cells, and survive the "rounded" reading
+
+**Claim type:** a conditional transfer lemma plus a robustness lemma, with exact rational checks.
+**No new κ.** It answers the open question of jwr404's
+[#4452](https://github.com/CrocSwap/integer-mult-bounds/pull/4452) and of my #4460: do the within-cell
+δ exponents survive on the banded reference across cells? The ideal gaps `1/(8p²)` stay hypotheses.
+
+## Setting
+
+The banded reference `H` has diagonal exactly one and bandwidth `W ≤ p − 1`. The ideal Gaussian matrix
+`N` has row and column off-sums `T ≤ 1 − g`, where `g = 1/(8p²)`. Within cells, `|H| ≤ N/(1 − δ)` with
+`δ = 2^{2−32760p}`, as in #4451 and #4452.
+
+## Lemma A: the downward reading
+
+LOG-A says "across cells, use the retained downward Gaussian entries", and #4449 proves the matching
+contract `0 ≤ H ≤ n`. Split each off-sum as `T = T_in + T_out`. Then
+
+    off(H) ≤ T_in/(1−δ) + T_out ≤ T/(1−δ) ≤ (1−g)/(1−δ),
+
+because `(1−δ)[T_in/(1−δ) + T_out] − T = −δ·T_out ≤ 0`. This is #4442's column split with δ in place
+of `1/(16p²)`. The global Neumann ceiling is therefore exactly #4452's
+`U = 8p²(D−4)/(D−32p²)`, so all five exponents transfer verbatim.
+
+## Lemma B: any reading with a small excess
+
+Suppose every row and column off-sum of `|H|` is at most `(1 − g) + ρ`, with `ρ ≤ 1/(32p³)`. Then
+`1 − off ≥ (4p−1)/(32p³) ≥ 7/(64p²) > 1/(10p²)`. Hence:
+
+- `‖H^{−1}‖₂ < 10p²`, so `100p⁴ < p^{11}` gives spectral endpoint 11;
+- `10p² < p⁶` gives normalizer 6;
+- the series error `< 10p²·e^{−p²} < p⁶e^{−p²}` at length `p^{24}`;
+- bandwidth and agreement distance stay below `p^{26}`.
+
+Per entry, an absolute error `e ≤ 1/(64p⁴)` on the at most `2W` band entries of a row or column is
+enough. The downward reading has `ρ ≤ 2δ`, far inside this budget.
+
+**Why this matters.** #4442 noted that FINE-PRIME says "rounded Gaussian entries" where LOG-A says
+"downward". Under the coarser ceiling `16p² − 1`, an overshoot of one part in 64 already broke the
+argument at `p = 2`. Under δ, the exponents no longer depend on the direction of rounding. Any rounding
+with absolute error at most `1/(64p⁴)` per entry works. In particular FINE-PRIME's own
+`poly(p)·2^{−(C−o(1))p}` row and column perturbation works eventually, which matches the eventual
+status of the ideal gaps.
+
+**#4449's repair is not needed for these exponents.** The raw negative-exponential oracle output `z`,
+with `|z − n| < 2η` and `η = 2^{−32768p}`, has a per-row excess of at most `2(p−1)·2η`. That is far
+below `1/(32p³)`, and the verifier checks it for every `p` from 2 to 64. Downward repair (#4449) is still
+what gives the exact ceiling `U` of Lemma A.
+
+**Near-tightness at `p = 2`.** On this route the excess tolerance at `p = 2` lies in
+`(0.0091, 0.0092)`. The budget `1/(32p³) = 1/256` sits inside it.
+
+## Checks
+
+`verify.py` checks:
+
+- the pinned LOG-A, FINE-PRIME and downstream phrases;
+- the split identity, as a polynomial identity of degree at most 2 per variable, on a 3×3×3 grid
+  (which proves it identically);
+- Lemma A's ceiling and exponents, exactly for `p` in 2..64, at several within/across shares;
+- Lemma B's gap, `B`, endpoint, normalizer, per-entry budget and bandwidth, exactly for `p` in 2..64,
+  together with the all-`p` inequalities `70 > 64`, `100 < p⁷` and `10 < p⁴`;
+- the `p = 2` tolerance interval.
+
+| | value |
+| --- | --- |
+| global ceiling, downward reading, `p = 2` | `U = 32.000…` (just above 32) |
+| robust excess budget | `1/(32p³)` per row or column |
+| per-entry budget | `1/(64p⁴)` |
+| `p = 2` tolerance | in `(0.0091, 0.0092)` |
+
+## Not covered
+
+- The ideal gaps `1/(8p²)`.
+- Whether an existing page generator implements either rounding.
+- The Schur complement and the core exponent 400.
+- The #4100 notes, which keep 20, 42, 45, 48 and 100.
+- Any new κ.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/delta-cross-cell-transfer --check-only
+python3.12 -B scripts/research_package.py --package research/delta-cross-cell-transfer
+```
+
+The verifier prints `PASS_DELTA_CROSS_CELL_TRANSFER` in about 45 seconds, using only the standard
+library.
+
+## Open next questions
+
+1. **Do the smaller exponents propagate through the Schur complement?**
+   - *Why it matters:* the core exponent 400 still dominates the agreement distance 26.
+   - *First step:* restate the interior elimination's row-dominance gap with `B < 10p²` in place of
+     `16p² − 1`.
+
+## Credit
+
+- The column split, the exponent route and the question are James Reed's (jwr404: #4442, #4451,
+  #4452).
+- The across-cell rounding contract is mihir-s-05's (#4449).
+- The source sentences come from LOG-A, FINE-PRIME and the downstream phase-cell report.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/delta-cross-cell-transfer/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "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": "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md",
+      "usage": "input",
+      "git_blob": "d72345a0aa748443c4efcddf87aa10d524664841",
+      "sha256": "3cdf492bcb719db4295658604dc202d6a2c5a008b87de43ec54f0107c64db730"
+    },
+    {
+      "path": "research/capped-fusion-t74-k554/vendor/pr1786/FINE-PRIME-PADDING.md",
+      "usage": "input",
+      "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3",
+      "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce"
+    },
+    {
+      "path": "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md",
+      "usage": "input",
+      "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73",
+      "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272"
+    }
+  ]
+}

research/delta-cross-cell-transfer/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": "Transfer #4452's within-cell delta exponents 11, 24, 26, 26, 6 to the banded reference across cells, and show they survive FINE-PRIME's 'rounded' reading.",
+  "scope_change_reason": "Open question of #4452 and #4460.",
+  "bottleneck_link": "Side result on the #4100 precision/conditioning obligation: removes the rounding-direction dependence of the halo exponents.",
+  "budget_minutes": 45,
+  "stop_rule": "Stop at the banded reference; Schur complement out of scope.",
+  "outcome": "completed",
+  "evidence": "Downward reading: off(H) <= (1-g)/(1-delta), global ceiling U, exponents transfer. Any reading with row/column excess <= 1/(32p^3) (per entry 1/(64p^4)): ||H^-1|| < 10p^2 and all five exponents hold. Exact for p=2..64; p=2 tolerance in (0.0091, 0.0092).",
+  "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": "Do the smaller exponents propagate through the Schur complement?",
+      "why_it_matters": "The core exponent 400 still dominates.",
+      "first_step": "Restate the interior elimination's row-dominance gap with B < 10p^2.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/delta-cross-cell-transfer/VERIFY.json

@@ -0,0 +1,22 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md",
+    "research/capped-fusion-t74-k554/vendor/pr1786/FINE-PRIME-PADDING.md",
+    "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Across-cell transfer of #4452's delta exponents: split identity (polynomial, grid-proved), global ceiling U under the downward reading, robust lemma (excess <= 1/(32p^3) gives ||H^-1|| < 10p^2, exponents 11/24/26/26/6) exactly for p=2..64 plus all-p inequalities, p=2 tolerance interval; pinned LOG-A/FINE-PRIME/downstream phrases."
+    }
+  ]
+}

research/delta-cross-cell-transfer/verify.py

@@ -0,0 +1,101 @@
+#!/usr/bin/env python3
+"""Across-cell transfer of the delta halo exponents 11, 24, 26, 26, 6 (#4452), and robustness to the rounded reading.
+
+Setting (#4442/#4452): banded reference H, diagonal exactly one, bandwidth W <= p-1, ideal Gaussian matrix N with
+row and column off-sums T <= 1 - g, g = 1/(8p^2). Within-cell entries obey |H| <= N/(1-delta), delta = 2^(2-32760p).
+  (A) Downward reading (LOG-A, #4449: 0 <= H <= n across cells). Split T = T_in + T_out:
+        off(H) <= T_in/(1-delta) + T_out <= T/(1-delta) <= (1-g)/(1-delta),
+      because (1-delta)[T_in/(1-delta) + T_out] - T = -delta T_out. So the global Neumann ceiling is #4452's
+      U = 8p^2(D-4)/(D-32p^2) and the five exponents transfer verbatim.
+  (B) Any reading with excess rho: if every row and column off-sum of |H| is at most (1-g) + rho with
+      rho <= 1/(32p^3), then 1 - off >= (4p-1)/(32p^3) >= 7/(64p^2) > 1/(10p^2), so ||H^-1||_2 < 10p^2 with 100p^4 < p^11
+      and B < p^6: endpoint 11, length 24, bandwidth/agreement 26 and normalizer 6 hold. Per entry, an absolute
+      error e <= 1/(64p^4) on the <= 2W band entries suffices. The downward reading has rho <= 2 delta.
+Exact rational checks for p = 2..64; the split identity is a polynomial identity of degree <= 2 per variable, checked
+on a 3x3x3 grid (hence identically). The tolerance is near-tight at p = 2 on this route.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from fractions import Fraction as F
+import hashlib
+import itertools
+import json
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+PMAX = 64
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def pins():
+    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"])
+    loga = (ROOT / "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md").read_text(encoding="utf-8")
+    fine = (ROOT / "research/capped-fusion-t74-k554/vendor/pr1786/FINE-PRIME-PADDING.md").read_text(encoding="utf-8")
+    down = (ROOT / "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md").read_text(encoding="utf-8")
+    need("across cells, use the retained downward Gaussian entries; set H_jj=1." in loga, "LOG-A downward phrase")
+    need("across cells use rounded\nGaussian entries, with diagonal exactly one." in fine, "FINE-PRIME rounded phrase")
+    need("poly(p) 2^(-(C-o(1))p)` in row and column norm" in fine, "FINE-PRIME perturbation phrase")
+    need("Set P=32768p and eta=2^(-P)." in down, "downstream precision")
+
+
+def split_identity():
+    # (1-d)[a/(1-d) + (t-a)] - t + d(t-a) == 0 as a polynomial in (a, t, d), degree <= 2 in each variable
+    vals = [F(1, 7), F(2, 5), F(3, 4)]
+    for a, t, d in itertools.product(vals, repeat=3):
+        need((1 - d) * (a / (1 - d) + (t - a)) - t + d * (t - a) == 0, "split identity")
+
+
+def downward(p):
+    D = 2 ** (32760 * p)
+    delta, g = F(4, D), F(1, 8 * p * p)
+    U = F(8 * p * p * (D - 4), D - 32 * p * p)
+    for t_in_share in (F(0), F(1, 3), F(1)):
+        T = 1 - g
+        off = t_in_share * T / (1 - delta) + (1 - t_in_share) * T
+        need(off <= T / (1 - delta) and 1 / (1 - off) <= U, "A: global ceiling is U")
+    need(U * U < p ** 11 and U < p ** 6 and T / (1 - delta) < 1, "A: exponents 11 and 6")
+    need(T / (1 - delta) - T <= 2 * delta <= F(1, 32 * p ** 3), "downward excess within the robust budget")
+    return U
+
+
+def robust(p):
+    g, rho = F(1, 8 * p * p), F(1, 32 * p ** 3)
+    off = 1 - g + rho
+    need(off < 1 and 1 - off == F(4 * p - 1, 32 * p ** 3) >= F(7, 64 * p * p) > F(1, 10 * p * p), "B: gap")
+    B = 1 / (1 - off)
+    need(B * B < p ** 11 and B < p ** 6 and B < 10 * p * p and 100 * p ** 4 < p ** 11 and 10 * p * p < p ** 6, "B: endpoint 11, normalizer 6")
+    need(2 * (p - 1) * F(1, 64 * p ** 4) <= rho, "B: per-entry error 1/(64p^4)")
+    # the raw exponential oracle (|z - n| < 2 eta, eta = 2^-32768p, no downward repair) on <= 2W = 2(p-1) entries
+    need(2 * (p - 1) * 2 * F(1, 2 ** (32768 * p)) <= rho, "B: raw oracle output fits the budget")
+    L = p ** 24
+    need((2 * L - 1) * (p - 1) < p ** 26 and (2 * L + 1) * (p - 1) < p ** 26, "bandwidth/agreement 26")
+
+
+def main():
+    pins()
+    split_identity()
+    for p in range(2, PMAX + 1):
+        U = downward(p)
+        robust(p)
+        if p == 2:
+            U2 = U
+    # all p >= 2: (4p-1)/p >= 7/2; 70 > 64; 100 < p^7 and 10 < p^4 for p >= 2
+    need(2 * (4 * 2 - 1) >= 7 * 2 and 70 > 64 and 100 < 2 ** 7 and 10 < 2 ** 4, "B for all p >= 2")
+    # near-tightness at p = 2: the exponent-11 route needs (1 - off)^2 * 2^11 > 1 with off = 31/32 + rho
+    ok = lambda rho: (1 - (F(31, 32) + rho)) ** 2 * 2 ** 11 > 1
+    need(ok(F(91, 10000)) and not ok(F(92, 10000)), "p = 2 tolerance lies in (0.0091, 0.0092)")
+    need(F(1, 256) < F(91, 10000), "the budget 1/(32p^3) = 1/256 at p = 2 is within it")
+    print(json.dumps({"status": "PASS_DELTA_CROSS_CELL_TRANSFER", "exact_p_range": [2, PMAX],
+                      "downward_global_ceiling_U_p2": f"{float(U2):.12f}", "robust_excess_budget": "1/(32p^3)",
+                      "per_entry_budget": "1/(64p^4)", "p2_tolerance_interval": [0.0091, 0.0092],
+                      "exponents": [11, 24, 26, 26, 6], "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())