BP0001 · bertrand_window_prime_divides_central_binomEvery prime strictly between n and 2n divides C(2n,n).
layer 0 · 22 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableCurrent 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.
BP0002 · bertrand_window_prime_square_exceeds_doubleA prime above n has square strictly larger than 2n.
layer 0 · 42 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBP0003 · bertrand_window_central_valuation_at_most_oneEvery central-binomial valuation at a Bertrand-window prime is at most one.
layer 1 · 45 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBP0004 · bertrand_window_central_valuation_nonzeroA Bertrand-window prime divides the positive central coefficient nontrivially.
layer 1 · 39 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBP0005 · bertrand_window_central_valuation_equals_oneEvery Bertrand-window prime has exact central-binomial valuation one.
layer 2 · 41 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBP0006 · bertrand_window_central_valuation_oneEvery Bertrand-window prime has a witnessed literal valuation-one graph.
layer 3 · 46 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBP0007 · central_binom_prime_divisor_multiplicity_one_existsFor every n>1, a prime in (n,2n) divides C(2n,n) exactly once.
layer 4 · 32 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBP0008 · bertrand_chain_singleton_code_existsEvery initial natural has an exact witnessed singleton Gödel-beta code.
layer 0 · 11 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBP0009 · bertrand_chain_singleton_existsA singleton beta code is a valid strict-Bertrand chain of zero steps.
layer 1 · 19 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBP000A · bertrand_chain_successor_preserves_guardEvery strict Bertrand successor preserves the initial 1<n domain guard.
layer 0 · 12 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBP000B · bertrand_chain_prefix_extendAppending a strict Bertrand successor recodes and preserves every prior chain edge.
layer 0 · 83 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBP000C · bertrand_chain_prefix_terminal_existsInduction constructs arbitrary strict prime chains and their guarded terminal values.
layer 2 · 55 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableBP000D · iterated_bertrand_prime_chain_existsEvery n>1 and finite k admit an exact beta-coded chain of k strict Bertrand primes.
layer 3 · 15 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableExactly 13 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.