Unique division · canonical signed Bézout · unordered prime factors · Constructive arithmetic

Constructive arithmetic and unique factorization

n>0 ⇒ ∃ prime factor list; any two lists are related by a witnessed bijection

Expose exact foundation interfaces and construct an actual finite permutation between arbitrary prime factorizations, with no sorting or supplied canonicalization.

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

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 1588 native tactic lines and 85 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem AF001B and follow only the lemmas and conservative definitions supporting prime_factorization_exists_unique_up_to_permutation.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G001 milestone · G002 milestone · G003 milestone · G004 milestone · G005 milestone → theorem and definition dependencies.
Major independently established statements: AF0001 foundation_division_exists_unique · AF0002 foundation_signed_bezout_canonical_gcd · AF0003 foundation_coprime_product_divisor · AF0004 foundation_prime_factor_list_exists · AF001A prime_factor_lists_permutation_exists · AF001B prime_factorization_exists_unique_up_to_permutation.
Independently verified Alpha v34 checked-use theorem family: 27 dependency-curried kernel-checked theorem bodies · 85 proof prerequisites · 22 linked definitions · 28 definition-dependency arrows · 1588 exact tactic lines · first admitted v28 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 862 bundle nodes; SHA-256 e56dda386bf60759d1bacda45417eacd7e6a67fd6e23799f002aac9964253ae1.
Exact mathematical boundary: The original division, gcd, cancellation, and factor-existence foundations are exposed through checked wrappers. Unordered uniqueness adds an actual bounded, injective, surjective index map matching repeated prime occurrences. The empty factor list represents one, not zero.