The mathematical certificate layer. AX-00015 verifies the inequality at 16 sampled k values; this axiom upgrades that to a universally-quantified statement over all sufficiently large k, formalized in Lean 4 and checked by `lake build`.

**The artifact.** A Lean 4 project (`lakefile.toml` + `lean-toolchain` + source) building against a pinned Mathlib commit. The project must export a theorem of approximately the form:

```lean theorem unit_distance_disproves_erdos : ∃ (δ : ℝ) (k₀ : ℕ), 0 < δ ∧ ∀ k ≥ k₀, Real.toNNReal (unitDistanceCount (construct k)) ≥ (Finset.card (construct k) : ℝ) ^ (1 + δ) := by ... ```

with `construct : ℕ → Finset (ℚ × ℚ)` defined in the project and `unitDistanceCount` defined in terms of pairwise rational distance.

The proof is expected to route through formal versions of the Golod-Shafarevich theorem and the existence of infinite class field towers, both of which exist in current Mathlib or must be ported as part of the submission. (Mathlib contains a partial formalization of class field theory as of late 2025; the gaps must be closed in this submission.)

**The verifier.** Standard Omenion Lean Tier-1: 1. `lake build` runs against the submitted project in a sandbox with the declared toolchain version. 2. Linter rejects any new `axiom` declaration or any `sorry` not present in the pinned Mathlib. 3. The exported theorem''s statement is hashed against the canonical statement above (modulo `α`-equivalence) and rejected if it does not match. 4. The `construct` definition in this Lean project is checked to agree bit-for-bit with AX-00015''s sandboxed constructor on k ∈ {k₀, ..., k₀+15} — i.e., the two `construct`s are the same function, not different functions that happen to share a name.

Step 4 is the load-bearing one: it stops a solver from proving the theorem about a *different* constructor than the one whose empirical witness AX-00015 verifies. The agreement check is a deterministic small-case match, not a deep equivalence — sufficient for Omenion''s correspondence guarantee.

**Why this is a research-grade Lean axiom.** Mathlib''s class field theory is one of the youngest active areas of the library. Golod-Shafarevich is present in some form but not in the shape needed here. A real submission will involve months of formalization work even given a paper-level proof of the construction''s growth rate. The bounty is sized accordingly.

**Eligibility.** Lean 4 only; submissions in Coq or Isabelle will be considered for a future axiom version but not this one. Toolchain must be `lean4@v4.13.0` or later with Mathlib pinned at a commit no older than 2026-04-01.