The definition-aware proof explorer

The definition-aware proof explorer#

The definition-aware explorer is a parallel reading edition of the same 557-theorem quadratic-reciprocity corpus. It gives recurring formulas short, linked names—such as Dvd(d,n), Prime(p), and ModEq(m,a,b)—without changing the explicit theorem statements, tactic scripts, proof terms, or kernel.

Alpha QR slice

This is not a second release edition and not the whole Alpha library. It is the definition-aware view of the same 557-node QR slice: 241 Stable prerequisites and 316 Alpha-only specifications. All 557 QR nodes now carry independently closed current Alpha-v16 checked-use evidence; the complete Stable catalog still has 432 rows, and the complete current Alpha v16 catalog has 1,673. K3B and K3C remain separate focused Alpha lenses. See Alpha and Stable library editions for the canonical scope distinction.

Defined notation is not kernel syntax

Every purple token on these pages is produced by an untrusted, conservative presentation layer. Before replay, the compiler expands the theorem statement and every compacted local proposition back into the ordinary PA formula language. The unchanged kernel sees only that expansion. A definition page is therefore neither an axiom nor a theorem nor a new predicate constant.

Open the definition-aware explorer Draw the mixed graph · PA00FW Open the exact explicit edition

What the second edition changes#

The complete elaboration pass covers all 557 theorem specifications and all 27,491 tactic lines. Of the 557 statements, 506 contain at least one selected definition. Of the 1,839 proposition-bearing have or suffices commands, 1,275 become definition-aware.

Surface measured	Fully expanded text	Defined edition	Reduction
all theorem statements	2,457,096 characters	107,386 characters	95.63%
all local `have`/`suffices` propositions	1,971,403	111,519	94.34%
longest theorem statement (`PA00EH`)	82,377	1,759	97.86%
largest expanded `have` command (`PA00FE`, line 15)	36,497	642	98.24%

The longest remaining defined local proposition is 963 characters (PA00EX, line 26); its full have command is 988 characters.

The quadratic-reciprocity endpoint itself is now displayed as:

∀ p. ∀ q. Prime(p) → Prime(q) → ¬p = q → Odd(p) → Odd(q) →
  (Mod4One(p) ∨ Mod4One(q) →
     (QRes(p,q) ∧ QRes(q,p)) ∨ (¬QRes(p,q) ∧ ¬QRes(q,p))) ∧
  (Mod4Three(p) ∧ Mod4Three(q) →
     (QRes(p,q) ∧ ¬QRes(q,p)) ∨ (¬QRes(p,q) ∧ QRes(q,p)))

This is the same parsed formula as the expanded endpoint, not a replacement theorem. Open PA00FW to move from any purple predicate call to its expansion and back to the exact native statement.

The persistent inventory, including raw overlapping occurrence counts and source provenance, is recorded in pa-proof-definitions.json and its human-readable audit.

The forty persistent definitions#

Mathematical layer	Linked definition pages
order and divisibility	`Le` · `Lt` · `Dvd` · `DivRem`
primes, gcd, and coprimality	`Prime` · `Coprime` · `IsGCD`
congruence, parity, and small residues	`ModEq` · `Even` · `Odd` · `Mod4One` · `Mod4Three`
finite coding and folds	`BetaAt` · `Product` · `Sum` · `AllBits` · `BitCount` · `Range` · `Repeat` · `Pow` · `Factorial`
quadratic residues	`QRes` · `BoundedQRes`
finite maps and factorization invariants	`BoundedPrefix` · `InjectivePrefix` · `SurjectivePrefix` · `ContainsPrefix` · `AllPrime` · `Sorted`
modular units and inverse maps	`UnitResidue` · `BalancedInverse` · `BoundedNonzeroInverse` · `ScaledInverse` · `ScaledFixedPoint` · `SuccessorInverse` · `InverseIndex` · `InversePrefix` · `ScaledInverseIndex` · `ScaledInversePrefix`
finite division traces	`DivisionPrefix`

