Referee report: The Quasi-Riemann Hypothesis

Review date: 9 October 2026. Primary manuscript: The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s) > 7/8, dated 30 September 2026, 199 pages.

Assessment

This audit does not establish the claimed theorem, and it has not identified a verified fatal mathematical error. The appropriate disposition is to keep the claim under technical review. The unresolved work is concentrated in the two moment reductions and their arithmetic closure, rather than in the final numerical optimization. This is an incomplete correctness assessment, not a conclusion that the theorem is false or that the manuscript must be rejected.

The manuscript claims a common zero-free half-plane for all finite-order Hecke L-functions over Q(sqrt(-3)) and, by quadratic transfer, all Dirichlet L-functions. Its statement concerns the open region Re(s) > 7/8 and excludes a principal pole at one; it does not claim the Riemann hypothesis or nonvanishing on the boundary. The proof first obtains 11/12 using a completed cubic-theta probe and then strengthens that boundary using compensated probes and marked inverse and fourth moments. The analytic continuation criterion requires a common positive saving, but permits constants, a fixed deleted Euler set, and the sufficiently large scale threshold to depend on the target character.

Several vulnerable-looking steps survive focused checking: the theta input does not impose an omitted coprimality condition; differentiation removes its constant terms before reflection; the local correction cancels the dangerous denominator on contours with negative Re(w); the displayed width transitions have the right signs; and the centered lattice main terms really cancel under the common-coefficient hypotheses. These are positive findings about particular proof components, not substitutes for verifying the entire 199-page dependency chain.

Scope and pinned provenance

The primary repository snapshot is openai/math at commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. The primary PDF SHA256 is 8fe93046f8cf5ef1ba5969c89addc02d76311adc4ee907509ff9cd96f7ec99e7; the TeX SHA256 is 42a5ee0febca59fd1def55cfd6c6808c322ef4237d7726303ea52f711deac6a3. The PDF metadata records 6 October 2026 creation/modification, so the date in the directory name alone is insufficient provenance. The source manifest and evidence dossier are under quasi-riemann-2026-10-09.

The independent focused examination covers Proposition 5.1 and its native theta source; the displayed local scalar and Euler-correction calculations in §7.2; the abstract finite-seminorm propagation rule in §17; the canonical width and margin transitions in §17.5; and the width, exceptional-character, and centered lattice calculations in §18. Two full-text model reviews were adjudicated against those checks, followed by complementary source-only adversarial packets sent to Anthropic, Google, xAI and Alibaba. Completed and incomplete attempts are distinguished below. The evidence dossier additionally supplies checked continuation and transfer arguments, a finite numerical scalar test, and an exact endpoint algebra check. Those checks are identified separately below.

The October 5 manuscript asserting 11/12 and the Landau–Siegel companion are distinct artifacts. Their complete proofs are outside this report. The Lean material is discussed as verification evidence with explicit limits; no Lean compilation or comparator run was performed for this report. No novelty or priority judgment is made.

Reading and dependency roadmap

The interactive roadmap and annotated reading guide provide the gist of the overall argument and individual claim arguments, their internal prerequisites, and the external references used or explicitly excluded. The export indexes all 67 numbered claims, 20 sections, and 28 bibliography entries, with 81 source-grounded relations. Edges point from prerequisite to consumer. The annotations attribute proposed inferences to the manuscript; they do not certify them or turn a candidate reference into a checked external input.

A compact reading order is:

1. §§1–2: continuation. A common power saving would continue each reciprocal L-function across the family zero supremum.
2. §§3–6: base reflection. Complete a cubic-theta probe and derive its low bound from reflection.
3. §§7–11: first high bound. Poisson-expand that same probe, isolate its principal reciprocal signal, bound other rows, and close 11/12.
4. §§12–16: compensation. Insert independent prime slots and asymmetric scales, with a new reflected low bound and local correction.
5. §17: marked inverse moment. Use two masked Poisson transforms, canonical child data, decreasing width, and amplification.
6. §18: plain fourth moment. Decrease effective width while centering equal-product rectangles so their inducing-character main terms cancel.
7. §19: refined row counts. Combine the two witnesses with slot capacity and prime supply.
8. §20: final closure. Balance complementary counts, reserve losses, verify the endpoint margin, and apply continuation and quadratic transfer.

