Project

Sources

• A362583 Irrationality — informal proof blueprint
  AuthorsEric Vergo

  Idself-authored informal proof blueprint for this project; realized as the browsable blueprint site generated from this repository

  Typespecification / informal blueprint

  LicenseApache-2.0

  Author contactedn/a
• OEIS A362583 — Concatenation of ((p mod 4) - 1)/2 for primes 3..prime(n), read as binary
  AuthorsEric Vergo

  Idhttps://oeis.org/A362583

  TypeOEIS entry (integer sequence: successive binary-integer digit prefixes; a(35) = 12032782746 used as a numeric cross-pin)

  LicenseCC BY-NC 4.0 (OEIS)

  Author contactedn/a

Status

Complete. The prime race constant ϱ = Σ_{k≥0} b_k·2^{-(k+1)} — the number whose binary expansion is 0.b0b1b2..._2, with b_k = 1 iff the k-th odd prime is ≡ 3 mod 4 — is irrational, via a non-degeneracy theorem for the mod-4 Chebyshev prime race: the race sum is never c·π(N) + O(1). The analytic input is only the continued L(s, χ₄), L(1, χ₄) ≠ 0, the Euler product, the divergence of Σ 1/p, and the identity theorem — no PNT, no PNT in APs, no zero-free regions, no quantitative oscillation (Littlewood/Shiu avoided by design).

Main results

• A362583.irrational_ϱ
  FileA362583/Main.lean

  Comparator configcomparator/comparator.json

  Literature dependenciesnone
  0 sorriesaxioms: standard 3
• A362583.raceSum_not_linear
  FileA362583/CaseZero.lean

  Literature dependenciesnone
  0 sorriesaxioms: standard 3

Automation

• agent
  FrameworkClaude Code

  Modelsclaude-fable-5

  Wall time~1 day (2026-07-03)

  Spendsubscription-based usage

  HardwareAPI-only; local builds on a MacBook (24 GB RAM), warm Mathlib cache

  Tool setupA main-session orchestrator spawning specialized subagents per phase: (0) two firewalled agents independently re-derived the analytic core from the theorem statement alone, then an adversarial referee checked both against the specification before any code; a parallel dependency fan-out verified every Mathlib dependency with compiling minimal working examples; (1) author + independent reviewer produced the frozen statement set; (2-4) one agent per proof layer, each owning a single file, checked via lake env lean against a shared warm build, merged and committed centrally by the orchestrator; (5) two independent auditor agents re-verified the acceptance criteria (including a mechanical diff of all locked statements against the frozen set) and the informal-to-formal correspondence, with adversarial spot-checks. Accumulated Mathlib-pin gotchas were fed forward into every subsequent agent prompt.

  Prompting notesSpecification-first workflow: a detailed human-authored specification with two blocking human sign-off gates (Phase-0 audit/re-derivation exit; Phase-1 statement lock). Statements were frozen before any proof work; proof agents received the informal blueprint, a verified table of Mathlib dependencies, compiling usage examples, and hard guardrails (no PNT-strength imports, no axiom patches, no statement changes without a lock-break escalation).

Fidelity

Statements were frozen before any proof work and are byte-identical to that frozen set. Proof-route deviations from the informal argument: the k=1 layer's analytic continuation is *defined* as the discrete by-parts series rather than continued after the fact; the Euler-sum split uses a per-prime identity instead of a double-sum rearrangement; in both cases (c ≠ 0 and c = 0) the contradiction is evaluated at a single explicit point instead of via limits (one plain one-sided limit remains, pinning L(1) real-positive); constants are deliberately generous rather than sharp.

Alignment

Acknowledgements

Built on mathlib4 (pinned v4.32.0). The proof route is only feasible because mathlib already contains the analytically continued Dirichlet L-function, its nonvanishing at s = 1, the exponential form of the Euler product, the divergence of the sum of prime reciprocals, and the identity theorem.