Independently check #4451/#4452: within-cell halo exponents 11, 24, 26, 26, 6 under delta (no new κ)

research/delta-halo-exponent-check/README.md

@@ -0,0 +1,81 @@
+# Independent check of #4451 and #4452: the halo exponents 11, 24, 26, 26 and 6 inside one cell
+
+**Claim type:** an independent check of conditional exponent arithmetic, by a separate proof route
+plus exact rational arithmetic. **No new κ.** It covers jwr404's
+[#4451](https://github.com/CrocSwap/integer-mult-bounds/pull/4451) (head `be243a28`) and
+[#4452](https://github.com/CrocSwap/integer-mult-bounds/pull/4452) (head `af68f597`). The ideal gaps
+`1/(8p²)` stay hypotheses.
+
+## What is checked
+
+Notation: `D = 2^{32760p}`, `δ = 4/D`, `g = 1/(8p²)`, `η = 2^{−32768p}`.
+
+1. **(R) Relative-error repair (#4451).** From `a − 4η < â ≤ a` and `a > 2^{−8p}`, we get
+   `a/â < 1/(1 − 4η·2^{8p}) = 1/(1 − δ)`. Also `δ < 1/(16p²)`.
+2. **(N) Neumann ceiling.** The identity `(1 − δ)/(g − δ) = U = 8p²(D − 4)/(D − 32p²)` is checked
+   exactly. Also the rounded off-sum `(1 − g)/(1 − δ)` is below 1, so the absolute sums are below 2.
+3. **(B) The U chain, for all `p ≥ 2`, by a route different from the PRs'.** From `p < 2^p` we get
+   `512p⁴ < 2^{4p+9} ≤ D`, so `r = 32p²/D < 1/(16p²)`. With `V = 8p²/(1 − r)`:
+
+       8p² < U < V < 8p² + 1 ≤ 16p² − 1 < p⁶,      V² < (8p² + 1)² < p^{11}.
+
+   The last step is `1089 < 2048` at `p = 2`, and `(8p²+1)² ≤ 81p⁴ ≤ p⁸` for `p ≥ 3`.
+4. **(S) Neumann polynomial.** `P − A^{−1} = −Q^L A^{−1}` and `‖Q‖ < 1 − p^{−22}`, so the error is
+   below `U·e^{−p^{−22}L}`. At `L = p^{24}` that is `U·e^{−p²} < p⁶e^{−p²}`. The bandwidth is
+   `(2L ± 1)(p − 1) < p^{26}`.
+5. **Exact replay.** Every inequality in 1–4 is checked with `Fraction` for each `p` from 2 to 64.
+6. **The "fails" column at `p = 2`.**
+   - `U > 32 = p⁵`, so normalizer 5 and spectral endpoint 10 fail.
+   - Length `p^{23}` fails on this route, by the certified lower bound `(1−x)^L ≥ e^{−xL−x²L}`.
+   - The loose radius `2p^{24} + 1` exceeds `p^{25}`.
+
+| Role | #4452 | Confirmed |
+| --- | ---: | --- |
+| Spectral endpoint | 11 | yes; 10 fails at `p = 2` |
+| Series length | 24 | yes; 23 fails at `p = 2` |
+| Bandwidth | 26 | yes; 25 fails (loose count at `p = 2`, sharp count for `p ≥ 3`) |
+| Agreement distance | 26 | yes |
+| Normalizer | 6 | yes; 5 fails at `p = 2` |
+
+## Remarks
+
+- **The sharp count at `p = 2` is below `p^{25}`.** The sharp bandwidth count is `2^{25} − 1`, so
+  "25 fails" at `p = 2` holds only for the loose count `(2p^{24}+1)W`. For `p ≥ 3`, the sharp count
+  exceeds `p^{25}`, so the uniform conclusion is unchanged. #4452's text already says this, and the
+  verifier records it explicitly.
+- **#4452 relies on `Ĝ_0 = 1`.** The Neumann step needs the unit diagonal. #4452's lemma states only
+  `0 ≤ Ĝ ≤ G`, but `Ĝ_0 = 1` is inherited from #4438/#4439. A future write-up should restate it.
+- **"Smallest" is relative to this proof route.** The failures are failures of the stated
+  majorant route, not lower bounds for the actual block.
+
+## Not covered
+
+- The ideal gaps `1/(8p²)` for every prime.
+- Across-cell entries (#4449, #4442).
+- Any new κ.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/delta-halo-exponent-check --check-only
+python3.12 -B scripts/research_package.py --package research/delta-halo-exponent-check
+```
+
+The verifier prints `PASS_DELTA_HALO_EXPONENT_CHECK` in about 20 seconds, using only the standard
+library.
+
+## Open next questions
+
+1. **Do 11, 24, 26, 26 and 6 survive across a cell?**
+   - *Why it matters:* this is #4452's own open question, and the global reference still uses
+     20, 42, 45, 48 and 100.
+   - *First step:* #4442's column split with `δ` in place of `1/(16p²)`, using #4449's `0 ≤ H ≤ n`.
+
+## Credit
+
+- The lemmas, exponents and proofs are James Reed's (jwr404, #4451 and #4452, building on #4438 and
+  #4439).
+- The downward rounding contract is in the pinned downstream phase-cell report.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/delta-halo-exponent-check/SOURCES.json

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

research/delta-halo-exponent-check/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": "Independently check the within-cell delta exponent arithmetic of #4451 and #4452 (11, 24, 26, 26, 6) by a separate proof route and exact rational replay.",
+  "scope_change_reason": "Independent audit of two open author-checked precision/conditioning steps.",
+  "bottleneck_link": "Side result: an independent check of one precision/conditioning step under the #4100 transfer obligations.",
+  "budget_minutes": 40,
+  "stop_rule": "Stop at the within-cell arithmetic; across-cell transfer is out of scope.",
+  "outcome": "completed",
+  "evidence": "All #4452 inequalities hold for all p>=2 via p<2^p (r=32p^2/D<1/(16p^2)) and exactly for p=2..64; each 'fails' entry confirmed at p=2. Remarks: the sharp bandwidth count at p=2 is 2^25-1 (only the loose count fails there); Ghat_0=1 is inherited from #4438.",
+  "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 11, 24, 26, 26 and 6 survive across a cell?",
+      "why_it_matters": "The global reference still uses 20, 42, 45, 48 and 100.",
+      "first_step": "#4442's column split with delta in place of 1/(16p^2), using #4449's 0<=H<=n.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/delta-halo-exponent-check/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md",
+    "research/unconditional-batched-crt/HALO.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Independent check of #4451/#4452: delta repair, exact Neumann ceiling identity U, the chain 8p^2<U<V<8p^2+1<=16p^2-1<p^6 and V^2<p^11 for all p>=2 (separate route) and exactly for p=2..64, series error at L=p^24, bandwidth <p^26, and every 'fails' entry at p=2."
+    }
+  ]
+}

research/delta-halo-exponent-check/verify.py

@@ -0,0 +1,102 @@
+#!/usr/bin/env python3
+"""Independent check of #4451 and #4452: within-cell halo exponents under delta = 2^(2-32760p).
+
+Separate route from the PRs' polynomial certificates. Write D = 2^(32760p), delta = 4/D, g = 1/(8p^2).
+  (R) a - 4eta < ahat <= a, a > 2^-8p, eta = 2^-32768p  =>  a/ahat < 1/(1-delta).
+  (N) Neumann ceiling (1-delta)/(g-delta) equals U = 8p^2(D-4)/(D-32p^2) (exact identity).
+  (B) For all p >= 2, p < 2^p gives 512 p^4 < 2^(4p+9) <= D, so r = 32p^2/D < 1/(16p^2), and with
+      V = 8p^2/(1-r):  8p^2 < U < V < 8p^2 + 1 <= 16p^2 - 1 < p^6, and V^2 < (8p^2+1)^2 < p^11.
+  (S) Neumann polynomial P = p^-11 sum_{j<L} Q^j A*: P - A^-1 = -Q^L A^-1, |Q| < 1 - p^-22,
+      so the error is < U (1-p^-22)^L <= U exp(-p^-22 L) < p^6 exp(-p^2) at L = p^24.
+Every comparison is also checked by exact rational arithmetic for p = 2..64, and each "fails" entry at
+p = 2 (or p = 3) is checked with certified bounds. Ryanson Jonathan with Claude Code (Claude Opus 5.5)
+assistance. Apache-2.0.
+"""
+from fractions import Fraction as F
+import hashlib
+import json
+import math
+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"])
+    down = (ROOT / "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md").read_text(encoding="utf-8")
+    for phrase in ("Set P=32768p and eta=2^(-P).", "2^(-8p)<a_j<=1.", "absolute error below four eta"):
+        need(phrase in down, f"pinned phrase {phrase!r}")
+
+
+def exact(p):
+    D = 2 ** (32760 * p)
+    delta, g = F(4, D), F(1, 8 * p * p)
+    eta, floor_a = F(1, 2 ** (32768 * p)), F(1, 2 ** (8 * p))
+    # (R): worst case a -> 2^-8p, ahat -> a - 4 eta
+    need(4 * eta / floor_a == delta and delta < 1, "R: 4 eta / 2^-8p = delta")
+    need(delta < F(1, 16 * p * p), "#4451: delta < 1/(16p^2)")
+    U = F(8 * p * p * (D - 4), D - 32 * p * p)
+    V = F(8 * p * p * D, D - 32 * p * p)
+    need((1 - delta) / (g - delta) == U, "N: Neumann ceiling identity")
+    need((1 - g) / (1 - delta) < 1, "rounded off-sum < 1, absolute sums < 2")
+    need(8 * p * p < U < V < 8 * p * p + 1 <= 16 * p * p - 1 < p ** 6, "B: U chain")
+    need(V * V < p ** 11, "B: V^2 < p^11")
+    need(U * U < p ** 11 and 4 < p ** 11, "spectrum of A*A inside (p^-11, p^11)")
+    L = p ** 24
+    need((2 * L - 1) * (p - 1) < p ** 26 and (2 * L + 1) * (p - 1) < p ** 26, "bandwidth/agreement < p^26")
+    return U
+
+
+def series_error_ok(p, length_exp):
+    """certified: U*(1-x)^L < p^6 exp(-p^2) with x = p^-22, L = p^length_exp; uses (1-x)^L <= exp(-xL)"""
+    xL = F(p ** length_exp, p ** 22)
+    U_upper = 8 * p * p + 1
+    # need log(U_upper) - xL < 6 log p - p^2, i.e. xL - p^2 > log(U_upper / p^6) (negative RHS)
+    return xL - p * p > math.log(U_upper / p ** 6) + 1e-9
+
+
+def series_error_fails(p, length_exp):
+    """certified failure of the bound route: U*(1-x)^L >= p^6 exp(-p^2), using (1-x)^L >= exp(-xL - x^2 L)"""
+    x = F(1, p ** 22)
+    L = p ** length_exp
+    lower_exp = x * L + x * x * L
+    U_lower = 8 * p * p
+    return math.log(U_lower / p ** 6) - float(lower_exp) > -p * p + 1e-9
+
+
+def main():
+    pins()
+    for p in range(2, PMAX + 1):
+        U = exact(p)
+        if p == 2:
+            U2 = U
+    # general p >= 2 by p < 2^p (B): 512 p^4 < 2^(4p+9) <= 2^(32760p) = D
+    need(all(p < 2 ** p for p in range(2, 200)), "p < 2^p sample")  # induction: 2^(p+1) = 2*2^p > 2p >= p+1
+    need(4 * 2 + 9 <= 32760 * 2 and 32760 - 4 > 0, "4p+9 <= 32760p for p >= 2")
+    # with r < 1/(16p^2): V = 8p^2/(1-r) < 8p^2 (1 + 2r) < 8p^2 + 1; 8p^2 + 1 <= 16p^2 - 1 iff p^2 >= 1/4;
+    # 16p^2 - 1 < p^6 iff p^4 >= 16; (8p^2+1)^2 < p^11: p = 2 gives 1089 < 2048, p >= 3 gives <= 81 p^4 <= p^8.
+    need(33 ** 2 < 2 ** 11 and 64 + 16 + 1 <= 81 <= 3 ** 4, "V^2 < p^11 for all p")
+    # Neumann series error at L = p^24 holds; lengths and endpoints one lower fail on this route at p = 2
+    need(all(series_error_ok(p, 24) for p in range(2, PMAX + 1)), "S: error < p^6 exp(-p^2) at L = p^24")
+    need(series_error_fails(2, 23), "series length 23 fails at p = 2")
+    need(U2 > 2 ** 5 and U2 * U2 > 2 ** 10, "endpoint 10 and normalizer 5 fail at p = 2")
+    need((2 * 2 ** 24 + 1) * 1 > 2 ** 25, "loose radius exceeds p^25 at p = 2")
+    need(all((2 * p ** 24 - 1) * (p - 1) > p ** 25 for p in range(3, PMAX + 1)), "sharp radius exceeds p^25, p >= 3")
+    need((2 * 2 ** 24 - 1) * 1 < 2 ** 25, "sharp radius stays below p^25 at p = 2 (only the loose count fails)")
+    print(json.dumps({"status": "PASS_DELTA_HALO_EXPONENT_CHECK", "exact_p_range": [2, PMAX],
+                      "exponents": {"spectral_endpoint": 11, "series_length": 24, "bandwidth": 26,
+                                    "agreement_distance": 26, "normalizer": 6},
+                      "U_at_p2": f"{float(U2):.12f}", "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())