For further inspection or reuse, the same roadmap is available as structured JSON, Mermaid, and Graphviz DOT. The source SHA256 and source-line anchors are retained. Of its 81 relations, 61 are annotated proof inputs, 18 background references, and two explicitly excluded inputs; annotations and candidate references remain distinct.

Concrete findings

1. Native theta source: the support and normalization match

I inspected Dunn–Radziwiłł, arXiv:2109.07463v3, §5, equations (5.4), (5.7)–(5.8), (5.13)–(5.16), and Appendix A, rows 1, 10, and 19. Their coefficient domain requires a squarefree primary first factor and a primary second factor; it does not require those factors to be coprime. The manuscript therefore does not manufacture support at shared primes when it uses n b³. The three cusp representatives and stated coefficient magnitudes match those source formulas. I visually checked the conjugation bars in (5.7): conjugating theta produces the unbarred normalized cubic Gauss sum used in the manuscript's infinity coefficient. These source identities are unconditional; the source's GRH-dependent prime asymptotic is a different result. Native source.

Annotation at Proposition 5.1: The paper masks the whole completed index before converting cubic notation to sextic notation, and leaves the dual cusp coefficient functions unmasked. For exponent zero, the local factor is still the principal character extended by zero. Finite Fourier inversion therefore includes both its zero-frequency factor 1−1/q and its nonzero-frequency factor −1/q. Treating that exponent as the constant function one would invalidate the reflection, but that is not what the displayed argument does.

The derivative ∂/∂bar(z) removes the z-independent constant term from each cusp expansion. The proposed entire continuation of the differentiated Mellin transform therefore does not fail merely because the undifferentiated theta series has a constant term. The reflection's later norm estimate and all moving-prime phase separations have not been independently reproduced in full.

2. Local Euler correction: the apparent contour singularity is canceled

Annotation at Lemma 7.1: With V=q^(−6z), W=chi_p(u)q^(−w), D=eta(p)conj(chi_p(u))q^(−x), and E_p=P_p*+D, the displayed identity is

H_p−1 = [D(V+W−VW)−VW+(1−V)(1−W)E_p]/(1−D).

It contains no denominator 1−W. Thus negative Re(w) in the first Euler region is not itself a singularity of the correction. The stated good-prime bounds are arithmetically consistent: in the first region the R-term starts at exponent at most −11/10, and the two possible negative-w factors leave at most −27/25; the DW-term is bounded by q^(−1−epsilon_0). In the second region the closest displayed good-prime exponent is 1−x_r−w_r−6z_r = −363/200 at its lower endpoints. The ramified leading exponent is 1−x_r−w_r ≤ −33/40. These estimates give normal convergence and a subpower ramified product, conditional on the stated local factorization and phase cancellation.

The dossier's scalar script checked 238 combinations at split degree-one primes 7, 13, and 19, including principal powers and nonunit zeros, with maximum floating-point discrepancy below 9.3×10^−13. That is useful evidence for the finite scalar table. It is not an exact proof, an inert-prime test, or a check of the Chinese remainder phases and global quadratic-refinement cancellation. Those are separate obligations.

A second finite calculation compared the individual summands of the full local family table with its ten stated rows: 25,920 cases at the same three primes, two family depths, all six valuations and residue phases, and two target unit phases passed, with maximum absolute discrepancy 3.99×10^−16. It used x=1.17+0.13i, w=1.21+0.17i, z=0.47+0.09i and the prime-power lift formula; the Gauss phase alpha was derived from the local Gauss identity. This checks the table algebra under that identity, not the independent identification of alpha with an Eisenstein prime generator or the global phases. The reproducible script and result are verify_local_family.py and local_family_check.json in the run directory.

