/teal-sea
teal-sea / zeta-labstate of record · compiled 02 Nov 2026 · revision b09fa4dd · source

Library · hunts/weil_propagation/c4_s2/bound_quad/BRIEF.md

Brief: bound_quad/, the quadrature, s cutoff, Gram and rounding errors of ΔT

1,459 words · 160 lines · source

You own hunts/weil_propagation/c4_s2/bound_quad/ and write nowhere else (except appending to c4_s2/modal/RUNS.md if you use Modal). Time box: 3 hours from your start. At the box, write RESULTS.md with what stands, commit, and finish.

Your job

Bound every error of ΔT_stored except the mode truncation, for a fixed mode count nvec: the s cutoff S (with the order-1/S tails), the w quadrature (Gauss panels on [1, 2^Kmax], the dyadic truncation at Kmax, the asymptotic 1/w tail series and its term count), the float64 mode data (η_n, ζ_n), the Gram step (ta_mellin.rho, QR since two_adic/ c3dca00), and float64 rounding in the assembly of the stored matrix. The target is ‖ΔT_nvec,exact − ΔT_stored‖ in spectral norm on the (2N+1)-dimensional space, where ΔT_nvec,exact is the same finite-mode object computed without any of these errors.

Two routes, pick by cost: (i) an a priori bound per source via arb enclosures of the integrands and derivative bounds for the Gauss rules, or (ii) an arb recomputation of ΔT_nvec itself as a ball matrix, giving eps = ‖center − stored‖ + radius. Route (ii) over about 140,000 w nodes and up to 364 modes will not fit locally: estimate one unit first (ask the coordinator, then append the estimate to modal/RUNS.md) before any batch. Mixed routes are fine; say which source each piece of your bound covers.

Milestones

  1. Plan, within 45 minutes. DERIVATION.md section 1: the list of sources above, for each the route and whether it closes, and a cost estimate from one measured unit. Commit; status message to the coordinator.
  2. Derivation, every assumption numbered. Commit and tell the coordinator: it goes to referee/.
  3. Enclosure code. eps_quad.py, eps_quad.json in the interface below, for every stored build at c ∈ {2.2, 2.5, 2.9}; INTERFACE.md; tests in test_bound_quad.py, including that the bound dominates the measured S responses (two_adic/ s7b: 6.5e−4, 1.1e−4 at 80 modes, 1.8e−4 at 160) and the QR-against-256-bit comparison of two_adic/ s10.3.
  4. RESULTS.md, first five lines: the bound per source, its values on the c = 2.9 builds, its grade, what is open.

The question (shared by all four folders)

R_S = Q − T_S with T_S = T_∞ + ΔT (two_adic/ RESULTS s5 item 2, s5b, s7b, s10). ΔT is the whole 2-adic part of T_S, ΔT(g) = Tr(ϑ(g)(Q_∞ − Q_S)ϑ(g)^*), computed by two_adic/ in float64 from a finite family of prolate modes (ta_prolate.py, ta_mellin.py, ρ by QR since c3dca00). At c = 2.9 the stored R_S has 4, 10, 20 eigenvalues below −band at N = 8, 16, 32 (checker/ s7.9, exact rational inertia of the stored float64 matrices, checker/checker_inertia.json). The band (8.2e−3 at c = 2.9, N = 32) is a response, not a bound, and 14 of the 20 at N = 32 lie between −2·band and −band.

Goal of this follow-up: a proven bound ε ≥ ‖ΔT_exact − ΔT_stored‖, spectral norm on the (2N+1)-dimensional space spanned by U_n, n = −N … N (MISSION.md interface contract), for each stored build, carried by arb enclosures; then the count of eigenvalues of the stored R_S strictly below −ε, by exact inertia. By Weyl, each such eigenvalue gives a negative eigenvalue of the Galerkin compression of the exact R_S, provided the errors of Q and T_∞ are inside ε too.

Stored builds (nvec | S | N; Kmax = two_adic.ta_prolate.kmax_for(nvec)): N = 8: 80|1200. N = 16: 80|1200, 80|1600, 120|1200, 120|1600, 160|1600. N = 32: 200|2400, 240|2400, 280|2266, 319|2633, 364|3060. The matrices are in checker/checker_ts_snapshot.json (key T_S, units) and modal/out_rho/checker_*.json; checker/run_checker_inertia.py shows how R is formed from them. Measured responses to compare against: two_adic/ s7b (nvec 80 → 200 at S = 4800, c = 2.2, N = 8) and checker/ s7.2, s7.3a, s7.8 (80 → 120 → 160 at N = 16, 200 → 364 at N = 32).

Error sources of ΔT_stored and their owners:

sourceowner
prolate modes beyond nvec omitted from Q_∞ and Q_Sbound_trunc/
s cutoff S of the Mellin and Gram integrals, including the order-1/S tailsbound_quad/
w quadrature: Gauss panels on [1, 2^Kmax], the dyadic truncation at Kmax, the asymptotic 1/w tail series (its term count)bound_quad/
mode data: η_n and ζ_n evaluated in float64 (scipy spherical Bessel)bound_quad/
the Gram step, QR of the Gram factor in ta_mellin.rhobound_quad/
float64 rounding in the assembly of the stored matrixbound_quad/
Q (checker/, mpmath dps 40, rounded to float64) and T_∞ (kernel/, dps 40)assembler/ states their size and grade; nobody re-derives them

The bound interface (fixed now, so the referee can test against it before it exists). Each bound folder exposes a Python function and a JSON file:

eps_upper is a decimal string that is an upper bound on the error (the upper end of the arb ball, rounded up), for every stored build at every c in {2.2, 2.5, 2.9}. assumptions lists the numbered assumptions of the folder's derivation that the number depends on. If a bound does not exist for a build, the entry says "eps_upper": null and why.

Outcomes (all acceptable; the numbers decide which)

  1. Growth below −ε: the count at c = 2.9 still grows over N = 8, 16, 32. Wording, per the operator's ruling (2026-09-24): C4 fixes no rank bound, so no finite N refutes bounded rank. Say: n_−(R_S) ≥ k_N at N = 8, 16, 32 on this construction (lower bounds), which rules out any remainder of rank below k_32 here and is evidence against bounded rank; not a refutation.
  2. Growth absent below −ε, with ε small enough to resolve it: C4 survives this test; say so plainly.
  3. The bound closes but ε swamps the spectrum: counts collapse because ε is large, not because the negatives are gone. This is "not resolved at ε", and it is not outcome 2.
  4. No usable bound: say precisely which step would not close. That is itself a result.

Grade ceiling. The tail and quadrature bounds are ordinary arguments. With arb carrying every numerical step and referee/ having reviewed the derivation, the best grade is "enclosure-carrying numerics on a derivation reviewed internally (unreviewed externally)". Only a statement AXLE checks in Lean with zero sorry is kernel-checked, and only for exactly that statement. A composite takes its weakest step.

Rules (all four folders)