Paul Erdős posed the unit-distance problem in 1946: given n points in the plane, how many pairs can be at exactly unit distance? Let u(n) denote the maximum over all n-point sets in ℝ². Erdős proved a lower bound of u(n) ≥ n^(1+c/log log n) using a √n × √n integer lattice with overlapping unit-distance pencils. The best-known upper bound, Spencer-Szemerédi-Trotter (1984), is u(n) = O(n^(4/3)). Erdős conjectured that u(n) = n^(1+o(1)) — equivalently, for every fixed δ > 0, there exists n₀(δ) such that u(n) ≤ n^(1+δ) for all n ≥ n₀(δ). The conjecture stood for 80 years and was widely believed to be sharp at the lower bound. In May 2026, an OpenAI general-purpose reasoning model produced an infinite family of point arrangements with u(|C(k)|) ≥ |C(k)|^(1+δ) for a fixed positive δ, drawing on infinite class field towers and the Golod-Shafarevich theorem (1964) to build the construction. The result disproves the conjecture: the unit-distance count grows polynomially faster than n^(1+o(1)) along the family. **Why this GP exists.** The OpenAI result was announced through a paper, not as a machine-checkable artifact. Omenion''s thesis is that the value of a result like this multiplies once the construction is reproducible bit-for-bit and the asymptotic claim is formally verified. GP-00003 turns the disproof into a contract: a concrete configuration, a deterministic constructor with empirically-verified growth, and a Lean 4 proof of the asymptotic — packaged so any party can re-run the verifier and confirm the result without trusting the original authors. **Decomposition.** Four axioms. AX-00014 is a small-case witness — produce a finite point set in ℚ² that beats the integer-lattice baseline by a stated margin, witness-checked exactly. AX-00015 is the parameterized constructor — a deterministic function C: ℕ → ℙ_fin(ℚ²) whose unit-distance counts beat n_k^(1+δ) at every sampled k, verified by exact rational arithmetic over O(K) constructor outputs. AX-00016 is the Lean 4 formalization of the asymptotic growth rate, including the class field tower and Golod-Shafarevich ingredients, verified by `lake build` against a pinned Mathlib. AX-00017 is the integration axiom that gates the GP-payout: all three artifacts published together, the constructor''s output reproduces under Omenion''s sandbox, and the Lean proof closes against the constructor''s formal definition. **Verification cost.** Witness checks are O(n²) exact-rational pair counts — milliseconds at n=10⁴, seconds at n=10⁶. The Lean check is dominated by Mathlib build time on a pinned snapshot — under an hour on standard CI. None of the axioms require simulation, training, or arbitration. This is Tier-1 verification end-to-end.

GP closes atomically when AX-00017 passes; sibling axioms pay independently.