AllPrime and Sorted have no whole-schema occurrence in this particular QR closure, but they are retained because the same notation registry also serves the factorization and FTA development. Three broader authoring composites— PermutationPrefix, BalancedBezout, and CanonicalPF—are also accepted by the opt-in parser, but remain outside the forty persistent graph nodes in this frozen edition.

Three synchronized views of one proof#

Every theorem page presents three related objects:

The compact theorem statement, with every definition occurrence linked to its persistent PD page.
The definition-aware tactic body. Only proposition bodies introduced by have and suffices are compacted; ordinary tactic commands remain exact.
The expanded native statement and an expandable Exact native replay line beneath every changed local command.

The adapter records a SHA-256 receipt for each exact explicit statement and tactic line. It also checks that expanding each compact formula reconstructs the same parsed PA abstract syntax tree. The explorer validates those receipts against the frozen explicit corpus before it writes any page.

This makes back-and-forth reading deliberate: open a purple formula token to study its expansion, follow a theorem token to its formal proof, and expand the native replay line whenever the abstraction hides a detail you want to inspect.

Authoring with the notation#

The notation is also available through an explicit compiler API. For example,

from peano_lab.library.defined_edition import (
    DefinedTheoremSpec,
    compile_defined_spec,
)

surface = DefinedTheoremSpec(
    "dvd_self_readable",
    "forall n. Dvd(n,n)",
    ("mul_one",),
    ("intro n", "exists 1", "symm", "apply mul_one"),
    "Every natural number divides itself.",
)
native = compile_defined_spec(surface)

native is an ordinary TheoremSpec: Dvd has already disappeared from its statement, and the normal proof engine and kernel receive only the expanded PA formula. The core parsing entry points still reject defined calls; authors opt in by using parse_defined_formula* or this compiler.

Reading the mixed dependency graph#

The mixed graph contains two kinds of vertices and two logically different kinds of arrows:

Shape	Meaning
Rounded theorem node	One theorem in the exact PA corpus
Purple hexagon	A conservative display definition
Solid proof arrow \(A\to B\)	Theorem \(A\) is a direct prerequisite of theorem \(B\)
Purple notation arrow \(T\to D\)	The statement or a local proof proposition of theorem \(T\) uses definition \(D\)

Definition-to-definition arrows record that one readable expansion is phrased using another definition. They describe notation structure, not proof authority. The graph records statement and local-proposition occurrence counts separately.

The mixed graph opens in a sparse neighborhood mode. It adds only the selected node’s definition closure and draws only the selected node’s direct arrows plus the theorem premise path. Definitions can be switched to off or to all definitions used by the visible theorems; Arrows can be hidden or restored in full. These controls suppress visual objects only. The selected-node panel and typed graph API continue to expose every exact proof and notation relation.

Proof paths contain theorem edges only

Critical paths and prerequisite cones are computed exclusively from the frozen theorem dependency adjacency. Purple notation edges never shorten, extend, or otherwise participate in a proof path.

Trust boundary and provenance#

Persistent PA tags identify theorem pages; persistent PD tags identify definitions. The generated corpus records the explicit-corpus digest, the definition-edition identity, source locations, expansion hashes, and all typed edges. None of those identifiers grants theorem authority. The generated labels remain exactly those of the explicit QR proof explorer, but they are campaign-local rather than canonical evidence: the later HA receipt upgrades mod_eq_add_cancel_left to alpha_closed only in the Alpha catalog. The historical labels are not a complete edition catalog.

This edition gate validates source-to-source compilation for all 557 specifications; it is not a second closed-certificate replay or admission claim. This notation view adds no proof evidence; canonical evidence, including the later HA overlap upgrade, comes from the Alpha catalog and its receipts.

For the core grammar and accepted proof constructors, read the PA language reference and axioms and proof rules. For theorem-only routes, use the dependency graph.

For the promotion rules, P0/P1/P2 tiers, API-completeness matrix, and paired source release gates, continue to Curating the next conservative edition.