# 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. ```{admonition} Alpha QR slice :class: note 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. {doc}`K3B ` and {doc}`K3C ` remain separate focused Alpha lenses. See {doc}`Alpha and Stable library editions ` for the canonical scope distinction. ``` ```{admonition} Defined notation is not kernel syntax :class: important 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: ```text ∀ 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`](https://github.com/nasqret/vietnam2026/blob/agent/quadratic-reciprocity-campaign/research/arithmetic-library/pa-proof-definitions.json) and its [human-readable audit](https://github.com/nasqret/vietnam2026/blob/agent/quadratic-reciprocity-campaign/research/arithmetic-library/defined-edition.md). ## 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: 1. The compact theorem statement, with every definition occurrence linked to its persistent `PD` page. 2. The definition-aware tactic body. Only proposition bodies introduced by `have` and `suffices` are compacted; ordinary tactic commands remain exact. 3. 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, ```python 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. ```{admonition} Proof paths contain theorem edges only :class: note 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 {doc}`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 {doc}`PA language reference <../peano/language-reference>` and {doc}`axioms and proof rules <../peano/axioms-and-rules>`. For theorem-only routes, use the {doc}`dependency graph `. For the promotion rules, P0/P1/P2 tiers, API-completeness matrix, and paired source release gates, continue to {doc}`Curating the next conservative edition `.