3. The abstract analytic propagation is valid under its hypotheses

Annotation at §17, finite-seminorm propagation: Backward induction on a finite acyclic graph correctly converts child seminorm and height bounds into fixed parent orders. In the product version, powers of Z add with the Cauchy–Schwarz weights, whereas seminorm and height orders add separately. The indexed corollary correctly allows a Z-dependent discrete family if its normalized coefficient measure has a fixed mass exponent independent of the requested Fourier moment.

This is a valid conditional bookkeeping lemma. It does not prove that the concrete arithmetic transforms satisfy its hypotheses. A failure would have to occur in a transformed profile, a purported common coefficient measure, an exponent defect, or the finite-depth claim—not simply in the observation that high derivative orders are needed.

4. The displayed inverse-moment transitions preserve both margins

Annotation at §17.5, canonical transition: The identities

F_c = F−D_c−2ell+j, M_c = M−2D_c−2ell+j

give F_c−M_c = F−M+D_c and 4F_c−3M_c = 4F−3M+2(A_i+t+g−theta+V)+j exactly. Together with the stated puncture bound Q_new ≤ Q+D_c+4eta, the declared shifts F_ch=F_c+delta_N, M_ch=M_c+eta preserve the first margin with loss at most 5eta and the second with loss at most 7eta.

The row decrease also checks: from D_c ≥ ell+V−2eta and j ≤ 2ell+3eta, one gets

M−M_ch ≥ 2(ell+V)−8eta ≥ 2d−8eta.

For eta ≤ d/16 this is at least 3d/2, exceeding the required decrease d. A fixed depth then suffices. This validates the displayed exponent ledger conditional on the construction of those child data and their actual support bounds. It does not independently verify the two Poisson identities, reconstruction multiplicities, or all character masks used to obtain those data.

I also recomputed all eight local first-Poisson exponent patterns: 4a_i + 1_(t≠0)(1±t) + pi(a_1+a_2) modulo six, with t=a_1−a_2+3pi. Both sides agree with the stated zero/four table in every case. Its fourth-power support is exactly the odd part s together with the even-part intersection J_2; other cube primes contribute a puncture. This supports the retained-cube-label identity at that finite local step. It leaves the full Gauss/ray phases, Poisson normalizations, and second transform unverified.

5. Centered exceptional terms: the claimed cancellation has a real mechanism

Annotation at §18, masked rectangle cancellation: For a fixed finite-ray character, annular smooth profile, and polynomial-size squarefree mask, two-dimensional Poisson summation gives a main term c X^(1+it) I(t) with a fixed polynomial height error. Inclusion–exclusion inserts the mask with coefficient c sum_{d|R} mu(d)theta(d)/q_d; extraction cancels q_d^(it), so that coefficient is independent of both scale and height. The divisor count costs an arbitrarily small power of Z. If the two rectangles have equal products of scales and retain the same character, mask, and norm power, their product main terms agree and cancel.

The ensuing estimate with minimum scale at least Z^r has the claimed saving Z^(−r); the all-scale absolute-volume fallback is also consistent. Thus this lemma is not an unexplained invocation of cancellation. Its application depends critically on the common-coefficient invariant through the complete-support extraction and full Möbius allocation. I inspected that invariant's formulation and allocation identities, but did not verify every preceding local correlation identity and amplifier error.

