The definition-aware Bertrand proof explorer

This parallel reading edition presents the complete 544-theorem proof of Bertrand’s Postulate using 28 conservative, linked mathematical definitions. It keeps all 1,917 proof dependencies, 28,410 authored tactic lines, and the exact endpoint BT0127, while making the campaign’s powers, binomial coefficients, primorials, valuations, and prime intervals readable.

Definitions are presentation, not proof authority

Each compact formula expands to exactly the original first-order PA formula. No definition introduces a kernel rule, axiom, predicate constant, theorem, or checked-use admission. The frozen Alpha-v12 catalog remains the sole source for theorem statements, tactic scripts, dependency evidence, and provenance.

Open the definition-aware Bertrand explorer Draw the mixed proof-and-definition graph Read the strict Bertrand theorem Inspect the exact fully expanded edition

Mathematical vocabulary of the proof

The explorer reuses foundational arithmetic notation where appropriate and introduces campaign-local abbreviations for the structures that actually drive Bertrand’s proof:

Proof layer	Relevant mathematical definitions
order, divisibility, and primality	Le, Lt, Dvd, and Prime
finite arithmetic constructions	Pow, Factorial, and encoded finite products
binomial coefficients	Choose and CentralBinom
products of primes	Primorial and its prime-factor support
prime-power accounting	PowerValuation and FactorialValuation
Legendre’s formula	LegendreSum and the factorial-valuation bridge
square-root bounds	FloorSqrt and the small-prime cutoff

Every highlighted call links to a definition page giving its arity, explicit first-order expansion, conceptual prerequisites, and the theorems that use it. The original statement and exact proof commands remain available beside their compact presentation.

Reading the mixed dependency graph

Solid arrows connect theorem prerequisites; purple arrows connect a theorem to definitions appearing in its statement or local proof propositions. Definition-to-definition arrows describe conservative notation structure. Only theorem arrows participate in proof paths, prerequisite cones, critical routes, and the 45-layer depth calculation.

The initial view focuses on BT0127 and its immediate proof neighborhood. Switch to Prerequisites for the complete proof, enable all definitions to inspect the visible mathematical vocabulary, or follow any linked theorem to its exact certificate and source provenance.

For the original frozen graph and release-evidence boundary, see the complete Bertrand proof explorer. For the mathematical campaign, see Bertrand’s Postulate.