Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Definition in prerequisite notation
p + N · qn + en = n + N · qp + ep ∧ (SignedDifferenceSquare(ep,en,t · t) ∧ Le(t + t,N))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((((p) + (N) * (qn)) + (en) = ((n) + (N) * (qp)) + (ep)) /\ ((((((ep) * (ep))) + (((en) * (en)))) = ((((t) * (t))) + (((((ep) * (en))) + (((en) * (ep))))))) /\ (exists ge_gap_lowerlayerhalf_bound. ge_gap_lowerlayerhalf_bound + (((t) + (t))) = (N))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
none