The dependency ladder

The dependency ladder#

A reusable library is a directed acyclic graph, not a long list sorted by subject name. Each theorem should depend only on earlier, smaller interfaces, and every high-level claim should expose the mathematical bridge it still needs.

Layer map#

Layer	Core interfaces	Current state
Equality	symmetry, transitivity, successor/add/multiply congruence, constructive equality decision	checked
Addition	identities, associativity, commutativity, cancellation, zero-sum rigidity	checked
Multiplication	identities, annihilation, distributivity, associativity, commutativity, zero product	checked core
Order	reflexivity, transitivity, trichotomy, incompatibility, addition monotonicity and cancellation	checked
Divisibility	units, zero, reflexivity, transitivity, addition/product closure, constructive decision, bounded nonzero common multiples	checked
Modular congruence	balanced equivalence laws and additive/multiplicative compatibility	reflexivity, symmetry, transitivity, addition, multiplication, both decomposition bridges, and bounded uniqueness checked; fixed mod-five residue ladder checked
Parity	even/odd dichotomy and arithmetic tables	useful future application, outside the closed current catalog
Division	quotient-remainder existence, uniqueness, block separation, and zero-remainder/divisibility bridges	checked
GCD/coprime	relational symmetry/projections/constructors, uniqueness, zero-right base, Euclidean invariance, existence, balanced Bézout, Gauss cancellation, product closure	checked through `coprime_mul_left` and `coprime_mul_right`
Primes	bounded factor search, primality decision, proper-factor descent, prime divisors, Euclid’s lemma, infinitely many primes	checked through `prime_divisor_exists`, `euclid_prime_dvd_product`, and `prime_unbounded`
Factorization	sorted β-coded existence and canonical extensional uniqueness	finite-prefix recoding, exact Product traces, greatest-prime descent, canonical append, existence, uniqueness, and combined native FTA checked at this integration checkpoint; primitive lists remain absent; Lean list companion checked independently

The generated dependency-graph.mmd is the exact graph for checked entries. The research catalog is the larger design graph and gives every unproved node a status and blocker.

How an edge becomes a checked certificate#

A dependency edge is no longer implemented by copying the dependency proof at every hypothesis use. Replay first checks the dependency as a closed certificate, then embeds it in a self-contained Cut(A, B, lemma, body). The kernel checks lemma : A once and checks body : B under a new hypothesis A. Nested dependency edges become nested Cuts, so the mathematical DAG remains visible as lexical sharing inside one closed certificate.

This is not a trusted theorem environment. The Cut contains the complete lemma proof and body proof; it contains no library name, hash, declaration identifier, or callback. The object formula at each ladder node is unchanged, and every final theorem is still checked from the empty context. The trusted checker is larger by exactly this reviewed rule. The detailed boundary is in Self-contained proof sharing.

Why congruence comes first#

The proof engine already has primitive equality rules such as congruence under successor, addition, and multiplication. Named theorems such as add_congr make these transformations reusable at the mathematical level:

\[ a=b\;\land\;c=d \quad\Longrightarrow\quad a+c=b+d. \]

They are small, but they prevent later modular and divisibility proofs from reconstructing the same transport scaffolding. They also give documentation a stable name that can link code, artifacts, and concepts.

Why cancellation precedes canonical residues#

An equation \(a+m q=b+m r\) can witness congruence without ordering either \(a\) or \(b\). To prove uniqueness of canonical remainders, however, one needs order bounds and cancellation. The intended chain is

\[\begin{split} \begin{aligned} &\text{additive cancellation} \to \text{order monotonicity} \to \text{division uniqueness}\\ &\to \text{canonical-remainder uniqueness} \to \text{decidable fixed-modulus residue cases}. \end{aligned} \end{split}\]

Fixed modulus proofs should therefore be downstream clients of generic division and residue lemmas. They should not be copied into the foundation for each numeral.

The prime spine#

The important dependency chain is not “define prime, then invoke FTA.” It is

\[\begin{split} \begin{aligned} \text{strong induction} &\to \text{proper-factor descent} \to \text{prime-divisor existence},\\ \text{division + gcd + Bézout} &\to \text{Gauss cancellation} \to \text{Euclid's lemma},\\ \text{prime-divisor existence + Euclid's lemma} &\to \text{factorization existence and uniqueness}. \end{aligned} \end{split}\]

Both arithmetic lines are now checked native chains. Constructive equality decision feeds quotient-remainder-based divisibility decision. Induction on a concrete bound then gives factor_search_up_to, which either verifies the prime factor-pair condition throughout that bound or returns an explicit nontrivial factor pair. prime_or_composite applies the divisor bound at \(B=n\); prime_decidable also handles zero and one explicitly.

Proper-factor descent is separate from that search decision: proper_factor_lt proves that \(n=cd\), \(n\ne0\), and \(d\ne1\) imply \(c<n\). prime_divisor_exists_up_to uses ordinary induction on an explicit upper bound to recurse through such a factor, and prime_divisor_exists specializes the bound to \(n\). This implements formula-specific strong descent without a predicate variable, a least-factor oracle, or classical DNE. All twelve new certificates are intuitionistic.

