Folder of the error-bound follow-up of 2026-09-24 (BRIEF.md, MISSION.md last section). Started 17:35 -0500; plan committed at ab0f8fa (DERIVATION s1), derivation, code and tests at 747487f.
What was done
- The two objects, made precise (DERIVATION s1.0, s2.1): ΔT_stored is
ta_prolate.delta_T_cellswith its defaults (A4); ΔT_nvec,exact uses the exact projections onto the first nvec modes and the window integral over all of ℝ. The s cutoff enters the stored object twice: in the window integral (E1) and in the projection itself (E2), because the Gram is taken on the s-grid. - Pieces that close, evaluated in arb for every stored build and cell (
eps_quad.py,eps_quad.json): E1 (Prop 2), E6 (Prop 5), E7 (Prop 6). - E2, stated as a proposition (Prop 3) with its numbers per build, and the measured evidence that the stored and exact projections really differ (
run_bound_quad.py,bound_quad_gram.json): at (80, 1200) the stored Gram of ζ has eigenvalues 0.0126 to 3.44 (at (80, 1600): 0.091 to 2.64), the leverages sum to 78.99 (A5), and replacing the stored Gram by the identity moves the Q_∞ part of ΔT by 3.8e−3 / 4.0e−3 / 4.2e−3 in spectral norm (c = 2.2 / 2.5 / 2.9, N = 8). The tail rows overshoot: Σ_n A_n²/(πS) = 3.38 at (80, 1200). - The cost of the closing route (
run_unit_cost.py,bound_quad_unit.json): 2.2e−5 s per arb phase and 2.2e−7 s per (s, w, mode) ball product at 106 bits, at a load average near 60; per build 2.2e4 core-seconds at (80, 1200), 7.2e5 at (280, 2266), 2.2e6 at (364, 3060), for the hats on the stored grid alone.
The checks the brief asked for (test_bound_quad.py)
- The measured S responses (two_adic/ s7b: 6.5e−4 for 1200 → 2400 and 1.1e−4 for 2400 → 4800 at 80 modes, 1.8e−4 for 4800 → 9600 at 160 modes, c = 2.2, N = 8), recomputed from
ta_gram_probe.json. The inequality a complete bound must meet is ε(S₁) + ε(S₂) ≥ ‖ΔT(S₁) − ΔT(S₂)‖₂ (triangle inequality through ΔT_exact at the same nvec); ε = +∞ meets it trivially. E1's bound alone also meets it, by a factor of at least 2, so the responses cannot show that E2 is needed: E2 is open because no argument here bounds it, not because a measurement exceeds the partial bound. This corrects section 1's plan, which expected the opposite (DERIVATION s2.9). - The QR route against the 256-bit reference (two_adic/ s10.3 A2, read from
ta_rho_check.json: deviations 6.8e−9, 1.4e−5, 6.5e−2, 0.21 at (80, S) for S = 300, 200, 150, 120, cond(F_z) 5.1e7 to 7.3e14). Prop 5 does not close at any of them, which is the direction the measurements require (the last two are of order 1e−1). Prop 5 is also tested against an enclosure of the exact ρ (arb, 256 bits) on a synthetic F with cond about 1e3, where it closes and dominates. - κ(S₀) of Prop 2 against the sampled window energy on |s| ∈ [S₀, 6S₀] (it dominates, and is within a factor 2 there); the stored s-grid sizes and Kmax against two_adic/ and checker/'s snapshot; no s-node within 1e−6 of a window frequency 2πn/L; the JSON equals what the module computes; the folder's text rules.
Reproduction
PYTHONPATH=$PWD <venv python> hunts/weil_propagation/c4_s2/bound_quad/eps_quad.py # seconds PYTHONPATH=$PWD <venv python> hunts/weil_propagation/c4_s2/bound_quad/run_bound_quad.py # 903 s at a load average of 60 to 80 PYTHONPATH=$PWD <venv python> hunts/weil_propagation/c4_s2/bound_quad/run_unit_cost.py # seconds PYTHONPATH=$PWD <venv python> -m pytest -q -n 2 hunts/weil_propagation/c4_s2/bound_quad
Nothing was run on Modal; modal/RUNS.md is untouched.