# Existence, Euclid's lemma and unique factors [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-unique-prime-factorization/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-unique-prime-factorization-01 · ocme-new142-reader-adoption-20261021 ## Goal and scope Every positive integer n>1 has a unique prime multiset; 360=2^3*3^2*5, with signs and units separate. Existence and uniqueness by strong induction and an explicit Bezout prerequisite, then complete trial division for 360. ## Givens and symbols - calc - G1 — The theorem domain is integers n>1; the example is 360; factor order is ignored but multiplicity retained. - p_i,q_j — prime factors with multiplicity - r,s — finite factor counts ## Rules and sources - calc · prerequisite — Assume exact integer arithmetic, division with remainder, and definitions of divisibility and gcd; every congruence has an explicit modulus. Also assume well-founded/strong induction on positive integers and the Bezout identity for coprime integers. - mko_definition · cited — Separate existence from uniqueness. Induction/well-founded reasoning gives existence, with complete bounded trial-division instances as computational companions. Uniqueness keeps the Euclid-lemma witness p|ab implies p|a or p|b, not just a few matching outputs. General factorizations may contain several distinct primes. Separate a negative sign, units±1 with the empty prime product and zero, which has no such factorization. · mko-unique-prime-factorization ## Main derivation S01 · impliesBefore n>1,\quad d=\min\{m>1:m\mid n\} After d\text{ prime} Conditions: none Rule: calc · Uses: G1 Leaf basis: calc If d=uv with 11\Rightarrow q\text{ has prime factors by induction} Conditions: none Rule: calc · Uses: G1, S01 Leaf basis: calc The quotient is smaller than n; strong induction factors q and adjoining d proves existence, with n=2 covered by q=1. S03 · impliesBefore p\text{ prime},\quad p\mid ab,\quad p\nmid a After \gcd(p,a)=1\Rightarrow\exists u,v:\ up+va=1 Conditions: none Rule: calc · Uses: G1 Leaf basis: calc The only positive divisors of p are 1,p; since p does not divide a, they are coprime and the stated Bezout prerequisite applies. S04 · impliesBefore up+va=1,\quad p\mid ab After b=upb+vab\Rightarrow p\mid b Conditions: none Rule: calc · Uses: G1, S03 Leaf basis: calc After multiplication by b, both terms are divisible by p, proving Euclid's lemma. S05 · impliesBefore \prod_{i=1}^{r}p_i=\prod_{j=1}^{s}q_j,\quad p_i,q_j\text{ prime} After p_1\mid\prod_{j=1}^{s}q_j\Rightarrow\exists j:\ p_1\mid q_j\Rightarrow p_1=q_j Conditions: none Rule: calc · Uses: G1, S04 Leaf basis: calc Finite-product induction using Euclid's lemma makes p1 equal to one prime on the right. S06 · impliesBefore p_1=q_j\ne0 After \text{cancel }p_1\text{ and induct on }r+s\Rightarrow\{p_i\}_{\rm multiset}=\{q_j\}_{\rm multiset} Conditions: none Rule: calc · Uses: G1, S02, S05 Leaf basis: calc Cancel the nonzero prime and decrease the total factor count until empty product 1; a nonempty prime product is at least 2 and cannot equal 1. S07 · impliesBefore 360 After 360=2\cdot180=2^2\cdot90=2^3\cdot45=2^3\cdot3\cdot15=2^3\cdot3^2\cdot5 Conditions: none Rule: calc · Uses: G1, S01, S02 Leaf basis: calc Extract 2 three times and 3 twice, leaving 5. Primes 2,3 qualify, and testing 2 suffices for remaining 5 since 3^2>5. S08 · impliesBefore 2^3\cdot3^2\cdot5=360 After 360\text{ has multiset }\{2,2,2,3,3,5\}\text{ uniquely} Conditions: none Rule: mko_definition · Uses: G1, S06, S07 Leaf basis: mko_definition Recheck the exact product; the uniqueness argument ensures any other prime list differs only in order. S09 · impliesBefore -360,\quad1,\quad-1,\quad0 After -360=-(2^3 3^2 5),\quad\pm1\text{ use empty prime product};\quad0\text{ excluded} Conditions: none Rule: calc · Uses: G1, S06, S08 Leaf basis: calc A negative sign is a unit factor; ±1 use empty prime product 1, and zero is outside the n>1 factorization domain. ## Substeps and lemmas No substeps in this guide. ## Reverse audits - S09 · premise_audit · G1, S06, S08 — Every prime divides zero, so it cannot have a finite unique prime multiset. - S08 · premise_audit · G1, S06, S07 — A single prime-power expression is insufficient because this example has three distinct primes. - S07 · premise_audit · G1, S01, S02 — The remaining 5 is not an unchecked composite; trial division reaches the square-root boundary. - S06 · premise_audit · G1, S02, S05 — Uniqueness retains multiplicities while ignoring order, and distinguishes empty from nonempty endpoints. - S05 · premise_audit · G1, S04 — This handles arbitrary finite prime factorizations, not merely two computed outputs. - S04 · premise_audit · G1, S03 — The case p dividing a is immediate; composite p does not ensure the preceding coprimality. - S03 · premise_audit · G1 — This identifies the actual Bezout dependency rather than assuming the Euclid lemma being proved. - S02 · premise_audit · G1, S01 — Induction uses only smaller positive integers, not the same n. - S01 · premise_audit · G1 — The divisor set is nonempty because n itself belongs; well-foundedness supplies its minimum. ## Error controls and negative controls Existence and uniquenessStrong induction gives existence; Euclid's lemma and cancellation give uniqueness. MultiplicityCompare prime multisets, not only distinct-prime sets. - 360=2^3*3*5. → reject — The right side is 120, missing a factor 3. - Euclid's lemma also holds for composite 4. → reject — 4 divides 2*2 but neither factor 2. - Zero's prime factorization is the empty product. → reject — The empty product is 1, not zero. ## Result and limitations Every positive integer n>1 has a unique prime multiset; 360=2^3*3^2*5, with signs and units separate. ## Verification and source binding 1 declared checks for this guide; only the listed expressions are covered. - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 648c53ebc102df797ce25af2afb0b128976c45a091ff54b1a47d03de1a9d1ad6 - original source SHA-256: 648c53ebc102df797ce25af2afb0b128976c45a091ff54b1a47d03de1a9d1ad6 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-unique-prime-factorization-01.json)