BT0127, while making the
campaign's powers, binomial coefficients, primorials, valuations, and prime
intervals readable.
```{admonition} Definitions are presentation, not proof authority
:class: important
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 onBT0127 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
{doc}`complete Bertrand proof explorer