Uniqueness of prime factorization, as multiplicity agreement

Identifier: F:nat-multiset-prime-factorization-unique
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

If two multisets of primes over the naturals have the same product, then they assign the same multiplicity to every natural. This is uniqueness of prime factorization, stated as agreement of multiplicities rather than as a permutation between two lists.

Formal statement

theorem Nat.Multiset.count_eq_of_prod_eq : ((x0 : AxNat.Multiset) -> ((x1 : AxNat.Multiset) -> ((x2 : ((x2 : AxNat) -> ((x3 : AxNat.lt AxNat.zero (AxNat.Multiset.count x0 x2)) -> And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) x2) (((x4 : AxNat) -> ((x5 : AxNat.dvd x4 x2) -> Or (Eq.{1} AxNat x4 (AxNat.succ AxNat.zero)) (Eq.{1} AxNat x4 x2))))))) -> ((x3 : ((x3 : AxNat) -> ((x4 : AxNat.lt AxNat.zero (AxNat.Multiset.count x1 x3)) -> And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) x3) (((x5 : AxNat) -> ((x6 : AxNat.dvd x5 x3) -> Or (Eq.{1} AxNat x5 (AxNat.succ AxNat.zero)) (Eq.{1} AxNat x5 x3))))))) -> ((x4 : Eq.{1} AxNat (AxNat.Multiset.prod x0) (AxNat.Multiset.prod x1)) -> ((x5 : AxNat) -> Eq.{1} AxNat (AxNat.Multiset.count x0 x5) (AxNat.Multiset.count x1 x5)))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

7 direct dependencies 0 direct dependents

Evidence

kernel-multiset-count-eq-of-prod-eq

Kind: kernel-term
Status: checked

Supports: Nat.Multiset.count_eq_of_prod_eq is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- Multiset.count_eq_of_prod_eq 2>/dev/null | grep -Ec '^Nat\.Multiset\.count_eq_of_prod_eq[[:space:]]')" -ge 1

Evidence notes

`build_nat_prelude` admits this theorem only through the trusted kernel gate, so a successful build IS the type-check. `crates/axeyum-lean-kernel/src/nat_prelude/multiset_tests.rs` additionally INSTANTIATES it at the two multisets {2,3} and {3,2} -- built by `Nat.Multiset.add` in opposite orders, so different constructor arguments and different bounds -- with the three hypotheses abstracted rather than proved, and checks that the inferred conclusion at the point 2 reduces to `1 = 1`, with `1 = 2` as the negative control.

footprint-multiset-count-eq-of-prod-eq

Kind: instance-pin
Status: checked

Supports: axiom_footprint: [] -- the Nat environment admits no trusted declaration

Checker command

cargo run -q -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free nat

Evidence notes

Reports `nat: axiom=0 opaque=0 quotient=0 total_trusted=0` over the FULL trusted surface (Axiom, Opaque and Quotient), not `Declaration::Axiom` alone, and exits non-zero unless the surface is empty. The enumeration is per-environment rather than per-theorem; it bounds this theorem's footprint because a proof cannot depend on a trusted declaration the environment does not contain. Read directly from `Kernel::axiom_footprint` for these ten `Nat.Multiset.*` theorems, `theorem_axiom_footprint` prints footprint size 0 and an empty axiom column for every one.

Provenance

{
  "date": "2026-09-02",
  "established_by": "axeyum-lean-kernel build_nat_prelude",
  "source": "theorem name and canonical type read directly via nat_theorem_inventory, which prints render_lean of the admitted type; declared by `nat_prelude/multiset.rs` (lane nat-multiset, ADR-1520)."
}