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.
Sparse modes suppress visual objects only. Every local proof and notation relation remains in the selected-node panel; external prerequisites and their exact release evidence appear on each individual theorem page.
Proof arrows run from prerequisite to dependent; notation arrows run from a theorem or definition to the conservative definition it uses. Select a node to inspect every direct relation.
dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged.
Constructive numerical example
Finite browser arithmetic illustrates the displayed formulas; it is not a theorem certificate.
Evidence and release boundary
All 102 displayed theorems are independently kernel- and Lean-verified Alpha v34 checked-use results: the historical 44-row forward construction and parity foundations, plus 58 square-factor, full inverse, strict-descent, and zero-boundary theorems first admitted in Alpha v26. G077 and G078 are complete. The all-z square-hypotenuse obstruction and full natural Fermat-four solution classification are unconditional; Stable remains unchanged.
Alpha v30 contains 102 of 102 displayed theorem bodies, including 102 independently verified alpha_closed checked-use theorems from 3222 checked release theorems; no displayed theorem is admitted to Stable. Historical replay experiments have no persisted certificate and do not change release evidence, checked-use authority, or Stable admission.