The exceptional-row count has the right necessary valuation condition: at an extracted prime of equal multiplicity one, the frozen row contributes valuation two, so an inducing character unramified there requires v_p(h') ≡ 4 mod 6. Writing h'=h_0 v^6 yields the forced norm saving used in the count. The count is conditional on the claimed disjointness of the genuine extracted support from previous moving support; replacing a row scalar by an absolute upper bound earlier would require a different argument.

The width statement M'=M+J−g−g_2+t_2 ≤ M−sigma is consistent with g−J ≥ sigma and g_2 ≥ t_2. The actual enclosing width is at most a fixed C_*xi larger, so choosing C_*xi < sigma/2 gives a strict decrease and excludes a same-band recursive cycle under the stated call order. Constants and thresholds may depend on the fixed slot count; the manuscript explicitly aggregates its support errors as H_N/log Z before choosing the final threshold. No contradiction in that quantifier order was found.

6. Final bridges and numerical certificate

The evidence dossier checks Proposition 2.1's continuation bridge without assuming that the global supremum of zero real parts is attained. It also checks the split/inert Euler-factor transfer in Proposition 11.3 and its separate treatment of the principal pole at one. Those are conditional bridges, not independent evidence for the moment bounds.

The endpoint certificate in §20 checks algebraically: SymPy gives an identically zero difference between the stated quadratic expression and its completed-square form, and 49/440640 > 1/10000 holds exactly. The displayed interval inequalities are consistent. This resolves the final optimization algebra conditional on the row exponent formula; it cannot certify the analytic inequalities entering that formula.

Ranked unresolved obligations

These are unresolved verification tasks, not asserted counterexamples. A mathematical rejection would require an explicit invalid implication, a counterexample to an estimate under its stated hypotheses, a circular dependency, or a demonstrably missing essential assumption. None has been established in this report.

What the Lean claims establish here

The repository's lean/docs/003.md claims formalization of the 7/8 zeta, Dirichlet, and Hecke statements and a uniform real-zero gap. The main theorem file calls assembly proofs and uses Mathlib's root Dirichlet L-function with a positive modulus and principal-pole exclusion. The inspected endpoint/assembly files contain ordinary proof terms.

The research pass fetched the complete static OAI import closure from Nonvanishing.lean and Foundation.lean: 2,924 modules, 25,009,201 source bytes, and zero fetch failures. It also reconstructed 19 imported external-package modules from pinned upstream versions and repository patches, checking every patch context/removal with zero reconstruction errors. Comment/string-aware scans found no code-level sorry, admit, axiom, unsafe, implemented_by, extern, native_decide, native_omega, run_cmd, or initialization/elaboration-hook token in that scoped set. This is substantial evidence against those visible admission mechanisms on the examined paths. It remains a textual scan rather than elaboration, semantic dependency verification, or an axiom report from Lean.

The static definition audit found no local redefinition of riemannZeta or root DirichletCharacter.LFunction. The namespaced Hecke-family LFunction is a separate construction, with a stated equality to its ideal series for Re(s)>1. Mathlib is pinned to the official commit d13f23b723b8a846827a245b89c10fc7d3f11612; no Mathlib patch or shadow target definition was found. The 19 external modules comprise four from PrimeNumberTheoremAnd and fifteen from RellichKondrachov; their reconstructed imported paths have no visible admissions or target substitutions. Unrelated additions elsewhere in the large patches and the entire transitive stock-Mathlib graph were not audited. The detailed evidence and limitations are recorded in lean-dependency-audit.md within the run directory.

The sorry in the comparator's challenge theorem is the target statement the solution must match. Its presence is not a discovered gap in the solution. The comparator configuration names the solution module and permits propext, Quot.sound, and Classical.choice, excluding sorryAx. Whether its entire solution closure compiles and matches the mathematical statement remains untested here. This report does not certify the Hecke definitions or transitive analytic inputs.

At the original review, the required toolchain was Lean 4.34.1 and the available local toolchain was 4.34.0. Comparator, landrun, and lean4export were absent. The configuration's automatic clone/patch hooks were read but not executed. No target build, #print axioms, or strict comparator run was performed for the paper. The static scan cannot be represented as a successful Lean verification.

Environment update, 2026-10-13: Lean 4.34.1 is now installed and the default. Compiler and Lake version checks passed, including toolchain selection in the paper's pinned source directory, and a separate core-Lean smoke proof compiled without axioms. This resolves the version mismatch. The paper itself has not yet been built or checked with the strict comparator; Comparator, landrun, and lean4export remain absent from PATH. Installation and smoke-check evidence.

A decisive follow-up should run lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json on the pinned repository after its documented setup, and likewise check the corresponding Dirichlet and Hecke comparators. Record the exact toolchain, dependency revisions, exit statuses, theorem matching and used axioms. Formal verification of the statement and verification that it represents the intended analytic L-functions are both relevant.

Full-text model review and adjudication

GPT-6.1 Sol at high reasoning reviewed the complete 766,316-character TeX source in 459.8 seconds. Its structured output identifies 67 elements, including two definitions and one remark; 64 are proof-bearing statements. It labels 56 elements valid and 11 unverifiable, and gives an overall model assessment score of 60/100. That score is not a probability that the theorem is true, a calibrated correctness measure, or an independent proof. Many of its valid labels explicitly mean valid conditional on earlier inputs.

The Sol result demonstrates no counterexample and identifies no particular false local factor. Its three main verification bottlenecks are Proposition 5.1's exact theta reflection; Lemma 17.2's arithmetic parent-to-child connection; and Lemmas 18.1–18.2's common centered coefficient through every transform and amplifier branch. These are consistent with the focused audit's remaining obligations.

One part of its uncertainty has been resolved by direct source inspection: the imported cusp coefficient support, magnitudes, and infinity conjugation convention do match Dunn–Radziwiłł. This removes that specific lack-of-source-check objection; it does not certify all cusp multipliers, moving-prime phases, or reflected energies. For Lemma 17.2, the precise identities still requiring reproduction are eq:first-poisson-column, eq:inverse-second-formal-component, eq:inverse-second-extraction, and eq:inverse-xi-identity. For §18 they begin with eq:first-poisson-bridge and must reach the independently allocated children with the common-coefficient invariant intact. The checked exponent ledgers and local cancellation cannot replace those identities.

The Sol assessment is preserved as sol-high/referee_uploaded_20261009_184532.json within the run directory. Its main finding is inability to close verification, rather than a mathematical disproof. This report consequently does not convert its unverifiable labels into claims that the corresponding lemmas are incorrect.

GPT-6 Astra at max reasoning completed a validated full-text JSON review in 2,862.7 seconds (47.7 minutes). It reviewed the same complete TeX source, counting the 64 proof-bearing statements and excluding the two definitions and remark. It labels 46 statements valid and 18 unverifiable, with a model assessment score of 58/100. The structured assessment and saved raw response are astra-max-json/referee_uploaded_20261009_190228.json and the corresponding .raw.txt file. Neither reviewer reports a demonstrated counterexample or a specific mathematical error classified as a major or minor defect.

These are observed workflow latencies, not a controlled model-speed benchmark. Sol used unconstrained output and the successful Astra rerun used JSON mode; possible SDK/output-budget retries were not instrumented. The timings therefore do not establish a model-speed ratio.

The counts reflect how the reviewers propagate unverified dependencies: Astra marks several downstream reflected-energy and low-estimate deductions unverifiable where Sol accepts the conditional deduction. They do not constitute independently established errors. Neither score is calibrated, and averaging them would not give a probability of correctness.

Astra independently identifies the same central gates. Its exact §17 concerns are the complete outer coefficient in eq:inverse-first-separated, the child-data independence needed for eq:inverse-xi-identity, and eq:canonical-child-polynomial. In §18 it specifically leaves the common character/puncture/norm power unverified through the valuation-1, 6, and 7 amplifier errors, the artificial off-coprime extensions, and the support budget old-eq:2.13. Its reasoning agrees that the displayed width, margin, finite-depth, and cancellation ledgers are coherent conditional on the exact transformations. These concerns refine the ranked verification tasks above; they provide no invalid step to reject.

Astra's Proposition 5.1 objection is a lack of independent confirmation of the imported cusp coefficients, infinity normalization, and shared-prime support. The direct native-source comparison in finding 1 addresses those specific support, magnitude, and conjugation questions. That objection should therefore not be repeated as evidence that the manuscript used the source incorrectly. All moving-prime multipliers, branch compatibilities, and reflected-energy consequences remain outside the completed source check.

An earlier Astra output file retained only an inner paper_info object because of a parser failure and manufactured a default score of 0/100. That file is a formatting failure, not an Astra mathematical verdict, and is excluded from this report's assessments. The validated rerun used JSON mode and preserved the raw response before parsing. The mathematical assessment above uses the validated rerun only.

Independent adversarial panel

The first phase comprised two full-text OpenAI reviews. The expanded phase uses four additional provider families with complementary source packets, not four new complete 199-page reviews or 67 independent claim reviews per provider. Each independent first pass receives only source evidence and precise error criteria, without Sol/Astra verdicts or another panel member’s findings. The task is to find an explicit invalid implication, missing essential hypothesis, circularity or counterexample under the actual hypotheses. Failure to finish a derivation is recorded separately. No cross-model vote or score average determines this report’s assessment.

The packet manifest records source spans, hashes and intentional exclusions. The reflection packet includes the full Proposition 5.1 argument and native Dunn–Radziwiłł formulas; the §17 and §18 packets each include their entire section and relevant finite-coefficient prerequisites. Some earlier internal proof statements are supplied without their proofs. An unseen prerequisite in one packet is therefore a coverage limit, not evidence that the manuscript omitted it.

Gemini supplies seven short positive checks and no objections. Its numeric equation anchors are unreliable: its claimed priority identities at (17.13)–(17.14) are actually reflected-energy bounds, and its claimed amplification identities at (17.60)–(17.61) are second-Cauchy/fiber-count calculations. The model’s descriptions can correspond to genuine arguments elsewhere in the section; its mismatched anchors and brief summaries do not independently reconstruct the exact masked transforms. This is a source-fidelity limitation of that review, not a mathematical defect in the manuscript.

Grok supplies eight source-anchored positive checks, including prime-power Fourier support, local correlation, the common-prime inequality, width decrease and centered deficits. Its common-prime arithmetic agrees with direct inspection: for i≥j≥1 and r=1 when 6 does not divide i−j, the positive-branch gap is (3i+11j−12−5r)/6, with equality at i=2,j=1. A purported j=0 counterexample would violate the shared-support hypotheses. Grok explicitly leaves five prerequisite/citation obligations unverified: functional-equation growth, fixed-numerator ray reduction, uniform kernel bounds, fixed-extension prime supply, and the earlier reciprocity-table proof. These are not claimed counterexamples; several proofs were deliberately outside its packet. Its summaries do not reconstruct every amplifier and artificially extended coefficient.

Fable’s completed reflection result examines the zero-extended exponent-zero Fourier factors, whole-index mask, derivative/chain rule, direct and reflected Mellin normalizations, cusp cases and local Gauss/Ramanujan branches. Its two objections are explicitly unverified steps, not asserted errors. The native coefficient/support/conjugation concern is addressed by direct DR source comparison, including its unconjugated Kubota character and stated homomorphic extension to Gamma2. Patterson’s underlying theorem proof was not rederived. The missing eq:pointwise-mellin-tail proof is a packet omission: the original source, lines 1164–1177, supplies repeated logarithmic integration by parts. The prescribed decay of V and all its logarithmic derivatives removes the boundary terms on each compact real strip; choosing the order above T’s polynomial strip-growth exponent removes the contour joins. I also independently checked that the displayed Mellin scalar ratio becomes (-i/81)[(2pi)^4/27]^(-t) at s=1/2−t. These resolve particular checks, not every later reflected-energy input.

Fable’s §17 and §18 recovery answers stop inside JSON audit entries at their final budgets. The preserved partial texts contain seven and six complete positive entries respectively, but neither contains a completed assessment or objection section. Their local character/exponent ledgers agree with the source checks above; no candidate counterexample appears in the surviving text. They remain incomplete reviews and are not counted as no-error-found verdicts.

Qwen returned no visible assessment before its client workflow was interrupted near its first 30-minute SDK deadline. The execution exited 130. This is a client cutoff, not a native provider timeout or a mathematical verdict. OpenAI SDK 2.31.0 defaults to two retries and the Alibaba adapter did not override that setting; the actual native retry count and server completion/billing outcome are unknown. No additional Qwen run was launched.

The source adjudication notes retain the distinction between a model’s claim and an independently checked fact. The final campaign manifest records seven closed jobs: three validated targeted reviews, three Fable budget failures (combined packet and the §17/§18 splits), and one Qwen client cutoff. These correspond to four additional provider families attempted, with completed assessments from three of them. No new panel result claims a demonstrated error, and the independent source adjudication establishes none. The ranked mathematical obligations above remain open. More no-error-found responses cannot close them by agreement alone.

Recorded attempts and resource limits

Every job preserves its exact invocation, system/user prompts, source/prompt hashes, requested model/effort, timestamps, validated result or complete error log. Fable, Gemini and Grok wire payloads and raw native responses are captured before adapter/schema processing, including request IDs and available usage. Completed visible answers are also saved before review-schema parsing. The initial Qwen job used a dedicated Alibaba Maas hostname omitted from the initial trace allowlist: its full invocation and prompt are saved and the first logical request is explicitly reconstructed, but original wire bytes, native usage and internal retry counts for that job are unavailable. The corrected runner covers that hostname for subsequent requests.

The first combined Fable request used 230,629 input tokens per attempt, substantially more than a character-count estimate. Its initial 32,768 and automatic 65,536 shared output budgets were entirely thinking, yielding no visible review and an explicit truncation failure after 1,020.2 seconds. Both attempts are preserved and excluded from mathematical verdicts. Recovery split the same source evidence into three independent, bounded high-effort checks; these are one provider’s coverage, not three votes. The split input counts were 60,649 (reflection), 99,597 (§17) and 72,582 (§18) per attempt. Each first attempt exhausted 32,768 tokens entirely in thinking. The successful reflection retry reported 51,526 output tokens, including 44,959 thinking; the failed §17 retry reported 65,536, including 62,303 thinking; the failed §18 retry reported 65,536, including 63,472 thinking. All reported zero cache hits. Failed first attempts provide empty readable thinking strings and opaque signatures, so no readable candidate argument is available to adjudicate. Visible partial answers are saved separately without completing their JSON or supplying a default verdict. No further Fable recovery followed these outcomes.

Google’s completed request reports 64,847 prompt, 22,591 thinking and 700 visible tokens; xAI reports 47,781 prompt, 61,312 reasoning and 1,579 visible tokens (110,672 total). Provider budget and usage definitions differ: xAI’s reasoning tokens are separate from its visible-answer budget. These observed workflow latencies include any recorded retries and are not a controlled provider-speed benchmark. No comparable total dollar cost is established: missing Qwen protocol usage and provider-specific accounting prevent a complete billed-cost reconstruction. The original xAI cost metadata is retained without assuming its conversion to dollars.

Sources

The run's complete source catalogue lists direct pinned URLs for the downloaded OAI closure, relevant patched external modules, and supporting sources. Principal sources inspected or used in this report are:

• Primary PDF, pinned repository commit
• Primary TeX, pinned repository commit
• Dunn–Radziwiłł, Bias in cubic Gauss sums: Patterson's conjecture, arXiv:2109.07463v3
• Repository disclosure and artifact index
• Lean verification disclosure
• Lean main nonvanishing theorems
• Lean final assembly
• Lean certified-band assembly
• Lean certified existence
• Comparator challenge theorem
• Comparator configuration
• Comparator setup and verification instructions
• Official pinned Mathlib zeta definition
• Official pinned Mathlib Dirichlet L-function continuation
• Pinned PrimeNumberTheoremAnd upstream
• Pinned RellichKondrachov upstream