"""v669 -- PRIME.FEJERDENS.01: THE FEJER DENSITY BOUND -- the renamed W2 residual task of the Garding envelope round (v663): a lower bound for the Fejer-smoothed spectral density of the TOTAL window symbol (gap control of the spectral mass in short windows), the honest identification of s_tot as a smoothed ZERO-COUNTING density, and the unconditional RvM chain with a machine-checked finite remainder. This module measures and derives; it moves no marker. THE RAW OBJECT (verbatim garding_envelope_probe). For a frame-A window [-a, a] the continuum total symbol per unit L^2 plane-wave mass s_tot(t; a) = s_sm(t; a) - sigma_at(t; a) + s_po(t; a), s_sm = int Omega(tau) F_a(tau - t) dtau, Omega(tau) = Re psi(1/4 + i tau/2) - log pi, F_a(s) = sin^2(a s)/(pi a s^2) (unit-mass Fejer), sigma_at = sum_{n <= e^{2a}} mu_n (1 - u_n/(2a)) cos(t u_n), u_n = log n, mu_n = 2 Lambda(n)/sqrt(n) (tent weight), s_po = 2 Re(A(t) conj(B(t)))/(2a), A/B = int_{-a}^{a} e^{itx} e^{+-x/2} dx (rank-2 cosh pole layer, closed form). F1 -- THE SMOOTHED OBJECT. rho_{a,delta}(t) = (s_tot(.; a) * Phi_delta)(t) with the unit-mass Fejer kernel Phi_delta(s) = delta sin^2(pi s/delta) / (pi^2 s^2), DECLARED NORMALIZATION: unit mass; "width" = main-lobe half-width = first spatial zero = delta; the Fourier transform of Phi_delta is the TENT (1 - |xi| delta/(2 pi))_+ on |xi| <= 2 pi/delta -- the same tent structure as the frame-A window autocorrelation that defines s_tot. Width ladder per window (declared): delta1 = 1/a (the literal premise of the task name), delta2 = pi/a (the plane-wave resolution = F_a main-lobe half-width), delta3 = 4 pi (fixed, a-independent RvM width), delta4 = pi a (the "F_{1/a}" Fourier reading: lag-tent of width 2/a). F2/F4 -- THE EXACT IDENTITY (derivation sketch). Apply Weil's explicit formula (Iwaniec-Kowalski Thm 5.12 normalization) to the test pair g_t(u) = (1/2a) (2a - |u|)_+ e^{-i t u}, h_t(r) = int g_t(u) e^{i r u} du = (2/a) sin^2(a (r - t))/(r - t)^2 = 2 pi F_a(r - t), g_t is continuous, compactly supported and of bounded variation (the Barner/Weil admissibility class); h_t is entire of exponential type 2a (Paley-Wiener) with 1/r^2 decay, so every term converges. Then, term by term: archimedean: (1/2pi) int h_t(r) Omega(r) dr = s_sm(t; a), primes: sum_n Lambda(n) n^{-1/2} (g_t(log n) + g_t(-log n)) = sum mu_n (1 - u_n/2a) cos(t u_n) = sigma_at(t; a), poles: h_t(i/2) + h_t(-i/2) = (1/2a) 2 Re(A conj(B)) = s_po(t; a) (indicator autocorrelation), zeros: sum_rho h_t(gamma_rho) = 2 pi sum_rho F_a(gamma_rho-t), and the explicit formula (zeros = arch + poles - primes) gives the EXACT identity s_tot(t; a) = 2 pi sum_rho F_a(gamma_rho - t), the sum over ALL nontrivial zeros rho = beta + i gamma with gamma of both signs (gamma_rho = (rho - 1/2)/i, complex iff off-line; F_a is evaluated by entire continuation there). DISTRIBUTIONAL READING: s_tot(.; a) = 2 pi (F_a * dN) with dN = sum delta_{gamma} once all zeros at the relevant heights lie on the line -- verified to height 3.0e12 (Platt-Trudgian 2021); hypothetical off-line zeros above that height contribute at most 2 cosh^2(a/2)/(pi a d^2) each (|Im| < 1/2), a rigorously negligible budget printed below (~1e-10). So s_tot IS (2 pi times) the Fejer-smoothed zero-counting density, its peaks sit at the zeros 14.13, 21.02, 25.01, ... (the envelope probe measured them there without reading any zero), and its dips are the zero gaps: dip depth ~ 2 pi F_a(gap half-width) ~ 1/(pi a d^2) -- the measured a^{-0.98} Fejer mechanism. F3 -- THE UNCONDITIONAL CHAIN (all constants cited, no RH input). (i) N(t) = t/2pi log(t/2pi e) + 7/8 + S(t) + E(t), |E(t)| <= 1/(48 pi t) + O(t^-3); |S(t)| <= A1 log t + A2 loglog t + A3 with (A1, A2, A3) = (0.112, 0.278, 2.510) for t >= e [Trudgian 2014, J. Number Theory 134, Thm 1; classical alternative Backlund 1918: (0.137, 0.443, 4.350); newer Hasanalizade-Shen-Wong 2022: (0.1038, 0.2573, 9.3675)]. (ii) window count, exact main term: N(u+d/2) - N(u-d/2) >= Mlo(u, d) := [main(u+d/2) - main(u-d/2)] - 2 Sbar(u+d/2) - EPS_N, main(x) = x/2pi log(x/2pi e), EPS_N = 2e-3 (the E budget), Sbar monotone. Mlo >= (d/2pi) log((u-d/2)/2pi) - 2 Sbar - EPS_N (log minorant, for the slope statement). (iii) box minorant of the Fejer kernel: Phi_delta decreases on the main half-lobe, so Phi_delta(s) >= (4/pi^2)(1/delta) for |s| <= delta/2, hence 2 pi (dN * Phi_delta)(u) >= (8/(pi delta)) max(Mlo(u,delta),0) =: L(u). (iv) mass transfer through F_a >= 0 (rho = 2pi dN*F_a*Phi = the F_a-average of the nonnegative 2pi dN*Phi): rho_{a,delta}(t) >= (1 - 4/(pi a t)) inf_{|s| <= t/2} L(t - s) = (1 - 4/(pi a t)) L(t/2) once L is nondecreasing on [t/2, 3t/2] (checked numerically on the used range; tail mass int_{|s|>t/2} F_a <= 4/(pi a t)). => THEOREM-GRADE bound rho_{a,delta}(t) >= B_{a,delta}(t) := (1 - 4/(pi a t)) (8/(pi delta)) max(Mlo(t/2, delta), 0) for all t >= t0(a, delta) := 2 u0(delta) (u0 = bisection root of Mlo). Asymptotic slope in log t: (4/pi^2)(1 - 4 pi A1/delta) -- POSITIVE iff delta > 4 pi A1 = 1.40743...: the RvM CERTIFIABILITY FLOOR. The literal width delta1 = 1/a <= 0.36 and the plane-wave width delta2 = pi/a <= 1.134 sit BELOW the floor for every family window (pi/a > 4 pi A1 would need a < 1/(4 A1) = 2.2321; the family starts at a0 = log 16 = 2.7726) -- the honest structural explanation of the Garding 1/log drift: per-mode (plane-wave) control is not certifiable from RvM + Trudgian at ANY height for these windows. delta3 = 4 pi and delta4 = pi a sit above the floor and close. (v) declared pair: c0_thm = 0.9 x (4/pi^2)(1 - 4 pi A1/delta) (the 10% shave absorbs the unbounded loglog drag into a finite C0), C0_thm = sup_{t >= t0} [c0_thm log(2+t) - B(t)] (numeric sup on a log grid to 1e12, decreasing-tail check printed). FINITE REMAINDER: rho_{a,delta}(t) >= c0_thm log(2+t) - C0_thm machine-checked on the grid [10, t0] -- and rho is assembled from primes + digamma ONLY, no zero enters, so the certificate is independent of the zero data ([E]-candidate). CALIBRATION (declared -- honesty first): run 1 (2026-08-02) failed ONLY the G0.2 dip-power comparator: the probe read the dip scaling at a FIXED t_hat (the largest window's minimum location), where the anchor window has no dip at all (its wider Fejer lobe catches gamma_2 there), giving a meaningless p = 5.34. The predecessor convention (garding_envelope_probe E2.2, the source of the 0.98 quote) fits the MATCHED per-window minima s*(a) = min_{[20,100]} s_tot(.; a). The comparator (not the bar, not any other number) was upgraded to the matched-minimum read; F2.4 evaluates the zero side at each window's own dip location. All other run-1 numbers reproduce unchanged. SLICES AND BARS (declared BEFORE the numbers): G0.0 [E] zero-comb integrity: cache monotone; n = 1, 2, 3, 2000 vs live mpmath zetazero (dps 20) <= 1e-8; RvM consistency max_n |main(gamma_n) + 7/8 - n| <= Sbar(gamma_n) + 0.01. (Completeness of the comb was Turing-certified by turing_cert_probe on the same cache -- cited, not rerun.) G0.1 [E] machinery: scipy digamma == mpmath at 4 points (< 1e-10); Fejer conv-kernel truncation masses < 1e-3 (renormalized, declared); Phi_delta truncation masses < 5e-3 (renormalized, declared); high-precision quadrature s_tot == grid s_tot at 6 points, dev <= 3e-3 (the declared conv-truncation bias scale). G0.2 [E] raw-envelope reproduction (task quotes): anchor continuum min_{[20,100]} s_tot within 0.03 of 0.057; raw hull constant within 0.015 of 0.021 (fit or implied route, closer one, declared); fixed-t dip power |p - 0.98| <= 0.2. F1.1 [MEASURED, central] rho tables: band minima (7 dyadic bands on [20, 2560]) per (a, delta), per-window and hull fits b + c0 log(2+t), the measured pairs (c0, C0) on [10, 2560] and [20, 2560], and the gain c0(delta)/c0(raw). F2.1 [E] the first four peaks of s_tot (largest window) match the task quotes (14.14, 21.02, 25.02, 30.42) AND the true zeros gamma_1..4 within 0.05. F2.2 [MEASURED] peak <-> zero matching on [10, 300] (largest window): matched fraction >= 0.85 at tol 0.25, median |residual| <= 0.08. F2.3 [MEASURED] gap structure: max zero gap on [10, 2515] vs the delta ladder; empty-window fractions per (a, delta) on [20, 2500]; bar: fraction(delta1) > 0.05 AND fraction(delta4) = 0 (the literal premise fails, the repaired widths fill); the RvM floor statement 4 pi A1 = 1.4074 printed. F2.4 [MEASURED] dip forensics at the matched per-window dips t*_w (E2.2 convention): zero-side prediction vs high-precision s_tot for all 5 windows, |residual| <= 1e-4; power fits p_meas vs p_pred, |p_meas - p_pred| <= 0.1. F3.0 [E] count-validity guard: min_u [count(u) - Mlo(u, delta)] >= 0 over the cache range for delta3 and delta4 (a targets largest window) -- the cited bound must hold on real zeros. F3.1 [ANALYTIC, cited] the constants table: slope factor sign per delta, t0(a, delta), (c0_thm, C0_thm) per (a, delta3/4); feasibility t0 <= 6000. F3.2 [E-candidate] finite certificates: min_t [rho - (c0_thm log(2+t) - C0_thm)] >= 0.05 on the grid [10, t0], all 10 (a, delta3/4) combinations (margin bar = 3x the declared systematics budget). F4.1 [E] identity numerics: V1 pointwise |s_tot - zero side| <= 1e-5 at ~17 declared points per window (a0 and largest; t <= 320, cache-tail-limited; the oscillation-blind tail budget ~2e-3 is printed, the bar ASSUMES the measured oscillatory cancellation -- declared); V2 t-averaged (Hann window on [50, 250], 201 points) |mean residual| <= 1e-6 -- the 1e-6 verification target of the task. High-t points (> 320) printed without bar. F4.2 [C] typing + contract note (report only). Verdict enums (frozen, precedence top-down): FEJER-MIXED (any G0.* or F3.0 fails), FEJER-DENSITY-THEOREM (F4.1 + F2.1 pass AND all 10 certificates pass AND min c0_thm >= 10 x raw hull c0), FEJER-DENSITY-PARTIAL (F4.1 passes AND >= 1 certificate passes), FEJER-IDENTITY-ONLY (F4.1 passes), FEJER-NO-GAIN (otherwise). FIREWALL (INVERTED, declared). Unlike v661/v663 this module DELIBERATELY reads Riemann zeros -- the identification question IS the task. Structural separation replaces the AST ban: s_tot and rho are assembled from primes + digamma ONLY (machinery verbatim v663_garding_envelope.py; no zero enters the symbol assembly or the F3.2 certificates); zeros enter ONLY the identification (F2/F4), the gap statistics (F2.3) and the count-validity guard (F3.0). Zero data: the shared Turing-certified cache (committed in experiments/tfpt-discovery/zero_comb_cache_n2000.json; completeness certified by v666_turing_cert.py, diagnostic zero-side line per the v589 convention). v563 import read-only; no marker moves; Python-only per GATE.WOLFRAM.02. PROVENANCE: discovery probe fejer_density_bound_probe.py (2026-08-02, 14/14, verdict FEJER-DENSITY-THEOREM); garding_envelope_probe.py + garding_probe.py (2026-08-02, the drift diagnosis, the envelope measurement, the renamed residual task), zero_comb_cache_n2000.json (v666: TURING-COMPLETE-BAND), v563_paper2_readouts (atom table, frame-A windows), Trudgian J. Number Theory 134 (2014) 280-292, Platt-Trudgian Bull. LMS 53 (2021) 792-797, Backlund 1918, Hasanalizade-Shen-Wong J. Number Theory 233 (2022), Iwaniec-Kowalski, Analytic Number Theory, Thm 5.12. """ import json import math import os import sys import time import numpy as np _here = os.path.dirname(os.path.abspath(__file__)) for _cand in (_here, os.path.join(_here, "..", "..", "verification")): if os.path.exists(os.path.join(_cand, "v563_paper2_readouts.py")): sys.path.insert(0, os.path.abspath(_cand)) break T0 = time.time() FAILS = [] N_CHK = 0 def check(name, ok, detail=""): global N_CHK N_CHK += 1 if not ok: FAILS.append(name.split()[0]) print("[%s] %s%s" % ("PASS" if ok else "FAIL", name, (": " + detail) if detail else "")) import v563_paper2_readouts as core # noqa: E402 (READ-ONLY import) import mpmath as mp # noqa: E402 from scipy.signal import fftconvolve # noqa: E402 from scipy.special import digamma as sp_digamma # noqa: E402 # ------------------------------------------------------------ constants T_REP = 2560.0 # report range top (predecessor T_HI) T_MIN = 10.0 # report range floor (declared) DT = 0.01 # master uniform grid S_PHI = 1200.0 # Phi kernel truncation half-width SIG_CONV = 700.0 # Fejer conv kernel half-width (verb.) DT_CONV = 0.01 BANDS = ((20.0, 40.0), (40.0, 80.0), (80.0, 160.0), (160.0, 320.0), (320.0, 640.0), (640.0, 1280.0), (1280.0, 2560.0)) A1_TR, A2_TR, A3_TR = 0.112, 0.278, 2.510 # Trudgian 2014 (t >= e) EPS_N = 2e-3 # theta-remainder budget (2x 1/(48 pi t)) RVM_FLOOR = 4.0 * math.pi * A1_TR # = 1.40743 certif. floor C0_SHAVE = 0.9 # declared shave (absorbs loglog drag) RH_HEIGHT = 3.0e12 # Platt-Trudgian verified height T0_FEAS = 6000.0 # certificate feasibility cap MARGIN_BAR = 0.05 # certificate margin bar (3x budget) BAR_DIGAMMA = 1e-10 BAR_MASS_CONV = 1e-3 BAR_MASS_PHI = 5e-3 BAR_HIPREC = 3e-3 # hi-prec vs grid s_tot BAR_ZERO_CACHE = 1e-8 BAR_REPRO_MIN, REF_MIN = 0.03, 0.057 BAR_REPRO_C0, REF_C0_RAW = 0.015, 0.021 REF_C_RAW = 0.055 BAR_REPRO_P, REF_P = 0.2, 0.98 BAR_PEAK = 0.05 PEAK_QUOTES = (14.14, 21.02, 25.02, 30.42) BAR_MATCH_FRAC, MATCH_TOL, BAR_MATCH_MED = 0.85, 0.25, 0.08 BAR_DIP_RES = 1e-4 BAR_DIP_P = 0.1 BAR_V1 = 1e-5 BAR_V2 = 1e-6 V1_T_MAX = 320.0 GAIN_THM_MIN = 10.0 DT_Q = 0.002 # identity quadrature grid T_Q = 3400.0 # identity quadrature range TAIL_END = 1.0e10 # smooth-tail log-grid end N_LERCH = 20000 _NN_L = np.arange(N_LERCH, dtype=float) _WTS = 1.0 / (_NN_L + 0.25) ** 2 mp.mp.dps = 30 LOGPI_F = math.log(math.pi) TWO_PI = 2.0 * math.pi UU = np.array([float(u) for u in core.U_ALL]) MU = np.array([float(m) for m in core.MU_ALL]) HERE = os.path.dirname(os.path.abspath(__file__)) # shared zero-comb cache: committed in experiments/tfpt-discovery/ # (repo tree); fall back to a local copy next to this module (website # mirror / standalone use). _REPO_CACHE = os.path.join(os.path.dirname(HERE), "experiments", "tfpt-discovery", "zero_comb_cache_n2000.json") _LOCAL_CACHE = os.path.join(HERE, "zero_comb_cache_n2000.json") CACHE = _REPO_CACHE if os.path.exists(_REPO_CACHE) else _LOCAL_CACHE # ------------------------------------------------- symbol machinery # (verbatim garding_envelope_probe continuum route: primes + digamma # ONLY -- no zero enters here; the structural firewall of the probe) def omega_arch(tau): z = 0.25 + 0.5j * np.asarray(tau, dtype=float) return np.real(sp_digamma(z)) - LOGPI_F def fejer_a(a, s): s = np.asarray(s, dtype=float) out = np.empty_like(s) small = np.abs(s) < 1e-9 ss = np.where(small, 1.0, s) out = np.sin(a * ss) ** 2 / (math.pi * a * ss ** 2) out[small] = a / math.pi return out def smooth_conv(a, t_hi): """s_sm on the uniform DT grid [0, t_hi] via FFT convolution of Omega with the truncated renormalized Fejer kernel (verbatim predecessor convention).""" tau = np.arange(-SIG_CONV, t_hi + SIG_CONV + 0.5 * DT_CONV, DT_CONV) om = omega_arch(tau) sig = np.arange(-SIG_CONV, SIG_CONV + 0.5 * DT_CONV, DT_CONV) F = fejer_a(a, sig) mass = float(np.sum(F) * DT_CONV) Fn = F / mass s = fftconvolve(om, Fn[::-1], mode="valid") * DT_CONV tg = np.arange(0.0, t_hi + 0.5 * DT_CONV, DT_CONV) return tg, s[:tg.size], abs(mass - 1.0) def sigma_at_tent(a, ts, ka): u = UU[:ka] w = MU[:ka] * (1.0 - u / (2.0 * a)) out = np.empty(ts.size) for lo in range(0, ts.size, 256): hi = min(ts.size, lo + 256) out[lo:hi] = np.cos(np.outer(ts[lo:hi], u)) @ w return out def s_po_cont(a, ts): t = np.asarray(ts, dtype=float) sA = 0.5 + 1j * t sB = -0.5 + 1j * t A = (np.exp(sA * a) - np.exp(-sA * a)) / sA B = (np.exp(sB * a) - np.exp(-sB * a)) / sB return 2.0 * np.real(A * np.conj(B)) / (2.0 * a) def phi_kernel(delta): """truncated renormalized Phi_delta on the DT grid; returns (kernel, half-width points, mass deviation).""" xs = np.arange(-S_PHI, S_PHI + 0.5 * DT, DT) b = math.pi / delta ker = np.empty_like(xs) small = np.abs(xs) < 1e-9 ss = np.where(small, 1.0, xs) ker = np.sin(b * ss) ** 2 / (math.pi * b * ss ** 2) ker[small] = b / math.pi mass = float(np.sum(ker) * DT) return ker / mass, (ker.size - 1) // 2, abs(mass - 1.0) def smooth_rho(s_tot, ker, npad): """rho = s_tot * Phi on the grid, even extension at t = 0; valid up to len(s_tot) - npad.""" ext = np.concatenate([s_tot[npad:0:-1], s_tot]) r = fftconvolve(ext, ker, mode="same") * DT return r[npad:] # ------------------------------------------------- fits and extrema def fit_flat(y): y = np.asarray(y, float) m = float(np.mean(y)) return m, float(np.sqrt(np.mean((y - m) ** 2))) def fit_affine(x, y): x = np.asarray(x, float) y = np.asarray(y, float) A = np.column_stack([np.ones(x.size), x]) bf, _, _, _ = np.linalg.lstsq(A, y, rcond=None) rms = float(np.sqrt(np.mean((y - A @ bf) ** 2))) return float(bf[0]), float(bf[1]), rms def refine_extremum(ts, ys, i, sign=+1): """3-point parabolic refinement at grid index i (sign=+1 minimum, -1 maximum); returns (t*, y*).""" if i <= 0 or i >= ts.size - 1: return float(ts[i]), float(ys[i]) y0, y1, y2 = float(ys[i - 1]), float(ys[i]), float(ys[i + 1]) den = y0 - 2.0 * y1 + y2 if sign * den <= 0: return float(ts[i]), y1 off = 0.5 * (y0 - y2) / den off = max(-1.0, min(1.0, off)) tstar = float(ts[i]) + off * (float(ts[1]) - float(ts[0])) ystar = y1 - 0.25 * (y0 - y2) * off return tstar, ystar def band_minima(ts, ys, bands): out = [] for (b0, b1) in bands: m = (ts >= b0) & (ts < b1) idx = np.where(m)[0] i = idx[int(np.argmin(ys[idx]))] out.append(refine_extremum(ts, ys, i, sign=+1)) return out def local_maxima_idx(ys): return np.where((ys[1:-1] > ys[:-2]) & (ys[1:-1] >= ys[2:]))[0] + 1 # ------------------------------------------------- RvM chain pieces def main_N(x): return x / TWO_PI * (np.log(x / TWO_PI) - 1.0) def s_bar(x): x = np.asarray(x, dtype=float) return A1_TR * np.log(x) + A2_TR * np.log(np.log(x)) + A3_TR def m_lo(u, d): """unconditional window-count lower bound N(u+d/2)-N(u-d/2) >= ...""" u = np.asarray(u, dtype=float) return (main_N(u + d / 2.0) - main_N(u - d / 2.0) - 2.0 * s_bar(u + d / 2.0) - EPS_N) def u0_of(delta): """bisection root of m_lo(u, delta) = 0 (None if slope factor negative -> no root below 1e7 or bound decreasing).""" lo = max(12.0, delta / 2.0 + 10.0) hi = 1.0e7 if m_lo(hi, delta) <= 0.0: return None if m_lo(lo, delta) > 0.0: return float(lo) for _ in range(200): mid = math.sqrt(lo * hi) if m_lo(mid, delta) > 0.0: hi = mid else: lo = mid return float(hi) def bound_B(t, a, delta): t = np.asarray(t, dtype=float) L = (8.0 / (math.pi * delta)) * np.maximum(m_lo(t / 2.0, delta), 0.0) return np.maximum(1.0 - 4.0 / (math.pi * a * t), 0.0) * L def run(): global N_CHK, FAILS N_CHK = 0 FAILS = [] print("=" * 78) print("THE FEJER DENSITY BOUND -- rho_{a,delta} = s_tot * Phi_delta" ", the zero-density identity, and the unconditional RvM chain") print("=" * 78) # ------------------------------------------------ G0.0 zero comb with open(CACHE, "r", encoding="utf-8") as fh: cache = json.load(fh) GAM = np.array([float(g) for g in cache["gammas"]]) n_z = GAM.size mono = bool(np.all(np.diff(GAM) > 0.0)) mp.mp.dps = 20 live = {n: float(mp.im(mp.zetazero(n))) for n in (1, 2, 3, n_z)} mp.mp.dps = 30 dev_z = max(abs(GAM[n - 1] - live[n]) for n in live) rn = np.abs(main_N(GAM) + 7.0 / 8.0 - np.arange(1, n_z + 1)) rvm_ok = bool(np.all(rn <= s_bar(GAM) + 0.01)) check("G0.0 [E] zero-comb integrity: %d zeros (dps %s, Turing-" "certified cache), monotone %s, live-mpmath dev at n=1,2,3," "%d: %.2e <= %.0e, RvM residual max %.3f <= Sbar+0.01" % (n_z, cache.get("dps"), mono, n_z, dev_z, BAR_ZERO_CACHE, float(np.max(rn))), mono and dev_z <= BAR_ZERO_CACHE and rvm_ok) gam_max = float(GAM[-1]) # ------------------------------------------------ window family kz0 = core.frame_a_zones()[0] r0 = core.build_window(kz0) a0 = r0["alpha"] zones = core.frame_a_zones() fam = [] for kz in zones: alpha = float(core.U_ALL[kz]) D_k = 0.5 * float(core.G_ALL[kz]) / float(core.NU_MAIN) Mz = int(math.ceil(alpha / D_k - 1.0e-9)) + 1 if Mz % 2: Mz += 1 hz = Mz // 2 complete = math.exp(2.0 * alpha) <= core.ATOM_MAX + 0.5 fam.append((kz, alpha, hz, complete)) comp = [t for t in fam if t[3]] hs_c = np.array([t[2] for t in comp], float) picks = [comp[0]] for qq in (0.25, 0.5, 0.75, 1.0): tgt = float(np.quantile(hs_c, qq)) cand = min(comp, key=lambda t: abs(t[2] - tgt)) if all(cand[0] != p[0] for p in picks): picks.append(cand) picks = sorted(picks, key=lambda t: t[2]) print("family (garding_probe B2 selection): h = %s, a = %s" % ([t[2] for t in picks], ["%.4f" % t[1] for t in picks])) A_FAM = [t[1] for t in picks] H_FAM = [t[2] for t in picks] # delta ladders and t0 needs (before any grid is built) def ladder(a): return (("1/a", 1.0 / a), ("pi/a", math.pi / a), ("4pi", 4.0 * math.pi), ("pi*a", math.pi * a)) t0_tab = {} for a in A_FAM: for lab, d in ladder(a): if lab in ("4pi", "pi*a"): u0 = u0_of(d) t0_tab[(a, lab)] = None if u0 is None else 2.0 * u0 tg_need = {} for a in A_FAM: need = T_REP for lab in ("4pi", "pi*a"): t0v = t0_tab[(a, lab)] if t0v is not None and t0v <= T0_FEAS: need = max(need, t0v) tg_need[a] = need + S_PHI + 80.0 # ------------------------------------------------ per-window build print("\nbuilding the 5-window continuum symbol family " "(primes + digamma only) ...") WIN = [] for (kz, alpha, hz, _c) in picks: t1 = time.time() tg_hi = tg_need[alpha] ts = np.arange(0.0, tg_hi + 0.5 * DT, DT) tgc, s_sm_c, mdev = smooth_conv(alpha, tg_hi) s_sm = np.interp(ts, tgc, s_sm_c) ka = core.atoms_in(alpha) s_at = sigma_at_tent(alpha, ts, ka) s_po = s_po_cont(alpha, ts) st = s_sm - s_at + s_po WIN.append(dict(a=alpha, hz=hz, ka=ka, ts=ts, s_tot=st, mdev=mdev, tg_hi=tg_hi)) print(" h = %4d (a = %.4f, %5d atoms, grid to %6.0f)" " [%.1f s]" % (hz, alpha, ka, tg_hi, time.time() - t1)) wA = WIN[0] wP = WIN[-1] # ------------------------------------------------ identity machinery tau_q = np.arange(0.0, T_Q + 0.5 * DT_Q, DT_Q) om_q = omega_arch(tau_q) lg = np.exp(np.linspace(math.log(T_Q), math.log(TAIL_END), 6000)) om_lg = omega_arch(lg) zg = np.exp(np.linspace(math.log(gam_max), math.log(TAIL_END), 6000)) dens_zg = np.log(zg / TWO_PI) / TWO_PI - 1.0 / (48.0 * math.pi * zg ** 2) def s_sm_hi(a, t): """high-precision s_sm(t; a): fine trapezoid on [0, T_Q] plus the smooth sin^2 -> 1/2 tail on a log grid (cos-part bounded, printed).""" f = fejer_a(a, tau_q - t) + fejer_a(a, tau_q + t) val = float(np.trapezoid(om_q * f, dx=DT_Q)) tail_int = om_lg / (2.0 * math.pi * a) \ * (1.0 / (lg - t) ** 2 + 1.0 / (lg + t) ** 2) val += float(np.trapezoid(tail_int * lg, np.log(lg))) return val def s_tot_hi(a, t, ka): u = UU[:ka] w = MU[:ka] * (1.0 - u / (2.0 * a)) sat = float(np.cos(t * u) @ w) spo = float(s_po_cont(a, np.array([t]))[0]) return s_sm_hi(a, t) - sat + spo def zero_side(a, t): """2 pi sum over the comb + smooth RvM density tail (sin^2 -> 1/2 on a log grid; boundary-count offset and cos-part are budgeted, printed).""" zsum = TWO_PI * float(np.sum(fejer_a(a, GAM - t) + fejer_a(a, GAM + t))) tail = dens_zg / a * (1.0 / (zg - t) ** 2 + 1.0 / (zg + t) ** 2) return zsum + float(np.trapezoid(tail * zg, np.log(zg))) # G0.1 machinery guards dg_dev = 0.0 for tq in (0.5, 5.0, 50.0, 400.0): ex = float(mp.re(mp.digamma(mp.mpf(1) / 4 + 0.5j * tq))) dg_dev = max(dg_dev, abs(float(omega_arch(np.array([tq]))[0]) - (ex - LOGPI_F))) phi_cache = {} phi_devs = [] for w in WIN: for lab, d in ladder(w["a"]): if d not in phi_cache: phi_cache[d] = phi_kernel(d) phi_devs.append(phi_cache[d][2]) hi_devs = [] for w in (wA, wP): for tq in (15.0, 25.0, 40.0, 80.0, 160.0, 300.0): i = int(round(tq / DT)) hi_devs.append(abs(s_tot_hi(w["a"], float(w["ts"][i]), w["ka"]) - float(w["s_tot"][i]))) check("G0.1 [E] machinery: digamma dev %.1e < %.0e; conv Fejer " "masses %s < %.0e; Phi masses %s < %.0e (renormalized, " "declared); hi-prec quadrature vs grid s_tot at 12 points: " "max dev %.2e <= %.0e" % (dg_dev, BAR_DIGAMMA, ["%.1e" % w["mdev"] for w in WIN], BAR_MASS_CONV, ["%.1e" % d for d in phi_devs], BAR_MASS_PHI, max(hi_devs), BAR_HIPREC), dg_dev < BAR_DIGAMMA and max(w["mdev"] for w in WIN) < BAR_MASS_CONV and max(phi_devs) < BAR_MASS_PHI and max(hi_devs) <= BAR_HIPREC) # ------------------------------------------------ raw envelope print("\nraw envelope (reproduction of the predecessor + baseline)") raw_bands = {} for w in WIN: raw_bands[w["a"]] = band_minima(w["ts"], w["s_tot"], BANDS) hull_b = [] for bi in range(len(BANDS)): cand = [raw_bands[w["a"]][bi] for w in WIN] hull_b.append(min(cand, key=lambda x: x[1])) tbh = np.array([x[0] for x in hull_b]) sbh = np.array([x[1] for x in hull_b]) b_r, c_raw_fit, r_r = fit_affine(np.log(2.0 + tbh), sbh) delta_h = sbh[-1] - sbh[0] lever = math.log(2.0 + tbh[-1]) - math.log(2.0 + tbh[0]) c_raw_impl = delta_h / lever c_raw = min((c_raw_fit, c_raw_impl), key=lambda c: abs(c - REF_C0_RAW)) mlo_ = (wA["ts"] >= 20.0) & (wA["ts"] <= 100.0) idxm = np.where(mlo_)[0] i0 = idxm[int(np.argmin(wA["s_tot"][idxm]))] t_min_a0, s_min_a0 = refine_extremum(wA["ts"], wA["s_tot"], i0) t_star = [] s_star_meas = [] for w in WIN: mw = (w["ts"] >= 20.0) & (w["ts"] <= 100.0) idxw = np.where(mw)[0] iw = idxw[int(np.argmin(w["s_tot"][idxw]))] tw, _sw = refine_extremum(w["ts"], w["s_tot"], iw) t_star.append(tw) s_star_meas.append(s_tot_hi(w["a"], tw, w["ka"])) t_star = np.array(t_star) s_star_meas = np.array(s_star_meas) a_arr = np.array(A_FAM) _b, slp, _r = fit_affine(np.log(a_arr), np.log(np.abs(s_star_meas))) p_meas = -slp print(" hull band minima: %s" % " | ".join("%.4f @ %.1f" % (s, t) for t, s in hull_b)) print(" raw hull fit: %+.4f %+.5f log(2+t) (rms %.4f); implied " "c0 = %+.5f; anchor min[20,100] = %.5f at t = %.3f; " "matched dips t* = %s, s* = %s, p_meas = %.3f" % (b_r, c_raw_fit, r_r, c_raw_impl, s_min_a0, t_min_a0, ["%.2f" % v for v in t_star], ["%.5f" % v for v in s_star_meas], p_meas)) C_raw_20 = 0.0 for w in WIN: m = (w["ts"] >= 20.0) & (w["ts"] <= T_REP) C_raw_20 = max(C_raw_20, float(np.max( REF_C0_RAW * np.log(2.0 + w["ts"][m]) - w["s_tot"][m]))) print(" raw C0 at c0 = %.3f on [20, 2560]: %.4f (quote %.3f)" % (REF_C0_RAW, C_raw_20, REF_C_RAW)) check("G0.2 [E] raw-envelope reproduction: anchor min[20,100] = " "%.5f (|dev - %.3f| = %.4f <= %.2f); raw hull c0 = %+.5f " "(closer route; |dev - %.3f| = %.4f <= %.3f); dip power " "p_meas = %.3f (|dev - %.2f| = %.3f <= %.1f)" % (s_min_a0, REF_MIN, abs(s_min_a0 - REF_MIN), BAR_REPRO_MIN, c_raw, REF_C0_RAW, abs(c_raw - REF_C0_RAW), BAR_REPRO_C0, p_meas, REF_P, abs(p_meas - REF_P), BAR_REPRO_P), abs(s_min_a0 - REF_MIN) <= BAR_REPRO_MIN and abs(c_raw - REF_C0_RAW) <= BAR_REPRO_C0 and abs(p_meas - REF_P) <= BAR_REPRO_P) # ------------------------------------------------ F1 rho tables print("\nF1 -- rho_{a,delta} = s_tot * Phi_delta on [10, 2560]") RHO = {} for w in WIN: for lab, d in ladder(w["a"]): ker, npad, _dv = phi_cache[d] RHO[(w["a"], lab)] = smooth_rho(w["s_tot"], ker, npad) fit_tab = {} for lab_i, lab in enumerate(("1/a", "pi/a", "4pi", "pi*a")): hull_rb = [] for bi in range(len(BANDS)): cand = [] for w in WIN: r = RHO[(w["a"], lab)] bm = band_minima(w["ts"][:r.size], r, (BANDS[bi],))[0] cand.append(bm) hull_rb.append(min(cand, key=lambda x: x[1])) tb = np.array([x[0] for x in hull_rb]) sb = np.array([x[1] for x in hull_rb]) bh, ch, rh = fit_affine(np.log(2.0 + tb), sb) mfl, rfl = fit_flat(sb) fit_tab[lab] = (bh, ch, rh, rfl, hull_rb) print(" delta = %-5s hull minima %s" % ( lab, " | ".join("%.4f@%.0f" % (s, t) for t, s in hull_rb))) print(" per-window log fits (c0 per delta):") win_c0 = {} for w in WIN: row = [] for lab, d in ladder(w["a"]): r = RHO[(w["a"], lab)] bm = band_minima(w["ts"][:r.size], r, BANDS) tb = np.array([x[0] for x in bm]) sb = np.array([x[1] for x in bm]) _bb, cc, _rr = fit_affine(np.log(2.0 + tb), sb) win_c0[(w["a"], lab)] = cc row.append("%s: %+.4f" % (lab, cc)) print(" a = %.4f: %s" % (w["a"], " | ".join(row))) print(" hull fits + gains vs raw (c_raw = %+.5f):" % c_raw) gains = {} meas_pairs = {} for lab in ("1/a", "pi/a", "4pi", "pi*a"): bh, ch, rh, rfl, _hb = fit_tab[lab] gains[lab] = ch / max(c_raw, 1e-4) C10 = 0.0 C20 = 0.0 for w in WIN: r = RHO[(w["a"], lab)] tsv = w["ts"][:r.size] m1 = (tsv >= T_MIN) & (tsv <= T_REP) m2 = (tsv >= 20.0) & (tsv <= T_REP) C10 = max(C10, float(np.max(ch * np.log(2.0 + tsv[m1]) - r[m1]))) C20 = max(C20, float(np.max(ch * np.log(2.0 + tsv[m2]) - r[m2]))) meas_pairs[lab] = (ch, C10, C20) print(" delta = %-5s: hull %+.4f %+.5f log(2+t) (rms %.4f " "vs flat %.4f) | measured pair (c0, C0[10..], C0[20..])" " = (%+.4f, %.4f, %.4f) | gain c0/c_raw = %.2f" % (lab, bh, ch, rh, rfl, ch, C10, C20, gains[lab])) check("F1.1 [MEASURED, central] smoothing gain on the hull " "envelope: c0(1/a) = %+.4f (gain %.2f), c0(pi/a) = %+.4f " "(gain %.2f), c0(4pi) = %+.4f (gain %.2f), c0(pi*a) = " "%+.4f (gain %.2f) -- the literal 1/a width does not fill " "the dips, the >= RvM-floor widths do" % (fit_tab["1/a"][1], gains["1/a"], fit_tab["pi/a"][1], gains["pi/a"], fit_tab["4pi"][1], gains["4pi"], fit_tab["pi*a"][1], gains["pi*a"]), True) # ------------------------------------------------ F2 peaks + gaps print("\nF2 -- peak <-> zero identification and gap structure") tsP = wP["ts"] stP = wP["s_tot"] m60 = (tsP >= 10.0) & (tsP <= 60.0) i60 = np.where(m60)[0] pk_i = local_maxima_idx(stP[i60]) + i60[0] pk = [refine_extremum(tsP, stP, i, sign=-1) for i in pk_i] pk_big = [p for p in pk if p[1] > 0.5 * max(x[1] for x in pk)] first4 = [p[0] for p in pk_big[:4]] d_quote = max(abs(fp - q) for fp, q in zip(first4, PEAK_QUOTES)) d_gamma = max(abs(fp - g) for fp, g in zip(first4, GAM[:4])) print(" first peaks (a = %.4f): %s" % ( wP["a"], ", ".join("%.3f (%.3f)" % p for p in pk_big[:8]))) check("F2.1 [E] the first four peaks of the zero-free symbol sit " "on the first four Riemann zeros: peaks %s vs quotes %s " "(max dev %.4f) vs gamma_1..4 %s (max dev %.4f), bar %.2f" % (["%.3f" % x for x in first4], list(PEAK_QUOTES), d_quote, ["%.4f" % g for g in GAM[:4]], d_gamma, BAR_PEAK), d_quote <= BAR_PEAK and d_gamma <= BAR_PEAK) m300 = (tsP >= T_MIN) & (tsP <= 300.0) i300 = np.where(m300)[0] pk3_i = local_maxima_idx(stP[i300]) + i300[0] pk3_t = np.array([refine_extremum(tsP, stP, i, sign=-1)[0] for i in pk3_i]) gam_in = GAM[(GAM >= T_MIN) & (GAM <= 300.0)] res = np.array([float(np.min(np.abs(pk3_t - g))) for g in gam_in]) frac = float(np.mean(res <= MATCH_TOL)) med = float(np.median(res)) check("F2.2 [MEASURED] matching on [10, 300] (largest window): " "%d zeros, %d peaks, matched fraction %.3f >= %.2f at tol " "%.2f, median |residual| = %.4f <= %.2f" % (gam_in.size, pk3_t.size, frac, BAR_MATCH_FRAC, MATCH_TOL, med, BAR_MATCH_MED), frac >= BAR_MATCH_FRAC and med <= BAR_MATCH_MED) gam_rep = GAM[(GAM >= T_MIN) & (GAM <= gam_max)] gaps = np.diff(gam_rep) gmax = float(np.max(gaps)) gmax_at = float(gam_rep[int(np.argmax(gaps))]) g100 = float(np.max(gaps[gam_rep[:-1] >= 100.0])) print(" zero gaps on [10, %.0f]: max = %.4f at gamma = %.3f " "(the gamma_1 -> gamma_2 gap); max above t = 100: %.4f; " "RvM certifiability floor 4 pi A1 = %.4f" % (gam_max, gmax, gmax_at, g100, RVM_FLOOR)) tt = np.arange(20.0, 2500.0, 0.05) emp = {} for w in WIN: for lab, d in ladder(w["a"]): lo = np.searchsorted(GAM, tt - d / 2.0) hi = np.searchsorted(GAM, tt + d / 2.0) emp[(w["a"], lab)] = float(np.mean(hi == lo)) print(" empty-window fractions on [20, 2500] (windows of width " "delta):") for w in WIN: print(" a = %.4f: %s" % (w["a"], " | ".join( "%s: %.4f" % (lab, emp[(w["a"], lab)]) for lab, _d in ladder(w["a"])))) e1_min = min(emp[(a, "1/a")] for a in A_FAM) e4_max = max(emp[(a, "pi*a")] for a in A_FAM) e3_max = max(emp[(a, "4pi")] for a in A_FAM) check("F2.3 [MEASURED] gap control: 1/a windows go empty " "(fraction >= %.4f on every window; the literal premise " "FAILS as a pointwise width), pi*a and 4pi windows are " "never empty (max fractions %.4f / %.4f); widths 1/a <= " "%.3f and pi/a <= %.3f sit below the RvM floor %.4f -- " "unconditional emptiness control is impossible there at " "ANY height with Trudgian constants" % (e1_min, e4_max, e3_max, 1.0 / min(A_FAM), math.pi / min(A_FAM), RVM_FLOOR), e1_min > 0.05 and e4_max == 0.0) dip_pred = np.array([zero_side(w["a"], t_star[i]) for i, w in enumerate(WIN)]) dip_res = np.abs(dip_pred - s_star_meas) _bp, slp_p, _rp = fit_affine(np.log(a_arr), np.log(np.abs(dip_pred))) p_pred = -slp_p print(" dip forensics at the matched dips t* = %s: measured %s " "/ predicted %s (zero side)" % (["%.2f" % v for v in t_star], ["%.5f" % v for v in s_star_meas], ["%.5f" % v for v in dip_pred])) check("F2.4 [MEASURED] the dips ARE the zero gaps: max |measured " "- zero-side| at the matched dips = %.2e <= %.0e; power " "fits p_meas = %.3f vs p_pred = %.3f (|dev| = %.3f <= %.1f)" " -- the a^{-1} Fejer mechanism is the kernel value at the " "gap-edge zeros, quantitatively" % (float(np.max(dip_res)), BAR_DIP_RES, p_meas, p_pred, abs(p_meas - p_pred), BAR_DIP_P), float(np.max(dip_res)) <= BAR_DIP_RES and abs(p_meas - p_pred) <= BAR_DIP_P) # ------------------------------------------------ F3 the chain print("\nF3 -- the unconditional chain: RvM + Trudgian -> " "theorem-grade (c0, C0, t0) + finite certificates") slack_min = math.inf for d in (4.0 * math.pi, math.pi * max(A_FAM)): uu = np.arange(30.0, gam_max - d / 2.0 - 1.0, 0.5) cnt = (np.searchsorted(GAM, uu + d / 2.0) - np.searchsorted(GAM, uu - d / 2.0)) slack = cnt - m_lo(uu, d) slack_min = min(slack_min, float(np.min(slack))) check("F3.0 [E] count-validity guard on the real comb: min slack " "count - Mlo = %.3f >= 0 (the cited Trudgian bound holds on " "[30, %.0f] for delta = 4pi and pi*a_max)" % (slack_min, gam_max), slack_min >= 0.0) print(" t0 / constants table (slope = (4/pi^2)(1 - 4 pi A1/" "delta); c0_thm = %.1f x slope; C0_thm = sup_{t>=t0}[c0 " "log(2+t) - B]):" % C0_SHAVE) cert = {} thm_tab = {} for w in WIN: a = w["a"] for lab, d in ladder(a): slope_fac = 1.0 - RVM_FLOOR / d if lab in ("1/a", "pi/a"): print(" a = %.4f, delta = %-5s (%7.4f): slope " "factor %+.4f < 0 -> NOT RvM-certifiable (below " "the floor %.4f), no t0" % (a, lab, d, slope_fac, RVM_FLOOR)) continue t0v = t0_tab[(a, lab)] if t0v is None or t0v > T0_FEAS: print(" a = %.4f, delta = %-5s: t0 = %s > %.0f -> " "certificate infeasible on this grid" % (a, lab, "inf" if t0v is None else "%.0f" % t0v, T0_FEAS)) continue slope = (4.0 / math.pi ** 2) * slope_fac c0t = C0_SHAVE * slope tgr = np.exp(np.linspace(math.log(t0v), math.log(1e12), 30000)) gap = c0t * np.log(2.0 + tgr) - bound_B(tgr, a, d) C0t = float(np.max(gap)) tail_dec = bool(gap[-1] < gap[-100]) uchk = np.exp(np.linspace(math.log(t0v / 2.0), math.log(1e6), 4000)) mono_L = bool(np.all(np.diff(m_lo(uchk, d)) > -1e-12)) r = RHO[(a, lab)] tsv = w["ts"][:r.size] mc = (tsv >= T_MIN) & (tsv <= t0v) margin = float(np.min(r[mc] - (c0t * np.log(2.0 + tsv[mc]) - C0t))) cert[(a, lab)] = (t0v, c0t, C0t, margin, tail_dec, mono_L) thm_tab[(a, lab)] = (c0t, C0t) print(" a = %.4f, delta = %-5s (%7.4f): t0 = %7.1f, " "c0_thm = %.4f, C0_thm = %.4f, cert margin on " "[10, t0] = %+.4f (L monotone %s, sup-tail " "decreasing %s)" % (a, lab, d, t0v, c0t, C0t, margin, mono_L, tail_dec)) n_cert = len(cert) check("F3.1 [ANALYTIC, cited] the chain closes structurally for " "delta = 4pi and pi*a on all windows: %d/10 (a, delta) " "pairs have t0 <= %.0f with monotone L and decreasing sup " "tail; below the floor (1/a, pi/a) NOTHING is certifiable " "-- the named 1/a premise is repaired by delta >= %.4f" % (n_cert, T0_FEAS, RVM_FLOOR), n_cert == 10 and all(v[4] and v[5] for v in cert.values())) n_pass = sum(1 for v in cert.values() if v[3] >= MARGIN_BAR) check("F3.2 [E-candidate] finite certificates on the zero-free " "rho grids: %d/%d margins >= %.2f -- combined with F3.1 " "this closes rho_{a,delta}(t) >= c0_thm log(2+t) - C0_thm " "for ALL t >= 10 (delta = 4pi and pi*a, every window), " "UNCONDITIONALLY given the identity" % (n_pass, n_cert, MARGIN_BAR), n_pass == n_cert == 10) # ------------------------------------------------ F4 identity print("\nF4 -- the identity s_tot = 2 pi (F_a * dN): numeric " "verification against the Turing-certified comb") v1_rows = [] v1_max = 0.0 vhi_rows = [] for w in (wA, wP): a = w["a"] ka = w["ka"] pts = [x[0] for x in raw_bands[a][:5]] pts += [p[0] for p in pk_big[:4]] if w is wP else \ [float(GAM[i]) for i in (0, 2, 4, 6)] gg = GAM[(GAM >= 12.0) & (GAM <= 320.0)] gp = np.diff(gg) top = np.argsort(gp)[-4:] pts += [float(0.5 * (gg[i] + gg[i + 1])) for i in top] pts += [float(t_star[0 if w is wA else -1])] for tp in sorted(set(round(p, 3) for p in pts)): if tp > V1_T_MAX: vhi_rows.append((a, tp)) continue sh = s_tot_hi(a, tp, ka) zs = zero_side(a, tp) r_ = abs(sh - zs) v1_max = max(v1_max, r_) v1_rows.append((a, tp, sh, zs, r_)) print(" V1 points (a, t, s_tot hi-prec, zero side, |res|):") for a, tp, sh, zs, r_ in v1_rows: print(" a = %.4f t = %8.3f %+.6f %+.6f %.2e" % (a, tp, sh, zs, r_)) blind = {} for w in (wA, wP): a = w["a"] Gm = gam_max - V1_T_MAX blind[a] = (4.0 / math.pi) * float(s_bar(gam_max)) / Gm \ + TWO_PI * float(s_bar(gam_max)) * fejer_a(a, np.array([Gm]))[0] off_bud = {} for w in (wA, wP): a = w["a"] off_bud[a] = (4.0 * math.cosh(a / 2.0) ** 2 / (math.pi * a) * math.log(RH_HEIGHT / TWO_PI) / (RH_HEIGHT - V1_T_MAX)) print(" declared budgets: oscillation-blind S-tail %s; " "off-line zeros above 3e12: %s (cosh^2(a/2) bound); " "quadrature ~1e-8 (Euler-Maclaurin boundary)" % (["a=%.2f: %.1e" % (a, b) for a, b in blind.items()], ["a=%.2f: %.1e" % (a, b) for a, b in off_bud.items()])) check("F4.1a [E] V1 pointwise identity: max |s_tot - 2 pi " "(F_a * dN)| = %.2e <= %.0e over %d points, both windows " "(cache-tail-limited; bar assumes the measured oscillatory " "cancellation of the S-tail, blind budget printed)" % (v1_max, BAR_V1, len(v1_rows)), v1_max <= BAR_V1) v2_stats = [] for w in (wA, wP): a = w["a"] ka = w["ka"] tv = np.arange(50.0, 250.0 + 0.5, 1.0) wts = np.hanning(tv.size) wts /= wts.sum() rr = np.array([s_tot_hi(a, float(t), ka) - zero_side(a, float(t)) for t in tv]) v2_stats.append((a, float(abs(np.sum(wts * rr))), float(np.max(np.abs(rr))))) check("F4.1b [E] V2 t-averaged identity (Hann on [50, 250], 201 " "points): %s -- the 1e-6 target; bar %.0e on the weighted " "mean" % (["a=%.4f: |mean| = %.2e (max %.2e)" % v for v in v2_stats], BAR_V2), max(v[1] for v in v2_stats) <= BAR_V2) if vhi_rows: print(" high-t points (> %.0f, printed, no bar):" % V1_T_MAX) for a, tp in vhi_rows: w = wA if abs(a - wA["a"]) < 1e-12 else wP sh = s_tot_hi(a, tp, w["ka"]) zs = zero_side(a, tp) print(" a = %.4f t = %8.3f %+.6f %+.6f %.2e" % (a, tp, sh, zs, abs(sh - zs))) # ------------------------------------------------ verdict + typing guards_ok = not any(f.startswith(("G0", "F3.0")) for f in FAILS) ident_ok = not any(f.startswith("F4.1") for f in FAILS) peaks_ok = not any(f.startswith("F2.1") for f in FAILS) all_certs = (n_pass == 10) c0_thm_min = min((v[0] for v in thm_tab.values()), default=0.0) gain_thm = c0_thm_min / max(c_raw, 1e-4) gain_ok = gain_thm >= GAIN_THM_MIN if not guards_ok: VERDICT = "FEJER-MIXED (guards failed)" elif ident_ok and peaks_ok and all_certs and gain_ok: VERDICT = "FEJER-DENSITY-THEOREM" elif ident_ok and n_pass >= 1: VERDICT = "FEJER-DENSITY-PARTIAL" elif ident_ok: VERDICT = "FEJER-IDENTITY-ONLY" else: VERDICT = "FEJER-NO-GAIN" check("F4.2 [C] typed reading: (i) THEOREM-GRADE (cited " "constants): RvM + Trudgian |S| ==> rho_{a,delta}(t) >= " "c0_thm log(2+t) - C0_thm for t >= t0 at delta in {4pi, " "pi*a}, min c0_thm = %.4f = %.1f x the raw measured hull " "c0 = %+.5f, with the finite remainder [10, t0] " "machine-checked on the zero-free rho ([E]-candidate); " "(ii) EXACT (derived, verified numerically): s_tot = 2 pi " "(F_a * dN) via the Weil explicit formula on the tent " "class -- pointwise to %.1e (cache-limited), t-averaged " "to %.1e; distributional caveats: tent admissibility " "classical, off-line zeros above 3e12 budgeted at %.1e; " "(iii) MEASURED: smoothing gains, peak/gap forensics; " "(iv) OPEN / honest breach: the literal 1/a (and the " "plane-wave pi/a) window sits BELOW the RvM floor 4 pi A1 " "= %.4f -- per-mode symbol control (the raw Garding drift) " "is NOT certifiable this way at any height; the theorem " "controls the smoothed density, i.e. wave packets of " "spectral width >= delta, not single DST modes. W2 (A5(a) " "discrete Garding, Mosco liminf) stays OPEN; no marker move" % (c0_thm_min, gain_thm, c_raw, v1_max, max(v[1] for v in v2_stats), max(off_bud.values()), RVM_FLOOR), True) print("\nVERDICT: %s" % VERDICT) print(""" CONTRACT-NOTE TEXT (report only -- nothing is written by this probe): PRIME.WEIL.OPERATOR.01 / W2, Fejer density round (2026-08-02): the renamed residual task of the envelope round -- a lower bound for the Fejer-smoothed spectral density of the total symbol -- was STRUCTURED and MEASURED. (1) IDENTITY (exact, Weil explicit formula on the tent class): s_tot(.; a) = 2 pi (F_a * dN), the Fejer-smoothed zero-counting density; verified numerically to %.1e pointwise / %.1e t-averaged against the Turing-certified 2000-zero comb; the envelope peaks ARE the zeros gamma_n (first four matched to %.4f), the dips ARE the zero gaps (dip forensics residual %.1e, Fejer p_meas/p_pred = %.2f/%.2f). (2) THEOREM CHAIN (unconditional, cited: Trudgian 2014 |S| <= 0.112 log t + 0.278 loglog t + 2.510; Platt-Trudgian 3e12; theta-remainder 2e-3): windowed RvM counting + Fejer box minorant + F_a mass transfer give rho_{a,delta}(t) >= c0_thm log(2+t) - C0_thm for t >= t0(a, delta), with the finite remainder [10, t0] machine- checked on the ZERO-FREE rho grid (certificates: %d/10 margins >= %.2f; min c0_thm = %.4f vs raw measured hull c0 = %+.5f, gain %.1f x). (3) THE HONEST FLOOR: the chain closes only for smoothing widths delta > 4 pi A1 = %.4f; the literal 1/a and the plane-wave resolution pi/a sit BELOW the floor for every frame-A window (pi/a certifiable only for a < %.4f < a0 = log 16) -- the Garding 1/log drift of the LATTICE route is thereby explained and typed: single DST modes see the un-smoothed density in a zero gap (depth ~ 1/(pi a d^2)); only spectral-width >= delta packets are covered by the theorem. TYPE: identity = derived + verified; density bound = theorem-grade modulo cited constants + finite [E]-candidate certificate; the pointwise A5(a) Garding inequality and W2 stay OPEN; no marker move. VERDICT %s. """ % (v1_max, max(v[1] for v in v2_stats), d_gamma, float(np.max(dip_res)), p_meas, p_pred, n_pass, MARGIN_BAR, c0_thm_min, c_raw, gain_thm, RVM_FLOOR, 1.0 / (4.0 * A1_TR), VERDICT)) print("checks: %d, failures: %d %s" % (N_CHK, len(FAILS), FAILS or "")) print("elapsed: %.1f s" % (time.time() - T0)) return len(FAILS) if __name__ == "__main__": raise SystemExit(1 if run() else 0)