The Euclid line uses the bounded theorem gcd_balanced_bezout_exists_up_to, which carries both the full relational gcd proof and four balanced coefficients through Euclidean descent. Its unrestricted wrapper gives coprime_balanced_bezout; coefficient scaling and the common-divisor bridge then give gauss_coprime_cancel. Finally, prime_divisor_eq_one_or_self applies the prime factor dichotomy to a relational gcd divisor of \(p\), and euclid_prime_dvd_product uses its two branches. Prime-divisor existence was proved independently; Euclid’s lemma does not supply it.

Infinitely many primes can be reached before a general factorial function. It is enough to construct, for each bound, a common multiple of every number from two to that bound and then take a prime divisor of one more than that multiple. The constructive infrastructure for the first half is now checked: bounded_common_multiple_step extends the invariant by one endpoint, and bounded_common_multiple_exists constructs a nonzero common multiple of every positive natural at most the supplied bound. The checked prime_unbounded client applies prime-divisor existence to the successor of that multiple. A divisor at or below the bound would divide the multiple as well, hence divide one by the consecutive-number remainder lemma, contradicting primality.

For FTA, the selected route uses greatest-prime-divisor descent to construct a sorted factor sequence. Single-position β-value existence, functionality, and the equivalence

\[ \operatorname{At}(b,c,i,x) \quad\Longleftrightarrow\quad x<M(c,i)\;\land\;b\equiv x\pmod{M(c,i)} \]

are now checked through fully expanded PA formulas. The checked representation layer now also includes constructive binary CRT for arbitrary nonzero coprime moduli. binary_crt_remainders recovers the two directed remainder equations, and binary_crt_beta_pair constructs one code realizing two bounded decoded values. The last theorem assumes the two expanded β moduli are coprime. The new conditional bridge proves that premise when

\[ j=i+g\qquad\text{and}\qquad g\mid c, \]

and binary_crt_beta_pair_of_gap_dvd applies it directly. The condition is not cosmetic: \(c=1\) produces moduli \(M(1,1)=3\) and \(M(1,4)=6\), so arbitrary members of the family are not pairwise coprime. Bounded common-multiple existence supplies a \(c\) divisible by every positive gap through a bound. The checked bounded-prefix theorems now prove that the whole bounded modulus family is pairwise coprime. Product coprimality and modulus descent support binary_crt_fold_step, whose universal clause preserves every old congruence modulo a divisor of the accumulated product while adding one new congruence. beta_accumulated_product_step and beta_crt_prefix_congruence_step supply the two successor halves, and beta_crt_prefix_invariant_step combines them. Ordinary induction in bounded_beta_crt_prefix_invariant now constructs, for each \(k\le N\), a nonzero accumulated product divisible by every earlier beta modulus, a value congruent to every earlier residue already decoded from the supplied code \(b\), and coprimality of that product with every future bounded beta modulus.

The full-bound projection bounded_beta_crt_for_existing_code did not by itself cross the recoding gate: its premise already said that each residue was decoded from \(b\). The later checked tranche closes that gap with an exclusive cross-base recoding invariant and beta_prefix_extend, then builds exact β-coded prefix-product traces and proves Product existence, functionality, zero/successor decomposition, append, and prefix transport. Greatest-prime descent plus canonical append yields factorization existence. Euclid’s lemma, product membership, sorted last-factor matching, and nonzero cancellation yield uniqueness by length.

At this integration checkpoint the exact endpoints check as follows:

Endpoint	Nodes	Depth	Cuts
`prime_factorization_existence`	43,973	98	1,328
`prime_factorization_uniqueness`	29,789	82	854
`fundamental_theorem_of_arithmetic`	73,767	99	2,184

The combined certificate has SHA-256 fd978f59bf3b0aa7b6c9ec1bc92ab5e7bbf949c25309173e098bd8f3b8de0958, checks from the empty context, and passes the full live-use path under the 500,000-occurrence/100,000-object/depth-256 cap. It uses PA1–PA6 and induction only, with no DNE. Runtime integration is complete.

The theorem remains deliberately relational: Peano Lab has no primitive list or multiset type, and uniqueness compares equal lengths and decoded entries, not raw β-code equality. The checked prime_unbounded theorem is not a dependency of FTA. Conventional integer-coefficient Bézout is not expressible with the natural-only terms; the four-natural balanced theorem is checked.

Admission invariants#

Every checked node must satisfy all of these conditions:

its name is stable, ASCII, lowercase snake case, and unique;
its statement is closed;
every dependency names an earlier node;
the authored script uses the reviewed library-replay surface;
replay is deterministic;
every dependency assumption is discharged by a self-contained Cut whose formula and certificate are embedded in the final proof;
the final certificate checks from the empty context;
its exact node count and depth fit the live import bound;
its source and documentation links resolve;
generated artifacts reproduce byte for byte.

Literal Cut erasure is an optional, untrusted audit, not an admission invariant. Although the formal expansion is (λh. body) lemma, the current bidirectional checker and capture-sensitive beta reducer do not provide a complete operational erasure path for every large certificate. An erased artifact has authority only if it independently passes the kernel.

These invariants turn the dependency organization into an executable contract, not merely a diagram in the documentation.