Ctrl+K

Curating the next conservative edition

Curating the next conservative edition#

The definition-aware explorer demonstrated that mathematical names can reduce the statement corpus by more than 95% without changing a single native formula. The next step is not to add more abbreviations indiscriminately. It is to turn the useful definitions into a coherent authoring API while retaining the exact expanded corpus as a regression oracle.

The invariant

Prime, Dvd, BetaAt, and every other displayed relation remain untrusted macros. They expand hygienically to the existing first-order formula AST before a theorem specification or certificate reaches the kernel. Definition nodes may appear in the reading graph, never in a proof path.

The first eleven definitions#

The P0 facade freezes the relations that are both broadly mathematical and central to the current dependency graph:

Layer

Canonical relations

order

Le, Lt

divisibility and primes

Dvd, Prime

gcd and division

Coprime, IsGCD, DivRem

congruence

ModEq

finite coding and folds

BetaAt, Product, Sum

Each relation gets one AST-first builder and one template owner. Duplicate private string builders are removed only after the replacement expands to the same parsed formula in every existing theorem and typed intermediate step.

A definition is not yet a library#

For every relation the curation dashboard records seven API families:

  1. introduction or construction;

  2. elimination and projections;

  3. zero, one, successor, and empty-prefix boundaries;

  4. characterization, uniqueness, or functionality;

  5. transport through equality, congruence, or recoding;

  6. constructive decision/search, or an explicit blocker;

  7. composition such as transitivity, append, restriction, or Euclidean step.

This exposes gaps that theorem counts hide. Prime(p), for example, becomes a useful interface only together with prime nonzero, factor characterization, decision, prime-divisor existence, and Euclid’s lemma.

Two synchronized source editions#

Every curated theorem has a readable source and an explicit source:

defined theorem + defined have/suffices propositions
                         │
                         ▼ expand and compare
ordinary theorem + ordinary tactic commands
                         │
                         ▼ construct
                 checked certificate

The release gate compares statement ASTs, dependency lists, statuses, expanded local propositions, authored commands, and deterministic certificate hashes. It also tests capture, shadowing, wrong arity, unknown names, definition cycles, and registry drift.

Dependency tiers#

  • P0 contains the eleven canonical general-purpose relations above.

  • P1 contains reusable parity, finite-fold, residue, factorial, bounded-map, and factorization relations, depending only on earlier P0/P1 definitions.

  • P2 contains campaign-specific inverse-prefix and division-prefix surfaces and remains visibly namespaced.

BalancedBezout, PermutationPrefix, and CanonicalPF are reviewed for new persistent IDs only after their occurrence and API value is established. Existing PD0001–PD0040 identifiers are never recycled.

Immediate route#

The verifier prerequisite is closed: Cut-aware source ab966fd1 passed pinned Lean 4.31/WMI job 218358. The remaining tranche is deliberately ordered:

  1. centralize the P0 AST builders without changing statements;

  2. complete the Even/Odd API and modulo-two bridges;

  3. add the round-tripping Prime surface and capture tests;

  4. generate fixed-residue classifications from generic division and congruence theorems;

  5. publish the first API matrix and duplicate-builder report before expanding P2.

The binding technical policy is curation-policy.md. Use the definition-aware explorer to inspect the current 40-definition baseline and language and trust for the kernel boundary.

Contents