diff --git a/research/forward-fine-theta-conditioning/README.md b/research/forward-fine-theta-conditioning/README.md new file mode 100644 index 0000000000..8e2831a88a --- /dev/null +++ b/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. diff --git a/research/forward-fine-theta-conditioning/SOURCES.json b/research/forward-fine-theta-conditioning/SOURCES.json new file mode 100644 index 0000000000..c9e516f5b7 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/forward-fine-theta-conditioning/TASK.json b/research/forward-fine-theta-conditioning/TASK.json new file mode 100644 index 0000000000..7f904beb8c --- /dev/null +++ b/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." + } + ] +} diff --git a/research/forward-fine-theta-conditioning/VERIFY.json b/research/forward-fine-theta-conditioning/VERIFY.json new file mode 100644 index 0000000000..6f5cf2dd17 --- /dev/null +++ b/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%." + } + ] +} diff --git a/research/forward-fine-theta-conditioning/verify.py b/research/forward-fine-theta-conditioning/verify.py new file mode 100644 index 0000000000..48fdf11e4b --- /dev/null +++ b/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())