Record

blockpos-0.672529

the constructive block-positivity residue transplants to the pinned upstream zero side, giving 0.672529 unconditionally

claimed by frontier_math blockpos session (2026-08). positivity of each block was checked numerically; the construction was believed basis-independent

rested on: the upstream zero side uses u u* (it uses u u^T)

rested on: off-line pair blocks interact non-negatively with on-line part

Antigravity Zeta Lab Researcher (blind) found: If an instrument evaluates u u^* instead of u u^T, it constructs a Gram matrix that is PSD by definition. This preserves the appearance of block positivity, but makes the interpretation false.; For an off-line root, u u^T + u_conj u_conj^T = 2(xx^T - yy^T), which is a hyperbolic block.

Luke Kenneth Casson Leighton, with an instance of ChatGPT they call C.A.T., unsolicited, via the zeta.teal-sea.com contact form, 2026-09-08 and 2026-09-09 (white-box) found: the generalization, which this ledger did not have: do not square, Hermitianize, or pass to a positive quadratic object until the signed or oriented carrier has been discharged, because x -> x^2, T -> T T* and u u^T -> u u* each quotient out the sign, orientation, conjugation or phase datum the intended theorem still…

frontier_math clean-kill session (2026-08-11) (white-box) found: the pinned upstream zero side uses u u^T, not u u*: an off-line pair is the hyperbolic block 2m(xx^T − yy^T), whose interaction with the on-line part can be negative; exact witness u_x=1, u_z=i, u_conj(z)=-i gives tr(P1 Q') = -2; with five unit on-line labels the final inequality reads 9 >= 13

urms2-0.51

the URMS2 bandwidth extends past the half band to 0.51, with the algebraic frontier formalized (main, 503158a and ancestors)

claimed by urms2 bridge sessions (2026-08-11). several apparent bandwidth barriers were artifacts of lossy estimates; this one fell to preserving frequency separation

rested on: the true logarithmic frequency separation is preserved rather than collapsed into a cutoff estimate

Fulcrum hunt R-FB9C81 (run 36a6a319, Antigravity, 2026-08-15) (blind) found: no structural failure found in the RC2 off-diagonal error bounds: the claim survives this attack; the arithmetic conditions the Montgomery-Vaughan mean-value theorem requires hold past the half-band, because coefficient decay absorbs the increased polynomial length

Fulcrum hunt R-065F29 (run 726a6b3f, Claude Opus 5, 2026-08-16) (white-box) found: the mathematics of the half-band crossing survives: the exact block second moment saturates to four significant figures (17.2964 to 17.3642) while W/U grows from 1.3 to 9.9, which is the W-independence the claim asserts, measured in the regime the old proof's W/U = o(1) forbade; section 4's partial summation is…

Fulcrum hunt R-2AC05F (run 55786d8e, Claude Opus 5, 2026-08-20) (white-box) found: the xi-double-prime form-factor row that hunts/higher_xi/ C2_EXACT.json and C2_EXTENDED.json rest on survives an independent fourth derivation: a formal Dirichlet word algebra written for this adjudication, importing neither hunt, reproduces C_2,i = 1, -8, 24, -32, 64/3, -64/3, 1216/45, -256/15, 1088/63, -11776/945…

rf-c003-window

the quartic window v*(s) = 1 - (1467/1000)s^2 + (1159/1000)s^4 improves the source paper's cos(8s/5) window, giving F(v*) = 2245228120295149280/3276332462159207451 and the RH-conditional constant 50176758585216887915/58973984318865734118 (hunts/rogue_frontier/window_opt/, landed 2026-08-21)

claimed by rogue_frontier campaign (2026-08-17/18). an even quartic has enough freedom to beat the paper's single cosine, and the whole functional is exactly rational on that class, so the improvement can be stated without any float

rested on: the source paper's SS7.1 and SS7.5(g) functional is transcribed correctly, so the optimisation is over the right F

rested on: the claim is RH-conditional and is not stated otherwise

Fulcrum hunt R-F00E48 (run 8b5765ae, Claude Opus 5, 2026-08-21) (white-box) found: this is a landing check, not a mathematical attack, and it is recorded as one so nobody later mistakes it for review: the hunt salvaged window_opt/ onto main and re-ran the arm's own code, so it shares every assumption the claim makes; what it does establish: moments_polyeven_exact(OPT_Q) recomputes F =…

k2-far-constant-depth1

the far-field constant 637/1000 does not survive at depth 1: sup Dam*(s^2-2)/y^2 measures 0.6636 > 0.637 there, so Wt_tail_le's 637/1000 is a correction any depth-1 argument must carry (K2-TWO-SPECIES.md section 2, 2026-08-15)

claimed by frontier_math two-species session (2026-08-15). the depth-1/2 scan gives 0.6220 < 0.637 and the depth-1 scan gives 0.6636 > 0.637, so the constant looked like it was being crossed as depth rose

rested on: the scanned range [8, 400] is the range on which 637/1000 is asserted (it is not: Wt_tail_le is stated for w = s^2-2 >= 1368, i.e. s >= 37.0135)

rested on: the failing constant belongs to Wt_tail_le (it does not: that lemma has no depth variable in its statement)

Fulcrum hunt R-A7C12F (run e09a7f8a, Claude Opus 5, 2026-08-23) (white-box) found: the claim is withdrawn: 637/1000 DOES survive at depth 1 on the range it is asserted on. An Arb pass at 96 bits over s in [37.0135, 400] with the depth as a thin ball gives sup Dam(1,s)*(s^2-2) <= 0.6317736, against 637/1000, margin +0.0052 (0.82%).

qrh-linnik-7/3

given OpenAI's Theorem 1.1 (no Dirichlet L-function vanishes in Re s > 7/8) and Chen-Gupta-Li's single-modulus zero-density estimate (arXiv:2507.08296v2, a preprint), the least prime p = a (mod q) with (a, q) = 1 satisfies p(q, a) <= C(eps) q^(7/3 + eps) for every modulus q and every class a, with C(eps) effective; on refereed density inputs alone the exponent is 12/5 (hunt #123, hunts/qrh_linnik/, PR #277, landed 2026-10-08). Grade: candidate, pending external review: an ordinary written proof that no person has reviewed, on an input whose argument no person has reviewed

claimed by hunt #123 session (qrh_linnik, branch hunt/qrh-linnik, 2026-10-08). a smoothed explicit formula with height cutoff a small power of x; the half-plane removes every zero above 7/8, so the Siegel zero, Deuring-Heilbronn repulsion and log-free density estimates drop out of the argument, and L is set by the single-modulus density exponent on [1/2, 7/8], which binds at sigma = 5/7 where Ingham's mean value bound meets CGL's q1^(1/3) term; CGL already state the conditional implication (Corollary 1.4), so nothing is claimed novel

rested on: OpenAI, 'The Quasi-Riemann Hypothesis' (preprint dated 2026-09-30), Theorem 1.1: zeta and every Dirichlet L-function have no zero with Re s > 7/8. Its Lean statements were rebuilt here and accepted by Lean's kernel and the independent NanoDa kernel (docs/38 section 7); its 195-page argument has been reviewed by no person

rested on: Chen-Gupta-Li Theorem 1.2 (arXiv:2507.08296v2, unrefereed) holds as stated for a single modulus, including its q1^(1/3) gcd-twist term, which sets 7/3

no adversarial pass recorded. This claim is open, not confirmed

qrh-class-number-1500

given OpenAI's Theorem 1.1 (no Dirichlet L-function has a zero with Re s > 7/8), h(D) >= sqrt|D| / (10 pi log log |D|) for every negative fundamental discriminant D, and L(1, chi_D) >= 1/(10 log log |D|) for every such D other than -3; hence the imaginary quadratic fields of class number h are exactly those the hunt's exact search finds, for every h <= 1500: 9 245 562 fields, the largest with |D| = 562 394 347 (hunt #124, hunts/qrh_class_number/, PR #279, landed 2026-10-08). Grade: candidate, pending external review: an ordinary written proof that no person has reviewed, every constant evaluated in Arb (enclosure-carrying), the lists by exact integer computation, on an input whose argument no person has reviewed

claimed by hunt #124 session (qrh_class_number, branch hunt/qrh-class-number, 2026-10-08). Littlewood's short Euler product with two Cesaro cutoffs, and Hadamard positivity for the zero sum with every zero charged at beta = 7/8, make L(1, chi_D) explicitly large; a verified interval cover gives D(h), and an exact reduced-form sieve without GRH then enumerates every fundamental discriminant below D(1500)

rested on: OpenAI, 'The Quasi-Riemann Hypothesis' (preprint dated 2026-09-30), Theorem 1.1: zeta and every Dirichlet L-function have no zero with Re s > 7/8. Its Lean statements were rebuilt here and accepted by Lean's kernel and the independent NanoDa kernel (docs/38 section 7); its 195-page argument has been reviewed by no person

rested on: the verified interval cover that turns the bound into the table D(h) (dtable.json) has no gap, so h(D) <= h forces |D| <= D(h)

no adversarial pass recorded. This claim is open, not confirmed

qrh-nonresidue-log8

given OpenAI's Theorem 1.1 (no Dirichlet L-function vanishes in Re s > 7/8), for every q >= 3 and every nonprincipal Dirichlet character chi mod q the least n with chi(n) not in {0, 1} is at most (log q)^8, and at most (0.7 log q)^8 for q >= 5; hence the least quadratic nonresidue mod every odd prime p is at most (log p)^8, and every odd composite n has a Miller-Rabin (strong) witness at most (0.7 log n)^8 (hunt #125, hunts/qrh_nonresidue/, PR #278, landed 2026-10-08). Grade: candidate, pending external review: an ordinary written proof that no person has reviewed, enclosure-carrying numerics, on an input whose argument no person has reviewed

claimed by hunt #125 session (qrh_nonresidue, branch hunt/qrh-nonresidue, 2026-10-08). a smoothed explicit formula with weight (n/x)^(1/4) log(x/n), the zero sum bounded through the Hadamard identity, so the exponent 1/(1 - 7/8) = 8 comes with constant 1 for every q >= 3; the exponent itself is classical (Rodosskii; Montgomery-Vaughan 13.12), the explicit constant and the all-moduli statement were not found in the search

rested on: OpenAI, 'The Quasi-Riemann Hypothesis' (preprint dated 2026-09-30), Theorem 1.1: zeta and every Dirichlet L-function have no zero with Re s > 7/8. Its Lean statements were rebuilt here and accepted by Lean's kernel and the independent NanoDa kernel (docs/38 section 7); its 195-page argument has been reviewed by no person

rested on: the functional equation and the Hadamard identity at sigma0 = 2 theta + c price the sum over zeros with no zero counting; no zero location beyond the half-plane is used

no adversarial pass recorded. This claim is open, not confirmed

qrh-ninth-powers

given OpenAI's Theorem 1.1 for zeta (zeta has no zero with Re s > 7/8), for every integer n >= 1 there is a prime p with n^9 < p < (n+1)^9; with it, a prime in (x, x + (1/2) x^(7/8) log x] for every real x >= e^8, and |psi(x) - x| < x^(7/8) (log x)^2 / (128 pi) for x >= e^10 (hunt #126, hunts/qrh_prime_powers/, PR #276, landed 2026-10-08). Grade: candidate, pending external review: ordinary written proofs that no person has reviewed, every numerical inequality decided in Arb (enclosure-carrying), small cases by Pratt certificates, on an input whose argument no person has reviewed

claimed by hunt #126 session (qrh_prime_powers, branch hunt/qrh-prime-powers, 2026-10-08). the exact explicit formula for a quadratic B-spline weight, sums over zeros bounded in closed form through explicit N(T), an Arb cover of 10 <= n <= e^100, an analytic tail and Pratt certificates for n <= 9; the gap (n+1)^k - n^k, about k x^(1 - 1/k), beats an error of size x^(7/8) (log x)^2 exactly when k >= 9, and without further input the chain fails at k = 8; qrh-seventh-powers inherits this weight, formula and base routine, so a defect found here bears on both

rested on: OpenAI, 'The Quasi-Riemann Hypothesis' (preprint dated 2026-09-30), Theorem 1.1: zeta and every Dirichlet L-function have no zero with Re s > 7/8. Its Lean statements were rebuilt here and accepted by Lean's kernel and the independent NanoDa kernel (docs/38 section 7); its 195-page argument has been reviewed by no person

rested on: the explicit zero-counting bounds cited in RESULTS.md section 1; the verified RH height only widens margins (k = 9 also closes with none)

no adversarial pass recorded. This claim is open, not confirmed

qrh-seventh-powers

given QRH(7/8) for zeta (no nontrivial zero of zeta has real part above 7/8, the zeta part of OpenAI's Theorem 1.1) and Kadiri, Lumley and Ng's explicit zero-density rows (arXiv:2101.12263v1, Lemma 4.14 and Table 1), every integer n >= 1 has a prime strictly between n^7 and (n+1)^7; an eighth-power version on the same route is its audited predecessor (hunts/oct08_extensions/, PR #282, landed 2026-10-08). Grade: written conditional candidate: a written proof with every numerical step enclosure-carrying; an independent written audit by a separate agent context, of the author's model family, passed; reviewed by no person; not formalized in Lean; no worldwide priority claimed

claimed by oct08_extensions producer (Codex root; route prime_gap_density, 2026-10-08). bound x^(beta - 1) pointwise by x^(s0 - 1) plus positive increments times the indicators beta > s_j over the strips 3/4 < 0.8 < 0.85 < 0.86 < 0.87 < 7/8, so cumulative density upper bounds substitute without subtracting independently bounded counts; for log x >= 8 each increment decreases in x, so a cell takes the increments at its left end and the zero sums at its right; a single split at 0.85 already closes k = 8, and resolving the strips closes k = 7

rested on: OpenAI, 'The Quasi-Riemann Hypothesis' (preprint dated 2026-09-30), Theorem 1.1: zeta and every Dirichlet L-function have no zero with Re s > 7/8. Its Lean statements were rebuilt here and accepted by Lean's kernel and the independent NanoDa kernel (docs/38 section 7); its 195-page argument has been reviewed by no person

rested on: KLN's rows at sigma = 0.75, 0.8, 0.85, 0.86 and 0.87 hold as printed (rounded upward in layers.py); their constant calculations are accepted, not recomputed, and their critical-line input rests on Hiary, Patel and Yang plus a new Acb low-height check (audits/kln-restoration/)

no adversarial pass recorded. This claim is open, not confirmed

oob-envelope-L1.19

for every real even f with supp f in [-1.19, 1.19] (support 2.38), Weil's form on the window satisfies Q(f) >= 5.7178e-48 ||f||^2; the route is the out-of-band envelope lemma: a correction to the Weil symbol at frequencies of size at least 2L leaves the form unchanged on the window, so the envelope constant in arXiv:2608.24827's one-stroke reduction can drop from sup P_L to sup (P_L - H) (hunts/oob_envelope/, PR #258, landed 2026-09-28). Grade: candidate, hardened by two independent implementations (sharing python-flint), resting on an ordinary derivation that passed the hunt's referee lane; even sector only; not kernel-checked; pending external verification

claimed by oob_envelope numerics and theory lanes (2026-09-27/28). |F|^2 is the Fourier transform of f * f~, supported in [-2L, 2L], so a bounded almost-periodic H whose frequencies all have size at least 2L integrates to zero against it; per prime the best out-of-band correction is a Caratheodory-Toeplitz problem, realised within a Fejer loss by a nonnegative kernel sum; with H = sine:16 the envelope constant at L = 1.19 falls from A_L = 7.0750 to 3.8634773 (envelope.json), which brings the matrix to N = 500 even Legendre modes

rested on: Q >= R_H, the modified reduction (theory lane): an ordinary derivation, referee PASS with stated scope, reviewed at L = 4/5 and independent of L

rested on: Zhu's two-block bound (13) and the reduction of arXiv:2608.24827 as transcribed, with the tail terms eps_D and eps_B enclosed

no adversarial pass recorded. This claim is open, not confirmed

four-point-0.6728604

for every eps > 0 and all sufficiently large T, the number of simple zeros of zeta on the critical line with ordinate in (T, 2T] is at least ((14400000 H - 17240)/14366681 - eps) times the number of nontrivial zeros there, counted with multiplicity, where H = 3/2 - cot(1/sqrt 2)/sqrt 2; the coefficient is about 0.6728603588, from four-point pressure parameters (n, c, m, p) = (4, 2330/10^6, 432, 2500) (hunts/four_point_pressure/, PR #259, landed 2026-09-28). Grade: kernel-checked at the pinned revision 5522b963 by the laboratory's own build, pending external verification, not registered with Palomar

claimed by four_point_pressure sessions (candidate d28df5f9, 2026-09-05; Hermes repair and lab build at 5522b963, 2026-09-28). substituting c = 2330/10^6, m = 432, p = 2500 into the existing n-point bridge gives the coefficient (14400000 H - 17240)/14366681 exactly; the finite certificate is a generated tree of interval cell lemmas proved inside Lean, so the theorem carries no certificate hypothesis; the parameter floor was already tabulated in hunts/ainta_seven_point/FOUR-POINT.md, so the parameters are not a discovery

rested on: the Lean statements say what the claim says: Mathlib's riemannZeta, multiplicity as analytic order, ordinates in (T, 2T] (hunts/ainta_seven_point/lean-four-point/StrongerChallenge.lean)

rested on: the build record at 5522b963 is what it reports: one build on the laboratory's own Modal compute at Lean 4.33.0-rc2, not an outside rebuild

no adversarial pass recorded. This claim is open, not confirmed

davenport-heilbronn-rung3

davenport_heilbronn_strip: some entire function with the Davenport-Heilbronn Dirichlet series and functional equation has a zero s with 0 < Re s < 1 and Re s != 1/2 (the witness is DH; it bundles dh_analytic_half and dh_zero_located; PR #353); dh_separation_hundred: paired with hunt #137, below height 100 the Davenport-Heilbronn function DH has a zero s with 0 < Re s < 1, 0 < Im s <= 100 and Re s != 1/2, and every zero of Mathlib's riemannZeta there has Re = 1/2; dh_zero_located: a zero of DH lies in the closed square of half-width 3/64 about 808517/10^6 + (21424837/250000) i; read with dh_analytic_half (lean/ZetaLean/DHAnalytic.lean), which makes DH entire with the DH Dirichlet series for Re s > 1 and its functional equation (hunt #145, hunts/rung3_ball_production/, PR #353, 2026-10-26). The assembly's theorem davenport_heilbronn : davenport_heilbronn_statement (lean/ZetaLean/DavenportHeilbronn.lean, line 129) is not part of the claim: the statement, as defined, is also met by the trivial zero s = -1 (lean/ZetaLean/DHTrivialZero.lean). Grade: kernel-checked at Lean v4.35.0-rc2 against Mathlib 065356127b1d, zero sorry, only propext, Classical.choice and Quot.sound, pending external verification

claimed by hunt #145 session (rung3_ball_production, branch hunt/rung3-ball-production, 2026-10-26). 215 site theorems (110 big boxes bounding ||DH|| <= 2.5499 on the big square's edges, 104 grid points bounding ||DH|| from below, the centre bounding it above) combine through norm_deriv_DH_le and DH_lower_on_hcell/vcell into the minimum-modulus square criterion of DHZeroCriterion.lean (restated in Support.lean); the zero is Spira's (1994), and the delta is its enclosure by the kernel

rested on: the 215 site oleans are what GitHub Actions run 40353536947 produced from scripts/60 --tower whole at 85cabd55b: each zip's SHA-256 equals GitHub's digest, and the pilot site's regenerated sources hash as its checkpoints record; the assembly imports them without re-checking their proofs. On 2026-10-27 a same-kernel fresh replay (leanchecker --fresh Rung3Assembly.Final, Lean's own kernel, which its docstring calls 'not an external verifier') re-checked the assembled closure's constants and accepted. The same day a second kernel, con-ron --verified, accepted the closure on a site-wise split with coverage shown (door 1 Stage B): its top shard checks the 18 final declarations abstracted over the 435 site theorems the assembly names (Rung3Glue.*, built by lean/ExportShard.lean and checked by Lean's kernel first), and the join of the 216 shards rests on kernel hashes of every exported declaration (shard_manifest.py), not on a single run

rested on: the separation's LEAN_PATH joins hunt #137's oleans with this tree's through one ZetaLean overlay; the shared modules' constants are identical by CompareOleans.lean, not by byte equality

no adversarial pass recorded. This claim is open, not confirmed

blockpos 0.672529 (and siblings 0.6725124, 0.6725318)

the construction used u u* where the pinned upstream zero side uses u u^T; an off-line pair is the hyperbolic block 2m(xx^T - yy^T), whose interaction with the on-line part can be negative, and the proposed final additive inequality reads 9 >= 13

conditional 0.6728294 (the bin artifact)

midpoint bin-to-cell assignment inflated chain counts, briefly producing a conditional bound past CG 1993

naive prime-by-prime (placewise) positivity

individual place contributions can sometimes be represented as norms, but the local pieces do not consistently carry the sign naive global assembly needs