# 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. ```{admonition} Two views at all times :class: tip 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. ``` ## Your learning route The checkboxes below are stored only in this browser. They do not affect the book, prover, or repository. (stage-foundations)= ## 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: ```text 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. ```{admonition} Predict before opening the card :class: dropdown 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-order)= ## 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

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-division)= ## 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: ```text 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-bezout)= ## 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-euclid)= ## 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-primes)= ## 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-beta)= ## 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

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-products)= ## 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-factorization)= ## Stage 9 — existence and uniqueness take different routes Existence selects a greatest prime divisor $p$ of $n$, writes $n=pq$, proves $q

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-fta)= ## Stage 10 — the native Fundamental Theorem of Arithmetic The combined theorem is the conjunction of the two preceding endpoints. Its authored body is exactly: ```text split exact prime_factorization_existence exact prime_factorization_uniqueness ``` ```{admonition} Why three commands still produce 73,767 nodes :class: dropdown 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 {doc}`theorem atlas ` as the back-and-forth proof reader. - Read {doc}`Language, notation, and trust ` when an exact expanded formula looks mysterious. - Read {doc}`Self-contained proof sharing ` when a short script seems too small for its measured certificate. - Read {doc}`Primes and unique factorization ` for the full representation argument and the separate Lean list-based cross-check. - Use {doc}`Using and extending the library ` to reproduce or extend the checked artifacts.