A guided route from zero to FTA

A guided route from zero to FTA#

This chapter is a map for repeated passes through the library. On a first pass, read the mathematical idea in each stage. On a second pass, open the exact native statement and proof links. On later passes, move backward to a missing prerequisite or forward to a theorem that consumes it.

Two views at all times

Readable notation such as \(a\mid b\), \(\gcd(a,b)=d\) and \(\operatorname{Product}(F,n)\) is explanatory notation. The native theorem cards show the fully expanded first-order formulas actually parsed and checked by Peano Lab.

Stage 1 — equality, semiring laws and induction#

Peano Lab begins with 0, successor S, addition, multiplication and equality. Even familiar algebraic laws are theorems. For example, PA3 explains addition by recursion on the right, so the left identity

\[0+n=n\]

requires induction.

The complete native session is small enough to run here:

pa> pa prove forall n. 0 + n = n
pa> induction n
pa> simp
pa> simp [IH]
pa> qed

Open the zero_add proof card, then move forward to add_comm. Its card shows exactly why zero_add and add_succ_left are the two prerequisites.

Predict before opening the card

Why does add_comm need two earlier theorems while add_assoc is proved directly by induction? Look at which argument PA3 unfolds, and then compare the two authored scripts in the atlas.

Stage 2 — discrete order without a primitive relation#

The surface notation \(a\le b\) expands to an additive gap:

\[ a\le b \quad:\!\Longleftrightarrow\quad \exists k.\;k+a=b. \]

Strict order is encoded by \(S(a)\le b\). This makes constructive order proofs witness-producing: a proof that \(a\le b\) contains the distance from \(a\) to \(b\). Cancellation, monotonicity and the discrete split

\[a\le b \Longrightarrow a=b\ \lor\ a<b\]

are the descent tools used by division, bounded factor search and factorization induction.

Additive gap
k + a = b

Cancellation
remove common prefixes

Descent
strictly smaller recursive input

Use the atlas to traverse le_refl → le_eq_or_lt → proper_factor_lt.

Stage 3 — division with remainder#

The native relation is

\[ \operatorname{DivRem}(n,d,q,r) \quad:\!\Longleftrightarrow\quad n=dq+r\ \land\ S(r)\le d. \]

The successor step has exactly two branches:

n = dq + r
current quotient and remainder

S(r) < d
keep q, replace r by S(r)

S(r) = d
replace q by S(q) and reset r to 0

division_remainder_succ implements that invariant. The general theorem first uses constructive case analysis to write the nonzero divisor as a successor, then specializes the successor theorem:

pa> pa prove forall m n. ~(m = 0) -> exists q r. n = m * q + r /\ S r <= m
pa> use zero_or_succ
pa> use division_remainder_succ
pa> intro m
pa> intro n
pa> intro hm
pa> specialize zero_or_succ m
pa> cases zero_or_succ
pa> exfalso
pa> apply hm
pa> exact zero_or_succ_left
pa> cases zero_or_succ_right
pa> specialize division_remainder_succ x
pa> specialize division_remainder_succ n
pa> rewrite zero_or_succ_right_witness
pa> rewrite zero_or_succ_right_witness
pa> exact division_remainder_succ
pa> qed

The wrapper has 219 nodes; uniqueness grows to 854 nodes because two quotient blocks must be separated and then the remainders cancelled. Move between division_remainder_exists and division_remainder_unique to compare their neighborhoods.

Stage 4 — relational GCD and balanced Bézout#

There is no gcd(a,b) term. Instead, IsGCD(d,a,b) expands to:

\[ d\mid a\ \land\ d\mid b\ \land \forall c.\;c\mid a\to c\mid b\to c\mid d. \]

Euclidean invariance transports this relation across \(a=bq+r\). The existence proof then performs formula-specific bounded descent and removes the bound with reflexivity.

Ordinary integer coefficients are also absent. The checked balanced equation uses four naturals:

\[ a x_+ + b y_+ = d + a x_- + b y_-. \]

It represents \(ax+by=d\) with \(x=x_+-x_-\) and \(y=y_+-y_-\) without adding integers or subtraction to the language.

a = bq + r
division witness

GCD(b, r) + balance
inductive package

GCD(a, b) + balance
transport coefficients

Study the complete scripts for balanced_bezout_euclid_step and gcd_balanced_bezout_exists.

Stage 5 — from Bézout to Gauss cancellation and Euclid’s lemma#

Balanced Bézout supplies the algebra behind Gauss cancellation:

\[ \operatorname{Coprime}(a,b)\land a\mid bc \Longrightarrow a\mid c. \]

For a prime \(p\), take a relational gcd \(g\) of \(p\) and \(a\). Every divisor of a prime is either \(1\) or the prime itself:

if \(g=1\), then \(p\) and \(a\) are coprime and Gauss cancellation gives \(p\mid b\);
if \(g=p\), the gcd witness already gives \(p\mid a\).

