Answer #4356's open question: the broad forward bound stays polynomial at theta = 1/(4p^2); actual blocks sit 1e-5..1e-6 below it and scale like theta^(-1/2) (no new κ)

research/forward-fine-theta-conditioning/README.md

@@ -0,0 +1,103 @@
+# Broad forward conditioning at the fine-prime θ
+
+**Claim type:** a written re-derivation of one θ-dependence, plus rigorous floating-point bounds
+on the actual phase-cell blocks at five primes. **No new κ.** It answers the open question of
+Matarener's [#4356](https://github.com/CrocSwap/integer-mult-bounds/pull/4356): does
+`FINE-PRIME.md` §2's conditioning bound stay polynomial at `θ = 1/(4p²)`?
+
+## Object
+
+`vendor/FINE-PRIME.md` reuses `FORWARD-SMALL-A-AUDIT.md` §1–2 at the smaller fine-prime θ:
+
+    ‖K⁻¹‖ ≤ α e^{3b/4} c_b^{-4} / (1 − e^{−bρθ})² = O(α⁵ ρ² θ⁻² e^{aρ/3}).
+
+Here `b = π/(α²ρ²)` and `c_b = Π(1 − e^{−2bρm})`. The blocks are
+`K_{k,i} = α⁻¹ exp(−b₀(i − λk − c)²)`, on a contiguous interval of one phase cell with
+`β'_k ∈ [−1/2, 1/2)`.
+
+## Re-derivation of the θ-dependence
+
+θ enters only through the reciprocal gap `1/(1 − e^{−bρθ})`. Since
+`x = bρθ = πθ/(α²ρ) < 1` and `1 − e^{−x} ≥ x/2` on `[0, 1]`, that gap is at most
+`2α²ρ/(πθ)`. The other factors do not involve θ:
+
+- `e^{3b/4} ≤ e^{3π/(4α²)}`;
+- `c_b^{-4} ≤ e^{aρ/3}`, by §1's logarithmic series bound.
+
+So the bound is
+
+    ‖K⁻¹‖ ≤ (4/π²) α⁵ ρ² e^{3π/(4α²)} e^{aρ/3} θ⁻²,
+
+valid for every θ in `(0, 1]`. At `θ = 1/(4p²)`, `θ⁻² = 16p⁴`. With `a ≤ 5 log(16p)`, the
+factor `e^{aρ/3}` is at most `(16p)^{5ρ/3}`, so the whole bound is polynomial in `p`. This is
+`FINE-PRIME.md`'s claim, and the answer to #4356's question is **yes**. The argument does not
+re-audit `BILATERAL-LDU.md`'s base inequality, whose θ-dependence §1 says is unchanged.
+
+## Measured norms
+
+`verify.py` builds the blocks at `p = 5, 7, 11, 13, 19`, with `α = 3` from the formula at all
+five. It covers three starting phases, `β'₀ ∈ {−1/2, −1/4, 0}`, and every dyadic length up to the
+whole remaining cell.
+
+For `‖K⁻¹‖_∞` and `‖K⁻¹‖₁` it gives rigorous upper bounds from float64 residuals. Those bounds
+use the standard `γ_{n+2}` rounding bound and fold in the error of each computed entry. The
+2-norm is a plain float value.
+
+| `p` | θ | ceiling | `‖K⁻¹‖_∞ ≤` | `‖K⁻¹‖₁ ≤` | `‖K⁻¹‖₂` | ratio |
+| --- | --- | --- | --- | --- | --- | --- |
+| 5 | 1/100 | 4.78e7 | 1505.9 | 1265.2 | 1092.8 | 3.2e-5 |
+| 7 | 1/196 | 1.76e8 | 2192.7 | 1702.4 | 1506.8 | 1.3e-5 |
+| 11 | 1/484 | 1.04e9 | 3643.3 | 2625.0 | 2367.4 | 3.5e-6 |
+| 13 | 1/676 | 2.02e9 | 4385.7 | 3094.1 | 2803.1 | 2.2e-6 |
+| 19 | 1/1444 | 9.14e9 | 6634.2 | 4513.2 | 4118.2 | 7.3e-7 |
+
+The ratio column is the larger rigorous norm divided by the ceiling. Every block is below its
+ceiling, and the worst block is always the longest one.
+
+**Scaling.** At fixed `α = 3`, with a whole cell starting at `β' = −1/2`, `‖K⁻¹‖₂·√θ` stays
+between 107.5 and 109.3 for θ from 1/100 to 1/3200. The verifier enforces that this ratio varies
+by less than 5%. So on these blocks the true dependence is about `θ^{−1/2}`, not `θ⁻²`. At the
+fine-prime θ this means `O(p)` rather than `O(p⁴)`.
+
+This is an observation at `α = 3` only, not a proof. A plausible mechanism is a single turning
+point, where the local shift passes the symbol's zero at `|s| = 1/2`. That would give the
+`θ^{−1/2}` of an Airy-type layer.
+
+## Not covered
+
+- `BILATERAL-LDU.md`'s base inequality.
+- Values of `α ≥ 4`, which first occur at `p ≥ 74`, where a cell has more than 21,000
+  coordinates.
+- The narrow kernel. For that, see #4402's column gap.
+- Any change to #4100's guards. `FINE-PRIME.md`'s `p¹⁰` envelope already absorbs the ceiling.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/forward-fine-theta-conditioning --check-only
+python3.12 -B scripts/research_package.py --package research/forward-fine-theta-conditioning
+```
+
+The verifier prints `PASS_FORWARD_FINE_THETA_CONDITIONING` in about 20 seconds. It needs
+`numpy`.
+
+## Open next questions
+
+1. **Can `‖K⁻¹‖ = O_α(θ^{−1/2})` be proved?**
+   - *Why it matters:* it would replace `θ⁻²` by `θ^{−1/2}` in `FORWARD-SMALL-A-AUDIT.md`, which
+     saves about `p³` at the fine-prime θ.
+   - *First step:* bound the inverse of a Gaussian Toeplitz operator whose shift varies linearly
+     through `1/2`. A turning-point (WKB) estimate is the natural route.
+   - *Blocked by:* nothing.
+2. **Does the constant in `θ^{−1/2}` grow like `e^{aρ/3}` in `α`?**
+   - *First step:* repeat the scaling table at `α = 4` and `α = 5` on shortened cells.
+
+## Credit
+
+- The bound is from `FORWARD-SMALL-A-AUDIT.md`, PR1673 (Vlado Vojdanovski's capped-phase
+  papers).
+- Its fine-prime reuse is #4100's `vendor/FINE-PRIME.md` (Cinna Davis).
+- Matarener's #4356 posed the question.
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/forward-fine-theta-conditioning/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/capped-phase-fusion/FORWARD-SMALL-A-AUDIT.md",
+      "usage": "input",
+      "git_blob": "0f7f80b3f74d469c2f72f3b9f338d32568b4eae3",
+      "sha256": "e37aaa30b15671a1dff00676b14572213efaaac99df202dbba5e09f57af487c0"
+    },
+    {
+      "path": "research/unconditional-batched-crt/vendor/FINE-PRIME.md",
+      "usage": "input",
+      "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3",
+      "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce"
+    }
+  ]
+}

research/forward-fine-theta-conditioning/TASK.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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": "Answer #4356's open question: re-derive the theta-dependence of FORWARD-SMALL-A-AUDIT sections 1-2 as used by FINE-PRIME.md at theta=1/(4p^2), and bound the actual broad forward block inverses there.",
+  "scope_change_reason": "The card asks for one quantified #4100 precision/conditioning step; #4356 left this one open.",
+  "bottleneck_link": "FINE-PRIME.md's p^10 conditioning envelope relies on this bound at the fine-prime theta.",
+  "budget_minutes": 40,
+  "stop_rule": "Stop at the re-derivation and the measured table; do not re-audit BILATERAL-LDU.",
+  "outcome": "completed",
+  "evidence": "verify.py: every block at p=5..19 (alpha=3) has rigorous ||K^-1||_inf,1 below the ceiling by a factor 3e-5..7e-7; ||K^-1||_2 sqrt(theta) = 107.5..109.3 for theta=1/100..1/3200.",
+  "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": "Can ||K^-1|| = O_alpha(theta^(-1/2)) be proved?",
+      "why_it_matters": "It would save about p^3 at the fine-prime theta in FORWARD-SMALL-A-AUDIT's bound.",
+      "first_step": "A turning-point estimate for a Gaussian Toeplitz operator whose shift passes 1/2 linearly.",
+      "blocked_by": "None."
+    },
+    {
+      "question": "How does the theta^(-1/2) constant grow with alpha?",
+      "why_it_matters": "alpha grows like sqrt(log p).",
+      "first_step": "Repeat the scaling at alpha=4,5 on shortened cells.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/forward-fine-theta-conditioning/VERIFY.json

@@ -0,0 +1,23 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [
+    "numpy==1.26.4"
+  ],
+  "inputs": [
+    "research/capped-phase-fusion/FORWARD-SMALL-A-AUDIT.md",
+    "research/unconditional-batched-crt/vendor/FINE-PRIME.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Pinned FORWARD-SMALL-A-AUDIT and FINE-PRIME phrases; actual phase-cell blocks at p=5,7,11,13,19, theta=1/(4p^2), three starting phases, dyadic lengths to the full cell: rigorous float-residual upper bounds of ||K^-1||_inf and ||K^-1||_1 below the audit ceiling; theta^(-1/2) scaling of ||K^-1||_2 at alpha=3 within 5%."
+    }
+  ]
+}

research/forward-fine-theta-conditioning/verify.py

@@ -0,0 +1,115 @@
+#!/usr/bin/env python3
+"""Broad forward phase-cell blocks at the fine-prime theta: rigorous inverse-norm bounds vs FORWARD-SMALL-A-AUDIT.
+
+FINE-PRIME.md reuses FORWARD-SMALL-A-AUDIT.md sections 1-2,
+    ||K^-1|| <= alpha exp(3b/4) c_b^-4 / (1 - exp(-b rho theta))^2 = O(alpha^5 rho^2 theta^-2 exp(a rho/3)),
+at theta = 1/(4p^2). For p in PRIMES, alpha = ceil(sqrt((4/pi) log(16p))), it builds the actual blocks
+K_(k,i) = alpha^-1 exp(-b0 (i - lambda k - c)^2) on contiguous intervals inside one phase cell
+(beta'_k = theta k - rho c in [-1/2, 1/2)), inverts them in float64 and bounds ||K^-1||_inf and ||K^-1||_1
+rigorously from float residuals with the standard gamma_n rounding bound. It checks every bound against
+the audit's ceiling and records how the true norm scales with theta.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+import hashlib
+import json
+import math
+from pathlib import Path
+import sys
+
+import numpy as np
+
+ROOT = Path(__file__).resolve().parents[2]
+PINS = {
+    "research/capped-phase-fusion/FORWARD-SMALL-A-AUDIT.md":
+        ("`||K^-1|| <= alpha exp(3b/4) c_b^-4/(1-exp(-b rho theta))^2`",
+         "`c_b^-4 <= exp(pi alpha^2 rho/3)=exp(a rho/3)`"),
+    "research/unconditional-batched-crt/vendor/FINE-PRIME.md":
+        ("||K^-1|| <= O(alpha^5 rho^2 theta^-2 exp(a rho/3)).",),
+}
+PRIMES = (5, 7, 11, 13, 19)
+STARTS = (-0.5, -0.25, 0.0)
+U = 2.0 ** -53
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def ceiling(alpha, theta):
+    rho = 1 + theta
+    b = math.pi / (alpha ** 2 * rho ** 2)
+    log_cb = sum(math.log1p(-math.exp(-2 * b * rho * m)) for m in range(1, 20000))
+    return alpha * math.exp(3 * b / 4) * math.exp(-4 * log_cb) / (-math.expm1(-b * rho * theta)) ** 2
+
+
+def block(alpha, theta, n, beta_start):
+    rho = 1 + theta
+    lam, b0 = 1 / rho, math.pi / alpha ** 2
+    c = -beta_start / rho                       # beta'_0 = theta*0 - rho c = beta_start
+    k = np.arange(n, dtype=float)
+    arg = b0 * (k[None, :] - lam * k[:, None] - c) ** 2
+    kmat = np.exp(-arg) / alpha
+    # relative entry error: exponent argument error <= arg * 8u, exp and division <= 3u
+    rel = arg.max() * 8 * U + 3 * U
+    return kmat, rel
+
+
+def rigorous_norms(kmat, rel):
+    """upper bounds of ||K^-1||_inf and ||K^-1||_1 for the true K with |K - kmat| <= rel |kmat|"""
+    n = kmat.shape[0]
+    x = np.linalg.inv(kmat)
+    g = (n + 2) * U / (1 - (n + 2) * U)
+    ax, ak = np.abs(x), np.abs(kmat)
+    out = []
+    for left in (True, False):
+        r = np.eye(n) - (x @ kmat if left else kmat @ x)
+        prod = ax @ ak if left else ak @ ax
+        rmat = np.abs(r) + g * (prod + np.eye(n)) + rel * prod * (1 + g)
+        norm = (lambda m: m.sum(1).max()) if left else (lambda m: m.sum(0).max())
+        rr = norm(rmat)
+        need(rr < 0.5, "residual small")
+        nx = norm(ax) * (1 + g)
+        out.append(nx / (1 - rr))
+    return out[0], out[1], float(np.linalg.norm(x, 2))
+
+
+def main():
+    for path, phrases in PINS.items():
+        text = (ROOT / path).read_text(encoding="utf-8")
+        for phrase in phrases:
+            need(phrase in text, f"{path}: {phrase}")
+    rows, scaling = [], []
+    for p in PRIMES:
+        theta = 1 / (4 * p * p)
+        alpha = math.ceil(math.sqrt((4 / math.pi) * math.log(16 * p)))
+        ceil_val = ceiling(alpha, theta)
+        need(ceil_val < 16 * p ** 4 * alpha ** 5 * math.exp(math.pi * alpha ** 2 * (1 + theta) / 3) * 10,
+             "ceiling has the stated alpha^5 theta^-2 exp(a rho/3) shape")
+        worst = [0.0, 0.0, 0.0]
+        cell = int(round(1 / theta))
+        for beta_start in STARTS:
+            span = int(math.floor((0.5 - beta_start) / theta))   # beta' stays below 1/2
+            lengths = sorted({min(span, 2 ** j) for j in range(1, 12)} | {span})
+            for n in lengths:
+                kmat, rel = block(alpha, theta, n, beta_start)
+                inf_hi, one_hi, two = rigorous_norms(kmat, rel)
+                need(max(inf_hi, one_hi) < ceil_val, f"p={p}, n={n}: below the audit ceiling")
+                worst = [max(worst[0], inf_hi), max(worst[1], one_hi), max(worst[2], two)]
+        rows.append({"p": p, "alpha": alpha, "theta": f"1/{cell}", "ceiling": f"{ceil_val:.4g}",
+                     "inf_upper": f"{worst[0]:.2f}", "one_upper": f"{worst[1]:.2f}", "two": f"{worst[2]:.2f}",
+                     "ratio_to_ceiling": f"{max(worst[:2]) / ceil_val:.2e}"})
+    # theta-scaling at fixed alpha = 3, full cell from beta' = -1/2
+    for inv_theta in (100, 200, 400, 800, 1600, 3200):
+        theta = 1 / inv_theta
+        kmat, rel = block(3, theta, inv_theta, -0.5)
+        _, _, two = rigorous_norms(kmat, rel)
+        scaling.append({"inv_theta": inv_theta, "two": f"{two:.2f}", "two_times_sqrt_theta": f"{two * theta ** 0.5:.3f}"})
+    s = [float(r["two_times_sqrt_theta"]) for r in scaling]
+    need(max(s) / min(s) < 1.05, "||K^-1||_2 sqrt(theta) constant within 5% over theta = 1/100 .. 1/3200")
+    print(json.dumps({"status": "PASS_FORWARD_FINE_THETA_CONDITIONING", "primes": rows,
+                      "theta_scaling_alpha3": scaling, "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())