The structural heart of the GP. This axiom captures the constructor itself — the infinite family of point sets whose unit-distance count grows polynomially faster than the conjecture allows. The OpenAI paper''s contribution at this layer is the use of infinite class field towers (a number-theoretic device for producing extensions of ℚ with controlled ramification) and the Golod-Shafarevich theorem (a 1964 result giving a lower bound on the rank of certain cohomology groups, used here to force the tower to be infinite).

**The artifact.** A sandboxed program — Python with a fixed-version interpreter and no network — exposing one entry point: `construct(k: int) -> list[tuple[Fraction, Fraction]]`. Submission includes source, a pinned-dependency lockfile, and a hash of the runtime image. The constructor must be deterministic (same k yields bit-identical output) and run in time polynomial in k, with k₀ + 15 invocations completing under the wall-clock cap.

The submission also declares (a) the exponent δ as a rational number — typically a small fixed quantity like 1/200 or 1/50, whatever the construction achieves — and (b) the offset k₀ from which the inequality is claimed to hold.

**The verifier.** A staged Omenion harness: 1. Spins up the sandboxed runtime from the submitted image hash. 2. For each k ∈ {k₀, k₀+1, ..., k₀+15}, invokes `construct(k)` and captures the rational-coordinate point list P_k. 3. Validates P_k: all entries are exact ℚ², |P_k| matches the constructor''s claimed size schedule (declared as a function in the manifest, e.g. n_k = 2^k or n_k = k³), no duplicates. 4. For each P_k, exact-counts unit-distance pairs via O(|P_k|²) rational arithmetic. 5. Computes the threshold T_k = ⌈|P_k|^(1+δ)⌉ via exact rational exponentiation on rational δ. 6. Passes iff u(P_k) ≥ T_k for every k in the sampled range.

**What this axiom proves, and doesn''t.** Passing AX-00015 establishes the inequality on 16 consecutive empirically-checked values of k. It does not by itself prove the asymptotic claim "for all k ≥ k₀." The asymptotic is the job of AX-00016 — the Lean proof. AX-00015 is the empirical reproduction harness; AX-00016 is the mathematical certificate; together they close the loop. Splitting them lets a solver claim the empirical bounty (this one) without yet having a formal proof, and lets a Lean-fluent prover claim the formal bounty against an already-verified constructor.

**Sandbox.** Standard Omenion benchmark sandbox: gVisor + read-only filesystem, no network, 32 GiB RAM, 1 hour wall-clock per `construct(k)` call. Python 3.12 with `fractions.Fraction` for exact rationals. The constructor may import `sympy`, `numpy` (for integer-only ops), and a pinned `sage`-subset.