Thus

\[p\mid ab\Longrightarrow p\mid a\lor p\mid b.\]

The full 36-command proof is embedded in euclid_prime_dvd_product. Move backward from that card to see its four immediate prerequisites, or forward to finite-product membership and factorization uniqueness.

Stage 6 — constructive prime search and a prime above every bound#

Primality is the expanded factor-pair formula

\[ \operatorname{Prime}(p)\;:\!\Longleftrightarrow\; p\ne1\land\forall a,b.\;p=ab\to(a=1\lor b=1). \]

Because the kernel is intuitionistic, negating that formula does not magically extract a factor. The library builds bounded factor search, a constructive prime-or-composite decision, proper-factor descent, and finally prime_divisor_exists.

Prime unboundedness then uses a separate Euclidean argument:

Common multiple c
every 1 ≤ t ≤ n divides c

Prime p ∣ S(c)
prime-divisor existence

n < p
otherwise p ∣ c and p ∣ 1

Open prime_unbounded to read all 84 authored commands and traverse its ten direct prerequisites.

Stage 7 — Gödel-β codes from division and CRT#

A β code is a pair of naturals \((b,c)\). Position \(i\) is decoded modulo

\[M(c,i)=1+(i+1)c.\]

The exact BetaAt(b,c,i,x) relation says that \(x<M(c,i)\) and that \(x\) is the remainder of \(b\) modulo \(M(c,i)\). Nothing here is a new sequence primitive: it is an expanded formula made from addition, multiplication, equality and existential witnesses.

DivRem
functional bounded remainders

Binary + bounded CRT
combine compatible residues

β prefix extension
preserve old entries, append one

The main construction is beta_prefix_extend: 105 authored commands elaborate, with checked dependencies, to 29,057 nodes.

Stage 8 — finite products without primitive lists#

One β code stores factors \(p_0,p_1,\ldots,p_{l-1}\). A second code stores prefix products \(r_0,r_1,\ldots,r_l\) with

\[r_0=1,\qquad r_{i+1}=r_i p_i,\qquad r_l=n.\]

factor code

p₀

p₁

⋯

p_l−1

product trace

r₀ = 1

r₁ = r₀p₀

⋯

r_l = n

The second code is not cosmetic. First-order PA cannot recursively multiply an unbounded list term because no such term exists. The trace makes every successor multiplication locally checkable.

Compare beta_prefix_product_trace_exists, beta_product_functional and beta_factor_divides_product.

Stage 9 — existence and uniqueness take different routes#

Existence selects a greatest prime divisor \(p\) of \(n\), writes \(n=pq\), proves \(q<n\), recursively factors \(q\), and appends \(p\). Greatestness makes the append preserve sortedness.

n
nonzero input

n = pq, q < n
p greatest prime divisor

factor q, append p
sorted canonical code

Uniqueness instead compares two sorted codes. Euclid’s lemma proves that the last prime in one product occurs in the other; sortedness forces it to be the other last prime. Cancel that factor and recurse on the shorter prefix.

same product
two sorted prime codes

match last primes
finite-product Euclid + sortedness

cancel and recurse
equal length and entries

Use the atlas to compare the two large wrappers: prime_factorization_existence and prime_factorization_uniqueness.

Stage 10 — the native Fundamental Theorem of Arithmetic#

The combined theorem is the conjunction of the two preceding endpoints. Its authored body is exactly:

split
exact prime_factorization_existence
exact prime_factorization_uniqueness

Why three commands still produce 73,767 nodes

Before the body is checked, prime_factorization_existence and prime_factorization_uniqueness have each been reconstructed as complete closed certificates. Cut embeds those certificates once and exposes their formulas locally. The final split uses the two local hypotheses. The kernel therefore receives a single self-contained tree, not three trusted theorem names.

Component	Nodes	Depth	Cuts
existence	43,973	98	1,328
uniqueness	29,789	82	854
combined FTA	73,767	99	2,184

The exact certificate SHA-256 is fd978f59bf3b0aa7b6c9ec1bc92ab5e7bbf949c25309173e098bd8f3b8de0958. It passes empty-context replay, live use/exact/qed, dependency and hypothesis mutation tests, a PA-leaf mutation, and a no-DNE/PA1–PA6 audit.

Open the complete fundamental_theorem_of_arithmetic card. Then use its prerequisite and dependent columns to move backward into the two proofs or forward into any future client theorem.

What to do next#

Use the theorem atlas as the back-and-forth proof reader.
Read Language, notation, and trust when an exact expanded formula looks mysterious.
Read Self-contained proof sharing when a short script seems too small for its measured certificate.
Read Primes and unique factorization for the full representation argument and the separate Lean list-based cross-check.
Use Using and extending the library to reproduce or extend the checked artifacts.