Prime existence · Native PA

Bertrand’s Postulate

n < p < 2n

The complete constructive proof graph, now in linked mathematical notation: primes, binomial coefficients, primorials, factorials, valuations, and the strict prime interval theorem.

Open the definition-aware map Read bertrand_strict Locate it in the grand campaign

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.

Complete route

Mixed dependency graph

Follow theorem dependencies and their readable definitions from the capstone BT0127 back to the arithmetic foundations.

Trace the full proof →

Exact certificate

Fully expanded PA

Inspect all 28,410 original tactic lines and the exact 1,917-edge dependency graph with every definition fully expanded.

Open the exact edition →
Zoom between mathematical scales: complete research atlas → prime-distribution family → proved Bertrand anchor → theorem and definition dependencies. The campaign also proves infinitely many primes 1 modulo 4 and 3 modulo 4; Dirichlet prime witnesses remain open.
Alpha v34 independently verified proof: 544 checked-use theorems · 202 Stable · 342 Alpha-only, not Stable · 28 linked definitions · 1,917 proof edges · 28,410 tactic lines · 45 layers. Every proof body is independently accepted by the original intuitionistic kernel and the compiled Lean verifier; historical Alpha-v12 enrollment remains unchanged.