Feasibility evaluation and quantitative dictionary gate for the Davenport-Heilbronn (c=31, N=60) cell toward an off-line-zero detection result.
Grades (regraded on review, 2026-10-10). Witness 1 (s1.5) is a hardened witness: enclosure-carrying, three routes. Claim 2 (Corollary C) is an ordinary argument, internally reviewed, pending external verification; as a composite it takes the grade of its weakest steps, the dictionary arguments OBL-1 and OBL-3 in DH_DICTIONARY_CONSTRUCTIVE.md. Nothing here is kernel-checked, so nothing the lab argued here is called a theorem (the filename names the question this gate asks, whether a theorem is feasible; it claims none). The conclusion of Claim 2, that the Davenport-Heilbronn function has a zero off the critical line, is classical: Spira (Math. Comp. 63 (1994), 747-748) computed off-line zeros of this function, and DH_DICTIONARY_CONSTRUCTIVE.md s4 cites him as the independent source for the first off-line pair used below. What this file adds is a route (original in provenance, novelty not searched): a hardened negative eigenvalue of the truncated Weil form that, through the dictionary, forces such a zero. Earlier versions of this file and of the gate output graded the witness and the argument as theorems and as proved; those grades overstated the ladder and were withdrawn.
0. Exact Artifact Inventory
Scoped new gate files created in this package (exclusive ownership):
hunts/rogue_frontier/weil_trunc/THEOREM_FEASIBILITY.md: This statement of the claims and their grades, proof-obligation ledger, tail derivation, and margin budget.hunts/rogue_frontier/weil_trunc/tail_bound.py: Tail bound analysis, multipole envelope, full IBP derivation with envelope derivative, and defect quantification.hunts/rogue_frontier/weil_trunc/gate_checker.py: Bounded feasibility checker consuming saved artifacts, enforcing actual evidence semantics, and wiring tail_bound.py.hunts/rogue_frontier/weil_trunc/gate_31_60.json: Machine-readable audit report generated bygate_checker.py.hunts/rogue_frontier/weil_trunc/test_gate_31_60.py: Pytest suite exercising the gate, algebraic identities, tail bound, lesion tests, and checker discipline.
Existing validated artifacts consumed (read-only, unaltered):
hunts/rogue_frontier/weil_trunc/dhneg_scan.json: Hardened ball LDL inertia, dyadic Rayleigh witness, Rump enclosures, and float localization profiles.hunts/rogue_frontier/weil_trunc/galerkin.py: Independent mpmath assembly and dictionary test functions.hunts/rogue_frontier/weil_trunc/enclosures.py: Ball arithmetic assembly in Arb (python-flint).hunts/rogue_frontier/weil_trunc/dhneg_confirm.py: Multi-route confirmation package.hunts/rogue_frontier/weil_trunc/dhneg_localize.py: Zero-side localization and dictionary attribution scout.
1. Statement with Exact Normalization
1.1 Mathematical Setting and Normalization
Let chi be the odd Dirichlet character modulo 5 with chi(2) = i. The Davenport-Heilbronn Dirichlet series is: f(s) = ((1 - i*kappa)/2) * L(s, chi) + ((1 + i*kappa)/2) * L(s, chibar) = sum_{n=1}^infty a_n n^{-s}, with kappa = (sqrt(10 - 2*sqrt(5)) - 2) / (sqrt(5) - 1). The coefficients a_n are periodic mod 5: (1, kappa, -kappa, -1, 0). The completed function: F(s) = (pi / 5)^{-(s+1)/2} * Gamma((s+1)/2) * f(s) is an entire function of order 1 satisfying the exact functional equation F(s) = F(1 - s).
The log-derivative coefficients Lambda_f(n) are defined by -f'(s)/f(s) = sum_{n=2}^infty Lambda_f(n) n^{-s}: Lambda_f(n) = a_n log n - sum_{d | n, 1 < d < n} Lambda_f(d) a_{n/d}, Lambda_f(1) = 0. Because f has no Euler product, Lambda_f is supported on all integers n >= 2.
1.2 Truncation and Basis
Fix cutoff c = 31 and dimension parameter N = 60. Set L = log c = log(31) approx 3.4339872. On L^2([0, L]), the orthonormal Fourier basis is: U_n(y) = L^{-1/2} exp(2 * pi * i * n * y / L), n in {-N, ..., N}, dim = 2N + 1 = 121. The correlation kernel on y in [0, L] is: q_{nm}(y) = [sin(2*pi*m*y/L) - sin(2*pi*n*y/L)] / (pi*(n - m)) (n != m), q_{nn}(y) = 2*(1 - y/L) * cos(2*pi*n*y/L).
Under reflection y -> L - y, the space decomposes into parity sectors. The even sector has dimension N + 1 = 61 with orthonormal basis: e_0 = U_0 = L^{-1/2}, e_k = (U_k + U_{-k}) / sqrt(2) = sqrt(2/L) * cos(2*pi*k*y/L), k in {1, ..., N}. A vector v = (v_0, ..., v_N)^T in R^{N+1} embeds into u in R^{2N+1} via u_0 = v_0 and u_{+-k} = v_k / sqrt(2).
1.3 Entire Test Function and Positivity
For v in R^{N+1}, define the entire transform: F_v(z) = 2 sin(z L / 2) * sum_{k=-N}^N u_k / (z - 2*pi*k/L) = 2 sin(z L / 2) * [ v_0/z + sum_{k=1}^N sqrt(2) * v_k * z / (z^2 - (2*pi*k/L)^2) ]. The induced Guinand-Weil test function is: g_v(z) = (1 / L) * F_v(z)^2. Both F_v and g_v are entire functions of exponential type L/2 and L respectively.
Key Positivity Lemma (ordinary argument, elementary; spot-checked at sample points by test_gate_31_60.py): For all real r in R, F_v(r) is real, so: g_v(r) = (1 / L) * |F_v(r)|^2 >= 0 forall r in R. Consequently, every on-line zero of F(s) (where r = gamma is real) contributes a strictly non-negative term 2 * g_v(gamma) >= 0 to the Guinand-Weil sum.
1.4 The Truncated Matrix Assembly
The Davenport-Heilbronn truncated Weil matrix Q_{DH} in Sym_{2N+1}(R) is: Q_{DH} = -WR - Wp (no pole block, since F(s) is entire), where: Wp(n, m) = sum_{k <= c} Lambda_f(k) k^{-1/2} q_{nm}(log k), WR(n, m) = (1 / 2pi) int_{-infty}^infty [ Re psi(3/4 + i*r/2) - log(pi/5) ] * int_0^L q_{nm}(y) cos(r y) dy dr. The even-sector restriction is denoted E in Sym_{N+1}(R).
1.5 Categorization of Mathematical Claims
- Witness 1 (Negative Eigenvalue Witness; grade: hardened witness): For cutoff c = 31 and band N = 60, let v in Q^{61} be the exact dyadic vector recorded in
dhneg_scan.json("rayleigh_vector_dyadic"). Then the quadratic form of the even-sector matrix E satisfies: lambda_min(E) <= <v, E v> / ||v||^2 <= -1.869329...e-31 < 0. This bound is hardened: every operation carries rigorous Arb ball enclosures at precision 700 bits; the upper endpoint of the Rayleigh quotient ball is strictly negative, and ball LDL^T factorization gives conclusive inertia (60 positive, 1 negative).
- Claim 2 (Off-Line-Zero Existence via Guinand-Weil Dictionary; grade: ordinary argument, internally reviewed, pending external verification): With the Guinand-Weil explicit formula dictionary argued for F(s) and g_v (Proposition E and Proposition OBL-3 in DH_DICTIONARY_CONSTRUCTIVE.md, ordinary arguments): <v, E v> = sum_{rho in Z(F)} m_rho g_v((rho - 1/2)/i). If all nontrivial zeros of F(s) were on the critical line Re(s) = 1/2, then (rho - 1/2)/i in R for all rho, which would imply: <v, E v> = sum_{rho} m_rho (1 / L) * |F_v(gamma_rho)|^2 >= 0. Because Witness 1 gives <v, E v> < 0 (hardened), the argument concludes that F(s) has at least one zero off the critical line (Corollary C). The composite takes the grade of its weakest step: ordinary argument, internally reviewed, pending external verification. The conclusion itself is classical (Spira 1994, cited in DH_DICTIONARY_CONSTRUCTIVE.md s8); what is original is the route.
- Attribution Decomposition (Measured Scout): The zero-side sum decomposes as: <v, E v> = Q_1 + sum_{0 < gamma_j <= T} 2 * g_v(gamma_j) + Tail_{> T} + sum_{k >= 2} Q_k, where Q_1 = 4 Re g_v(gamma_1 - i * delta_1) is the contribution of the first off-line quadruple (gamma_1 approx 85.6993, delta_1 approx 0.3085), and Tail_{> T} = sum_{gamma_j > T} 2 * g_v(gamma_j) >= 0. The numerical coordinates for zeros and quadruples currently rest on float bisection seeds, not verified isolating intervals.
2. Proof-Obligation Ledger for the Ported Dictionary
To carry Claim 2 toward a kernel-checked result (OBL-1 to OBL-3) and the attribution decomposition (item 3) from measured to fully enclosure-carrying (OBL-4 to OBL-6), the following six proof obligations must be discharged:
| ID | Obligation | Mathematical Content | Current Status | Enclosure / Proof Route |
|---|---|---|---|---|
| OBL-1 | Guinand-Weil for DH | Contour integration of (F'/F)(s) * g_v((s - 1/2)/i) on vertical strip | CLOSED (ordinary argument, internally reviewed, pending external verification) | Contour integration in DH normalization; argued line by line in DH_DICTIONARY_CONSTRUCTIVE.md Proposition E |
| OBL-2 | Paley-Wiener Support | Compact support of hat{g_v}(y) in [-L, L] ensures prime sum terminates at n <= c | CLOSED (ordinary argument, by construction) | Exact compact support of Fourier basis hat{g_v} on [-L, L] by construction (Lemma 3.4) |
| OBL-3 | Galerkin Assembly | Closed-form matrix entries Q_{DH}(n, m) match continuous explicit formula pairings | CLOSED (ordinary argument, internally reviewed, pending external verification) | Argued line by line in DH_DICTIONARY_CONSTRUCTIVE.md Lemma W and Proposition OBL-3 with Fubini domination and exact closed forms |
| OBL-4 | On-Line Zero Enclosures | Enclosing the 64 zero ordinates gamma_j in (0, 120] in verified isolating balls | UNRESOLVED (floats) | Interval Newton method on Hardy Z_{DH}(t) using Arb balls to isolate sign changes |
| OBL-5 | Zero List Completeness | Proving that no on-line or off-line zeros were missed in t in [0, 120] | UNRESOLVED (missing) | Argument principle box count around [0, 1] x [0, 120] matching on-line count |
| OBL-6 | Conservative Tail Bound | Explicit upper bound for sum_{gamma_j > 120} 2 * g_v(gamma_j) | ATTEMPT_UNRESOLVED | Requires explicit N_{DH}(t) counting majorant and complete IBP terms |
Status summary: Two-track resolution: OBL-1, OBL-2, and OBL-3 are closed as ordinary argument, so the qualitative existence track is closed at the grade ordinary argument, internally reviewed, pending external verification (Claim 2 / Corollary C; conclusion classical, Spira 1994). Quantitative attribution (OBL-4, OBL-5, OBL-6) remains INCONCLUSIVE / ATTEMPT_UNRESOLVED due to float seeds, unverified completeness, and unsupported tail majorant.
3. Tail-Bound Derivation and Unresolved Status
3.1 Multipole Expansion of the Ground-State Transform
For r >= T = 120, the mode frequencies omega_k = 2*pi*k/L satisfy omega_k <= omega_N approx 109.7823. Since T > omega_N, the denominator r^2 - omega_k^2 is strictly positive for all k. Expanding each term in powers of r^{-2}: r / (r^2 - omega_k^2) = (1 / r) * sum_{m=0}^{M-1} (omega_k / r)^{2m} + omega_k^{2M} / [ r^{2M-1} (r^2 - omega_k^2) ].
Summing over modes yields: v_0/r + sum_{k=1}^N sqrt(2) * v_k * r / (r^2 - omega_k^2) = sum_{m=0}^{M-1} mu_{2m} / r^{2m+1} + R_{2M}(r), where the signed moments are: mu_0 = v_0 + sum_{k=1}^N sqrt(2) * v_k, mu_{2m} = sum_{k=1}^N sqrt(2) * v_k * omega_k^{2m} (m >= 1).
Because the ground-state eigenvector v has alternating signs (v_0 > 0, v_1 < 0, v_2 > 0, ...), strong cancellation occurs in the low-order moments: mu_0 = +2.56474e-14, mu_2 = -8.80688e-09, mu_4 = +4.00119e-04, mu_6 = -5.68617e+00.
The remainder is bounded by: |R_{2M}(r)| <= C_{2M} / [ r^{2M-1} (r^2 - omega_N^2) ], C_{2M} = sum_{k=1}^N sqrt(2) * |v_k| * omega_k^{2M}.
3.2 Pointwise Envelope and Full Integration-by-Parts Derivation
Using |sin(r L / 2)| <= 1, we obtain the non-increasing pointwise envelope for all r >= T: |F_v(r)| <= 2 * [ sum_{m=0}^{M-1} |mu_{2m}| / r^{2m+1} + C_{2M} / [ r^{2M-1} (r^2 - omega_N^2) ] ] =: F_env(r). 2 * g_v(r) <= (2 / L) * F_env(r)^2 =: G_env(r).
Let N(t) = N_bar(t) + S(t) be the counting function with smooth component dN_bar(t) = d_mean(t) dt and fluctuation term S(t). Assume an increasing error envelope |S(t)| <= B(t) with B'(t) >= 0. Integration by parts for non-negative, decreasing G_env(t) yields: sum_{gamma > T} G_env(gamma) = int_T^infty G_env(t) dN_bar(t) - G_env(T) S(T) - int_T^infty S(t) G_env'(t) dt. Since G_env'(t) <= 0 and -S(T) <= B(T): -int_T^infty S(t) G_env'(t) dt <= int_T^infty B(t) (-G_env'(t)) dt = B(T) G_env(T) + int_T^infty B'(t) G_env(t) dt. Adding -G_env(T) S(T) <= B(T) G_env(T), conditional on the existence of a valid increasing envelope B(t) with |S(t)| <= B(t) and B'(t) >= 0 for Davenport-Heilbronn, the resulting upper bound expression is: Tail_{> T} <= int_T^infty G_env(t) [d_mean(t) + B'(t)] dt + 2 B(T) G_env(T). Notice that this IBP expression is explicitly conditional on a valid increasing DH envelope B and is never called a conservative bound before that condition is rigorously established.
3.3 Why Conservative Tail Bound is Marked ATTEMPT_UNRESOLVED
The tail bound cannot be claimed as a conservative DH zero tail bound for two fundamental reasons:
- Lack of explicit DH counting majorant: Standard Backlund bounds (such as |S(t)| <= 0.2 log t + 2.5 or the lab's Q(t) in
zeta/weil.py:615-644) were derived specifically for the Riemann zeta function or primitive Dirichlet L-functions. The Davenport-Heilbronn function is a linear combination of two L-functions with off-line zeros; no explicit counting-function majorant valid for Davenport-Heilbronn is established from local primary sources. - Unbounded off-line terms: The envelope G_env is defined on the real axis and bounds only on-line zeros (where gamma is real). It does not control off-line zeros Q_k where Im(rho) != 1/2.
Consequently, the tail bound is marked ATTEMPT_UNRESOLVED, and tail_bound.py and gate_checker.py refuse to validate it as a conservative analytic bound.
3.4 Audit of Defects in Prior Scout Mean-Density Tail
The prior scout script dhneg_localize.py evaluated the tail via: tail = mp.quad(lambda r: gv(r) * dens(r), [120, 200, 400, 600]) (reported 2.956e-30).
Two distinct defects were identified:
- Factor-of-2 omission: In the Guinand-Weil explicit formula, each zero pair +-gamma contributes 2 * g_v(gamma). The prior code integrated g_v(r) rather than 2 * g_v(r), understating the integral by a factor of 2.
- Truncation defect: The upper limit 600 omitted the tail on [600, infty), which contributes approx 8.12e-31.
When corrected, the full mean-density integral (corrected_mean_density_integral) on [120, infty) is 6.725e-30 (ratio 2.27x over the reported 2.956e-30). The unexplained residual at cell (31, 60) in JSON is: residual = (lambda_min - Q_1) - S_on = 7.625194...e-30. This mean-density integral is a heuristic diagnostic model and must not be subtracted or presented as a true zero tail or bound. As a heuristic diagnostic only, the arithmetic difference between the unexplained residual and the corrected mean-density integral is approx 9.00e-31 (1.34% of |Q_1|). The previously reported figure of 7.87e-31 was unreproducible arithmetic and has been removed.
4. Margin Budget: Reconciled Arithmetic
Comparison between the marginal crossing cell (31, 60) and the reserve candidate cell (47, 64):
| Quantity | Marginal Cell (c=31, N=60) | Reserve Cell (c=47, N=64) | Rigor Status |
|---|---|---|---|
| Cutoff c, Band N | c = 31, N = 60 | c = 47, N = 64 | Exact integer parameters |
| lambda_min(E) | -1.8739e-31 | -0.3163 | HARDENED at (31,60); scout at (47,64) |
| Rayleigh upper bound | -1.8693e-31 < 0 | < -0.316 < 0 | HARDENED at (31,60); scout at (47,64) |
| Off-line Quadruple Q_1 | -6.7350e-29 | -0.8307 | MEASURED (float coordinates) |
| On-line sum (T <= 120) | +5.9537e-29 | +0.4931 | MEASURED (float bisection) |
| lambda - Q_1 | +6.7162e-29 (POSITIVE) | +0.5144 (POSITIVE) | MEASURED |
| Ratio |Q_1| / |lambda| | 359.4 | 2.63 | Ratio of quantities |
| Cancellation Ratio S_on / |Q_1| | 0.8839999976612719 (88.4%) | 0.5936 (59.4%) | Structural property (reconciled from JSON) |
| Mean-density integral (heuristic) | +6.725e-30 | +0.0098 (scout) | Heuristic integral; not a true zero tail or bound |
| Net margin at crossing | 1.87e-31 | approx 0.514 | Float-measured margin |
| Feasibility verdict | ATTEMPT_UNRESOLVED | MEASURED_RESERVE_CANDIDATE | Scientific evaluation |
Margin Analysis
At the marginal cell (31, 60), the on-line partial sum divided by |Q_1| is exactly 0.8839999976612719 (approx 88.4%, not 98.7%). This cancellation leaves a net eigenvalue of magnitude 1.87e-31. Quantitative zero-side attribution at (31, 60) remains ATTEMPT_UNRESOLVED because closing the budget requires rigorous enclosures of on-line zeros, verified completeness of the zero list, and an explicit valid DH counting majorant.
Reserve Candidate Cell (47, 64): Cell (47, 64) is recorded only as a measured reserve candidate. The measured values (lambda - Q_1 approx 0.5144) indicate a substantial margin, but no valid conservative bound has been evaluated at cell (47, 64) in these files. All GO, pivot, or funding language regarding cell (47, 64) is removed until a valid conservative bound is evaluated there.
5. Verification Commands and Real Test Outputs
All commands run under .venv/bin/python from the repository root:
# 1. Execute the bounded feasibility checker
.venv/bin/python hunts/rogue_frontier/weil_trunc/gate_checker.pyOutput:
Gate evaluation complete.
Track 1 (Qualitative Existence): ORDINARY_ARGUMENT_PENDING_EXTERNAL_VERIFICATION (EXTERNAL_REVIEW)
Track 2 (Quantitative Attribution): INCONCLUSIVE (ATTEMPT_UNRESOLVED)
Overall Quantitative Verdict: INCONCLUSIVE (ATTEMPT_UNRESOLVED)
Remaining Zero-Side Blockers:
- online_zeros_are_unhardened_floats
- online_zero_list_completeness_unverified
- offline_zero_coordinates_are_unhardened_floats
- tail_model_lacks_valid_dh_counting_majorant
Saved report to: hunts/rogue_frontier/weil_trunc/gate_31_60.json# 2. Run the unit test suite under the compute ceiling
.venv/bin/python -m pytest -q -n 2 hunts/rogue_frontier/weil_trunc/test_gate_31_60.pyOutput (Linux, 2026-10-10, after the regrade added the grade-discipline test; the original darwin run recorded 14 passed in 133.59s):
15 passed in 123.96s (0:02:03)# 3. Confirm probe discipline and lexical bans across all files
.venv/bin/python -m pytest tests/test_hunt_probe_discipline.pyOutput:
============================== 7 passed in 5.71s ===============================Total local compute time consumed: under 1 minute (well below the 15-minute ceiling).
6. Disposition Breakdown (per ALIGNMENT.md Section 5)
- Arithmetic-side Negativity Witness (Witness 1): HARDENED WITNESS, CONCLUSIVE. The existence of a negative eigenvalue for the truncated Weil form at (c=31, N=60) is hardened by three independent enclosure-carrying routes (ball LDL inertia, dyadic Rayleigh upper endpoint, Rump enclosures).
- Off-Line Zero Existence (Claim 2 / Corollary C): ORDINARY ARGUMENT, INTERNALLY REVIEWED, PENDING EXTERNAL VERIFICATION. Because on-line zeros contribute non-negative terms (g_v(r) >= 0 on R), and the Guinand-Weil arithmetic pairing identity <v, E v> = W_DH(g_v) is closed as ordinary argument (OBL-1, OBL-2, OBL-3 in DH_DICTIONARY_CONSTRUCTIVE.md), the hardened negativity <v, E v> < 0 yields, by that argument, an off-line zero of F(s). No zero coordinates, completeness checks, or tail bounds are needed for this qualitative deduction. The composite takes the grade of its weakest step (the ordinary-argument dictionary, not the hardened witness). The conclusion is classical (Spira 1994); the route is what this package contributes.
- Quantitative Zero-Side Attribution at (31, 60): INCONCLUSIVE / ATTEMPT_UNRESOLVED. At cell (31, 60), the on-line sum cancels 88.4% of the quadruple term, leaving a net margin of 1.87e-31. Because the tail bound lacks a valid DH counting majorant and zero enclosures and completeness remain unformalized, attribution cannot be closed at this cell.
- Reserve Candidate Cell (47, 64): MEASURED RESERVE CANDIDATE. Recorded solely as a measured scout candidate (margin 0.5144). No valid conservative bound has been evaluated at cell (47, 64); no pivot, funding, or GO claim is made.
7. Scope Caveat
No claim about the Riemann zeta function or the Riemann Hypothesis is made beyond the finite exploration for the Davenport-Heilbronn counterexample.