Answer #4371's open question 1: one coefficient's error path through #4100's transforms carries one factor of T (m = 1), so C = 5 suffices for b >= 13 (no new κ)

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.

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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."
+    }
+  ]
+}

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())