The complete Bertrand proof explorer

This explorer is the line-by-line reading room for the complete transitive dependency closure of bertrand_strict. It uses the same searchable theorem pages and layered graph controls as the quadratic-reciprocity explorer, but its input is the exact Alpha-v12 catalog rather than an independently curated campaign stack. A parallel definition-aware edition links 28 conservative definitions for primes, binomial coefficients, primorials, factorials, powers, valuations, and the other mathematical relations used by the proof.

Complete proof, conservative release status

The map contains all 544 theorem nodes, 1,917 direct dependency edges, 28,410 authored tactic lines, and 45 layers needed by the final strict Bertrand theorem. Of those nodes, 203 have checked-use evidence and 341 are Alpha body_checked rows. The focused endpoint suites independently kernel-check complete empty-context certificates; Alpha v12 still withholds checked-use from its new rows pending a later promotion review.

Permanent explorer tags have the form BTxxxx. They are derived from the immutable Alpha enrollment index in base 35, so additive editions cannot renumber an existing page. The final endpoint is BT0127, bertrand_strict.

Open the definition-aware proof map Browse theorems and linked definitions Open the exact expanded proof map Search all 544 theorem pages Open the final strict theorem

Reading with mathematical definitions

The definition-aware edition presents each native theorem in conservative mathematical notation, while preserving its exact fully expanded PA statement and tactic script. Its mixed graph distinguishes genuine proof-dependency arrows from notation links. Definition nodes are reading aids: they introduce no axiom, kernel rule, theorem dependency, or additional proof authority.

Open the definition-aware theorem and definition index or the readable strict Bertrand endpoint. Every linked definition exposes its exact expanded formula, while the original expanded edition remains available.

For the campaign-specific vocabulary and mixed-graph trust boundary, continue to the definition-aware Bertrand proof explorer.

Reading the map

Arrows point from prerequisite to dependent. The initial view displays the complete 544-node prerequisite cone but only the focused route arrows, keeping the overview legible. Select All direct arrows to draw the literal 1,917-edge graph. Other views expose:

• a shortest route from a theorem root;

• a critical route witnessing the full 45-layer depth;

• every route between a selected start and the endpoint;

• a direct neighborhood; or

• the dependent cone of any selected theorem.

Click any node to inspect its statement, evidence status, direct relations, and source. The theorem-page link opens the exact expanded PA statement and the complete numbered tactic body. Browser Back and Forward retrace the route.

What the map does and does not certify

The builder reads the byte-frozen Alpha-v12 catalog and verifies the hash of every source file represented in the closure. It does not execute tactics, construct certificates, change enrollment, or grant proof authority. The graph is a navigable rendering of evidence established elsewhere:

• candidate bodies were checked with their declared dependencies as hypotheses;

• focused recursive-closure tests rebuilt and kernel-checked the final BP01 and BP02 empty-context certificates; and

• Alpha v12 records reviewed provenance while continuing to reject checked replay for its body_checked suffix.

For the mathematical narrative, see the Bertrand campaign. For the release distinction, see Alpha and Stable library editions.