Exact binomial valuation · arbitrarily long prime chains · Constructive arithmetic

Bertrand prime windows and iterated chains

n < p < 2n · vₚ(C(2n,n)) = 1 · pᵢ < pᵢ₊₁ < 2pᵢ

Thirteen complete proofs establish a prime of multiplicity exactly one in the central binomial coefficient and construct beta-coded strict Bertrand chains of arbitrary finite length.

Open the definition-aware map Read the final theorem See campaign milestone G024

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.

Exact certificate

Fully expanded arithmetic

Inspect all 462 native tactic lines and 40 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem BP000D and follow only the lemmas and conservative definitions supporting iterated_bertrand_prime_chain_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G023 milestone · G024 milestone → theorem and definition dependencies.
Major independently established statements: BP0007 central_binom_prime_divisor_multiplicity_one_exists · BP000D iterated_bertrand_prime_chain_exists.
Independently verified Alpha v34 checked-use theorem family: 13 dependency-curried kernel-checked theorem bodies · 40 proof prerequisites · 15 linked definitions · 17 definition-dependency arrows · 462 exact tactic lines · first admitted v20 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 590 bundle nodes; SHA-256 1b623064f36e362c1a117daa193b1ee33ee7905ec804ee1ac164b42345b67069.
Exact mathematical boundary: Every displayed theorem was first admitted in Alpha v20, remains independently kernel- and Lean-verified for current Alpha v30 checked use, and has not been promoted to Stable.