Construct the actual first k primes, prove that none is omitted, and bound the last prime by explicitly constructed powers of two.
Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable
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.
PE0001 · foundation_primes_above_every_boundG021: every supplied natural bound has an actual larger prime; no nonempty list or prime-search witness is supplied.
layer 0 · 8 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE0002 · least_prime_above_finite_scanFinite decidable scanning either finds the actual least prime above a or proves every such prime exceeds the scanned interval.
layer 0 · 57 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE0003 · least_prime_above_existsEuclid unboundedness terminates the finite least-prime scan without any unbounded-search axiom.
layer 1 · 25 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE0004 · least_prime_above_uniqueThe least prime above any natural is uniquely determined by its minimality, not by its code.
layer 0 · 20 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE0005 · least_prime_above_bertrand_boundBertrand's theorem bounds the actual consecutive prime, rather than only producing a sparse prime subsequence.
layer 0 · 24 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE0006 · least_prime_above_exists_uniqueLeast-prime search is a total, uniquely valued constructive relation for every natural input.
layer 2 · 14 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE0007 · initial_prime_chain_singleton_existsThe one-entry initial prime chain is an actual beta code of the prime two.
layer 0 · 16 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE0008 · initial_prime_chain_prefix_extendAppending the actual next prime preserves every old decoded entry and every minimal-successor edge.
layer 0 · 82 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE0009 · initial_prime_chain_prefix_restrictEvery initial segment retains the same genuine least-prime transitions.
layer 0 · 19 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE000A · initial_prime_chain_terminal_is_primeEvery decoded terminal entry of an initial-prime chain is genuinely prime, including the first entry two.
layer 0 · 45 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE000B · initial_prime_chain_bounded_existsConstruct the first k+1 primes with their actual terminal value strictly below the witnessed power 2^(k+2).
layer 2 · 84 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE000C · first_primes_double_exponential_boundFor every positive k, construct exactly the first k primes and both power witnesses proving p_k < 2^(2^k).
layer 3 · 62 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE000D · initial_prime_chain_strict_orderEvery earlier decoded prime is strictly smaller than the terminal prime; repetitions and descending lists are excluded.
layer 1 · 87 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE000E · initial_prime_chain_exhausts_primesEvery prime no larger than a decoded terminal prime occurs in the actual prefix; no smaller prime is omitted.
layer 1 · 110 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE000F · prime_list_nonempty_chainEvery positive-length first-prime list exposes its actual final index and minimal-successor chain.
layer 0 · 10 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE0010 · prime_list_every_entry_is_primeEvery entry of every first-prime list is prime, with the empty-list boundary proved vacuously.
layer 1 · 36 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE0011 · prime_list_omits_no_smaller_primeThe first-prime list is exhaustive below each of its entries, with an explicit bounded index witnessing every smaller prime.
layer 2 · 42 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE0012 · prime_list_strictly_increasingEvery first-prime list is strictly increasing at all valid index pairs, not merely at its last transition.
layer 2 · 44 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StablePE0013 · first_primes_list_existsEvery finite number of initial primes has a real beta-coded list, including the empty list at zero.
layer 4 · 25 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableExactly 19 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.