Actual Euclidean gcd · norm descent · witnessed units and permutation · Constructive arithmetic

Unique factorization in the Gaussian integers

0≠z∈ℤ[i] ⇒ z=u·π₁⋯πₖ, unique up to witnessed units and permutation

Construct a finite prime factorization of every nonzero Gaussian integer, and a genuine matching between any two factorizations.

Open the definition-aware map Read the final theorem See campaign milestone G082

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 7859 native tactic lines and 673 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem GF00B2 and follow only the lemmas and conservative definitions supporting gaussian_unique_prime_factorization.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G082 milestone → theorem and definition dependencies.
Major independently established statements: GF001B gaussian_unit_iff_norm_one · GF0053 gaussian_divides_decidable · GF0065 gaussian_gcd_bezout_exists · GF0066 gaussian_gcd_unique_up_to_associate · GF006C gaussian_irreducible_iff_prime · GF0098 gaussian_prime_factorization_exists · GF00B2 gaussian_unique_prime_factorization.
Independently verified Alpha v34 checked-use theorem family: 180 dependency-curried kernel-checked theorem bodies · 673 proof prerequisites · 38 linked definitions · 68 definition-dependency arrows · 7859 exact tactic lines · first admitted v30 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 453 bundle nodes; SHA-256 e0e10f11c5b12b411843054000a77be22ede7db53602814f9532e3e7c8daa270.
Exact mathematical boundary: Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.