Showcase / abstract-regular-polyhedron-realizable-iff
Attribution inferred from git history (no explicit solver credit). Kernel-verified at Gate A; no human in the correctness path.
The goal record the swarm was asked to discharge — the source of truth for this proof's identity and difficulty.
The Lean statement the swarm proved, kernel-verified at Gate A.
import Mathlib
theorem abstract_regular_polyhedron_realizable_iff (p q : ℕ) (hp : 3 ≤ p) (hq : 3 ≤ q) :
(p, q) ∈ ({(3, 3), (3, 4), (4, 3), (3, 5), (5, 3)} : Finset (ℕ × ℕ)) ↔
∃ V E F : ℕ, 0 < V ∧ 0 < F ∧ p * F = 2 * E ∧ q * V = 2 * E ∧ V + F = E + 2 := by
sorry