BP0001 bertrand_window_prime_divides_central_binomEvery prime strictly between n and 2n divides C(2n,n).
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; 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.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableBP0003 bertrand_window_central_valuation_at_most_oneEvery central-binomial valuation at a Bertrand-window prime is at most one.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableBP0004 bertrand_window_central_valuation_nonzeroA Bertrand-window prime divides the positive central coefficient nontrivially.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableBP0005 bertrand_window_central_valuation_equals_oneEvery Bertrand-window prime has exact central-binomial valuation one.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableBP0006 bertrand_window_central_valuation_oneEvery Bertrand-window prime has a witnessed literal valuation-one graph.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableBP0007 central_binom_prime_divisor_multiplicity_one_existsFor every n>1, a prime in (n,2n) divides C(2n,n) exactly once.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableBP0008 bertrand_chain_singleton_code_existsEvery initial natural has an exact witnessed singleton Gödel-beta code.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableBP0009 bertrand_chain_singleton_existsA singleton beta code is a valid strict-Bertrand chain of zero steps.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableBP000A bertrand_chain_successor_preserves_guardEvery strict Bertrand successor preserves the initial 1<n domain guard.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableBP000B bertrand_chain_prefix_extendAppending a strict Bertrand successor recodes and preserves every prior chain edge.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableBP000C bertrand_chain_prefix_terminal_existsInduction constructs arbitrary strict prime chains and their guarded terminal values.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableBP000D iterated_bertrand_prime_chain_existsEvery n>1 and finite k admit an exact beta-coded chain of k strict Bertrand primes.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableND0001 Beta(b,c,i,x)Exact hygienic Gödel-beta extraction; a signature-identical alias of checked BetaAt.
Conservative definition · notation layer 0PD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0PD0004 Prime(p)p is nonunit and every factorization of p has a unit factor.
Conservative definition · notation layer 0PD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0PD0003 Dvd(d,n)The natural number d divides n.
Conservative definition · notation layer 0PD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0PD0014 Product(b,c,l,z)z is the product of a beta-coded prefix of length l.
Conservative definition · notation layer 1PD0019 Repeat(b,c,a,l)The decoded prefix repeats a for l positions.
Conservative definition · notation layer 1PD0020 Pow(a,e,z)z is the relational e-th power of a.
Conservative definition · notation layer 2PD0044 PowerDivides(p,e,n)The relational power p to exponent e divides n.
Conservative definition · notation layer 3PD0045 BoundedPowerValuation(p,n,b,e)e is the greatest exponent at most b for which p to that exponent divides n.
Conservative definition · notation layer 4PD0046 PowerValuation(p,n,e)e is the canonical bounded p-adic power valuation of n.
Conservative definition · notation layer 5ND0006 BertrandWindow(n,p)Prime(p) together with the exact strict inequalities n<p<2*n.
Conservative definition · notation layer 1ND0007 PowerValuationOne(p,n)The exact existing bounded prime-power valuation relation at literal exponent one.
Conservative definition · notation layer 6ND0008 BertrandChain(b,c,n,k)A beta-coded length-k strict prime chain starting at n, without choice or a new sequence primitive.
Conservative definition · notation layer 2Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.