diff --git a/research/one-factor-of-t/README.md b/research/one-factor-of-t/README.md new file mode 100644 index 0000000000..4f907fcc3f --- /dev/null +++ b/research/one-factor-of-t/README.md @@ -0,0 +1,91 @@ +# One factor of `T` on #4100's coefficient error path + +**Claim type:** a written ∞-norm error ledger, plus a fixed-point simulation of the normalized +synthetic convolution. **No new κ.** It answers open question 1 of unpaidmoon's +[#4371](https://github.com/CrocSwap/integer-mult-bounds/pull/4371): how many factors of `T` does one +coefficient pick up through `PROOF.md`'s three source transforms, the pointwise product and the +final `M` scale? + +#4371 showed that the literal "full array dimension in all norm changes" reading costs +`2^{Θ(p²)}`, while one factor of `T` allows `C = 5` for `b ≥ 13` and `C = 8` for `b ≥ 2`. + +## Ledger + +Measure every error in the sup norm over coefficients. For stages `L_k` with +`‖L_k‖_∞ ≤ λ_k` and rounding `ρ_k`, the final error is at most `Σ_k ρ_k Π_{j>k} λ_j`. The point is +that no downstream product contains `T` more than once. + +| Stage (`PROOF.md`) | `‖·‖_∞` on errors | Source of the bound | +| --- | --- | --- | +| CRT address map and the permutations `R`, `Q`, `P_s`, `P_t` | 1 | permutations | +| Chirp `a`, twist `y^k`, twiddles `y^E` | 1 | unimodular diagonals, plus truncation toward zero | +| Normalized butterflies `H0 = [[1,1],[1,−1]]/2` | 1 | row sums equal 1 | +| Ring products, divided by `r` | bounded | exact Kronecker packing on bounded data | +| Final `×M` inside one synthetic convolution | `M = T/r < 2^{p/6+2}` | `PROOF.md` | +| Completed normalized `S_gauss` and `D N⁻¹ C` | 1, times `2^γ` | dyadic normalization, with `γ = O(d log p) = o(p)` | + +The `D N⁻¹ C` contraction rests on row sums: `‖N⁻¹‖_∞ ≤ 1/δ` (`INVERSE-CONDITIONING.md`) and +`D ≤ e^{a/4}`. + +**The factor `M` touches only internal rounding.** As an exact map, the synthetic convolution +`w ↦ M·F_plus((F_minus a)(F_minus w)/r) = (a*w)/T` is a cyclic average of bounded data. It is an +∞-contraction, so errors already present in its inputs are **not** multiplied by `M`. Only rounding +made after its forward transforms is multiplied by `M`. That rounding is at most `c·ℓ·2^{−P}`, +because normalized levels average their errors. + +**Count.** Each of the three transforms (two forward, one inverse) contains one synthetic +convolution, in the middle map `Q F_t`. Its internal error is at most about `M·ℓ·2^{−P}`, then +passes through contractions and `2^γ`. The pointwise product `U·V1` is bilinear on bounded data, so +it adds errors rather than multiplying them. The contributions therefore add: + + final error ≲ 3·2^{2γ}·M·poly(p)·2^{−P}, + +which gives **`m = 1`**. With `P = Cp` and `M < 2^{p/6+2}`, #4371's one-factor table applies: +`C = 5` for `b ≥ 13`, and `C = 8` for `b ≥ 2`. + +## Simulation + +`verify.py` simulates the scalar case `r = 1` (`M = T`) with `P = 40`-bit truncation toward zero, +on random inputs of modulus below 1/4, for `T = 2^4..2^14`: + +- **Error bound.** The maximum error stays below `4·M·ℓ·2^{−P}`. +- **Ratio to `M·ℓ`.** `error/(M·ℓ·2^{−P})` falls from 0.68 to 0.34. +- **Ratio to `M²`.** `error/(M²·2^{−P})` falls from `1.7·10⁻¹` to `2.9·10⁻⁴`, so there is no second + factor of `T`. +- **Inputs.** An exact-map input perturbation of sup size `η` moves the output by at most `η`. + +## Not covered + +- **The effective row gap after truncation and rounding** (#4217). Until it holds, the + `D N⁻¹ C` row is conditional on it, as #4371 notes. +- **The internal rounding of `GAUSSIAN.md`'s circuits.** This ledger uses its claim that they are + contractions up to `2^γ`. +- **The ℓ² reading.** If a stage were only an ℓ²-contraction, each ℓ∞→ℓ² change would cost up to + `√T`. The ∞-norm row-sum bounds avoid any change of norm. +- **The final scaling** `S²·2^{2b+4}`. It is part of exact recovery, which `PROOF.md` budgets + separately. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/one-factor-of-t --check-only +python3.12 -B scripts/research_package.py --package research/one-factor-of-t +``` + +The verifier prints `PASS_ONE_FACTOR_OF_T` in about one second. It needs `numpy`. + +## Open next questions + +1. **Are `GAUSSIAN.md`'s completed circuit stages ∞-contractions with only `2^γ` growth, once + their internal rounding is included?** + - *Why it matters:* this is the remaining assumption in the ledger. + - *First step:* bound one shifted-interior circuit's prefix factors in the ∞-norm. + +## Credit + +- The construction and the sentence are Cinna Davis's (#4100). +- The failure of the product reading and the `C` table are unpaidmoon's (#4371). +- #4320 and #4311 are earlier audits of the same chain. + +Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. +Apache-2.0. diff --git a/research/one-factor-of-t/SOURCES.json b/research/one-factor-of-t/SOURCES.json new file mode 100644 index 0000000000..e6f5836a55 --- /dev/null +++ b/research/one-factor-of-t/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/unconditional-batched-crt/PROOF.md", + "usage": "input", + "git_blob": "406eb561cc8d6041ea3fba1a849653b654f2198c", + "sha256": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060" + } + ] +} diff --git a/research/one-factor-of-t/TASK.json b/research/one-factor-of-t/TASK.json new file mode 100644 index 0000000000..2c7fd028ef --- /dev/null +++ b/research/one-factor-of-t/TASK.json @@ -0,0 +1,74 @@ +{ + "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 #4371's open question 1: count the factors of T on one coefficient's error path through PROOF.md's transforms, product and M scale.", + "scope_change_reason": "The card asks for one quantified #4100 implication; #4371 reduced PROOF.md's 2^-4p sentence to this count.", + "bottleneck_link": "The working-precision constant C in P = Cp depends on this count.", + "budget_minutes": 30, + "stop_rule": "Stop at the ledger and the scalar simulation; do not audit GAUSSIAN circuit rounding.", + "outcome": "completed", + "evidence": "Written sup-norm ledger gives m = 1 (additive over the three transforms); simulation: error <= 4 M ell 2^-P with error/(M ell 2^-P) 0.68 -> 0.34 and error/(M^2 2^-P) 1.7e-1 -> 2.9e-4 over T = 2^4..2^14.", + "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": "Are GAUSSIAN.md's completed circuit stages sup-norm contractions up to 2^gamma including internal rounding?", + "why_it_matters": "It is the ledger's remaining assumption.", + "first_step": "Bound one shifted-interior circuit's prefix factors in the sup norm.", + "blocked_by": "None." + } + ] +} diff --git a/research/one-factor-of-t/VERIFY.json b/research/one-factor-of-t/VERIFY.json new file mode 100644 index 0000000000..55d43bd837 --- /dev/null +++ b/research/one-factor-of-t/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==1.26.4" + ], + "inputs": [ + "research/unconditional-batched-crt/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned PROOF.md phrases; fixed-point (P=40, truncation toward zero) normalized synthetic convolution for T=2^4..2^14: error <= 4 M ell 2^-P, error/(M^2 2^-P) -> 0, exact-map input perturbation not amplified." + } + ] +} diff --git a/research/one-factor-of-t/verify.py b/research/one-factor-of-t/verify.py new file mode 100644 index 0000000000..cc0b928c0f --- /dev/null +++ b/research/one-factor-of-t/verify.py @@ -0,0 +1,106 @@ +#!/usr/bin/env python3 +"""Factors of T on one coefficient's error path: fixed-point simulation of #4100's normalized synthetic convolution. + +PROOF.md computes (f*g)/(rM) as M F_plus((F_minus f)(F_minus g)/r) with normalized butterflies +H0 = [[1,1],[1,-1]]/2, truncation toward zero after each round, and an exact final multiplication by M = T/r. +The README's ledger says one coefficient's error is at most about M * (c ell) * 2^-P: the factor M multiplies +only rounding made inside the synthetic convolution, and errors already present in the inputs pass through a +contraction (a cyclic average of bounded data). This verifier simulates the scalar case r = 1 (so M = T) with +P-bit truncation for T = 2^4 .. 2^14 and checks: + * max error <= 4 * M * ell * 2^-P on every size (one factor of M, with a logarithmic level count); + * max error / (M * 2^-P) stays bounded while max error / (M^2 * 2^-P) -> 0 (no second factor of T); + * an exact-arithmetic input perturbation of sup size eta changes the output by at most eta (no M). +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +import hashlib +import json +from pathlib import Path +import sys + +import numpy as np + +ROOT = Path(__file__).resolve().parents[2] +PROOF = ROOT / "research/unconditional-batched-crt/PROOF.md" +PHRASES = ( + "Use the normalized simultaneous butterfly H0=[[1,1],[1,-1]]/2 from", + " M F_plus((F_minus f)(F_minus g)/r)=(f*g)/(rM)", + "It can amplify numerical error by M<2^p, already allowed in the error", + "all norm changes costs at most2^O(p), since T=2^Theta(p).", +) +P = 40 +rng = np.random.default_rng(4371) + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def trunc(z): + """truncate real and imaginary parts toward zero on the 2^-P grid""" + s = 2.0 ** P + return np.trunc(z.real * s) / s + 1j * np.trunc(z.imag * s) / s + + +def normalized_fft(x, sign): + """radix-2 decimation in time with H0 butterflies; every level divides by 2 and truncates""" + n = len(x) + ell = n.bit_length() - 1 + rev = np.array([int(format(i, f"0{ell}b")[::-1], 2) for i in range(n)]) + a = x[rev].astype(complex) + size = 2 + while size <= n: + half = size // 2 + w = trunc(np.exp(sign * 2j * np.pi * np.arange(half) / size)) + a = a.reshape(-1, size) + top, bot = a[:, :half], a[:, half:] * w + a = trunc(np.concatenate([(top + bot) / 2, (top - bot) / 2], axis=1)).reshape(-1) + size *= 2 + return a + + +def synthetic(f, g): + T = len(f) + uf, ug = normalized_fft(f, -1), normalized_fft(g, -1) + prod = trunc(uf * ug) # r = 1 + back = normalized_fft(prod, +1) + return back * T # exact multiplication by M = T + + +def exact(f, g): + T = len(f) + return np.fft.ifft(np.fft.fft(f) * np.fft.fft(g)) / T # (f*g)/T + + +def main(): + text = PROOF.read_text(encoding="utf-8") + for phrase in PHRASES: + need(phrase in text, f"PROOF.md phrase: {phrase}") + rows = [] + unit = 2.0 ** -P + for ell in range(4, 15): + T = 2 ** ell + worst = 0.0 + for _ in range(3): + f = (rng.uniform(-1, 1, T) + 1j * rng.uniform(-1, 1, T)) / 4 + g = (rng.uniform(-1, 1, T) + 1j * rng.uniform(-1, 1, T)) / 4 + err = np.abs(synthetic(f, g) - exact(f, g)).max() + worst = max(worst, err) + # input perturbation through the exact map: no factor of M + eta = 1e-6 + e = eta * np.exp(2j * np.pi * rng.uniform(0, 1, T)) + change = np.abs(exact(f + e, g) - exact(f, g)).max() + need(change <= eta * (1 + 1e-9), "input error is not amplified by M") + need(worst <= 4 * T * ell * unit, f"T=2^{ell}: error <= 4 M ell 2^-P") + rows.append({"T": T, "ell": ell, "err_over_unit": f"{worst / unit:.1f}", + "over_M_ell": f"{worst / (T * ell * unit):.4f}", + "over_M2": f"{worst / (T * T * unit):.2e}"}) + m_ratio = [float(r["over_M_ell"]) for r in rows] + m2_ratio = [float(r["over_M2"]) for r in rows] + need(max(m_ratio) < 4 and m2_ratio[-1] < m2_ratio[0] / 100, "one factor of M, not two") + print(json.dumps({"status": "PASS_ONE_FACTOR_OF_T", "precision_bits": P, "rows": rows, + "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())