Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every integer n1n \ge 1 is a finite product of primes: there are rNr \in \mathbb{N} and a list p:rZp : r \to \mathbb{Z} of primes with n=i<rpin = \prod_{i<r} p_i, the case n=1n = 1 being the empty product

Statement

Write finite products in the commutative monoid (Z,,1)(\mathbb{Z},\cdot,1) of (Z,,1)(\mathbb{Z}, \cdot, 1) is a commutative monoid whose group of units is {1,1}\{1, -1\}; equivalently u1u \mid 1 holds exactly for u=1u = 1 and u=1u = -1, as in The product g0g1gn1g_0 g_1 \cdots g_{n-1} of a finite list in a monoid, by recursion, with the empty product (n=0n = 0) equal to the identity; a list of primes of length rr means a function p:rZp : r \to \mathbb{Z} on the von Neumann natural r={0,,r1}r = \{0,\dots,r-1\} with every pip_i prime (Prime and composite integers: pp is prime when p>1p > 1 and its only positive divisors are 11 and pp).

  1. Existence. For every nZn \in \mathbb{Z} with n1n \ge 1 there are rNr \in \mathbb{N} and a list p:rZp : r \to \mathbb{Z} of primes with

    n  =  i<rpi.n \;=\; \prod_{i<r} p_i .

    At n=1n = 1 this holds with r=0r = 0: the empty product is 11, so 11 is a product of primes, of no primes at all, and needs no separate clause.

  2. Every such product is at least 11. Conversely, for every rNr \in \mathbb{N} and every list p:rZp : r \to \mathbb{Z} of primes, i<rpi1\prod_{i<r} p_i \ge 1. So the integers of clause 1 are exactly the values of finite products of primes.

Facts & Assumptions

Given: The commutative monoid (Z,,1)(\mathbb{Z},\cdot,1) ((Z,,1)(\mathbb{Z}, \cdot, 1) is a commutative monoid whose group of units is {1,1}\{1, -1\}; equivalently u1u \mid 1 holds exactly for u=1u = 1 and u=1u = -1, Semigroup and monoid); the embedding ι:NZ\iota : \mathbb{N} \to \mathbb{Z} of The naturals embed in the integers; and the property P(k)P(k): "if ι(k)1\iota(k) \ge 1 then ι(k)=i<rpi\iota(k) = \prod_{i<r} p_i for some rNr \in \mathbb{N} and some list p:rZp : r \to \mathbb{Z} of primes".

[L1]

i<0gi=e\prod_{i<0} g_i = e and i<σ(r)gi=(i<rgi)gr\prod_{i<\sigma(r)} g_i = \bigl(\prod_{i<r} g_i\bigr) \cdot g_r; the value depends only on g0,,gr1g_0,\dots,g_{r-1}, so a list u:rMu : r \to M determines i<rui\prod_{i<r} u_i (The product g0g1gn1g_0 g_1 \cdots g_{n-1} of a finite list in a monoid, by recursion, with the empty product (n=0n = 0) equal to the identity).

[L3]

Strong induction: if for every kk the truth of PP below kk implies P(k)P(k), then PP holds everywhere on N\mathbb{N} (Strong (complete) induction).

[L4]

Induction: a subset of N\mathbb{N} containing 00 and closed under σ\sigma is N\mathbb{N} (The principle of mathematical induction).

[L5]

ι\iota is injective, preserves addition, multiplication and order, and its image is exactly the nonnegative integers, with ι(0)=0\iota(0) = 0 and ι(1)=1\iota(1) = 1 (The naturals embed in the integers, The integers as equivalence classes of pairs of naturals).

[L7]

The order on Z\mathbb{Z} is total, antisymmetric and transitive, is compatible with addition, and positives are closed under multiplication (The integers form a totally ordered ring, Order on the integers).

[L8]

Z\mathbb{Z} is a commutative ring: multiplication is associative and commutative, x1=xx \cdot 1 = x, x0=0x \cdot 0 = 0, multiplication distributes over addition, and every xx has an additive inverse x-x, with (x)=x-(-x) = x and (x)y=(xy)(-x)y = -(xy); we write uvu - v for u+(v)u + (-v) (The integers form a commutative ring, Arithmetic on the integers).

[L9]

On N\mathbb{N}: 0k0 \le k for every kk (Order on the natural numbers); m<km < k exactly when σ(m)k\sigma(m) \le k (Discreteness: σ(n)\sigma(n) is the immediate successor); 1=σ(0)1 = \sigma(0) (The natural numbers N\mathbb{N} (von Neumann)); and r<σ(r)r < \sigma(r), with i<σ(r)i < \sigma(r) exactly when iri \le r (On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n).

Proof

technique · induction
1.1

0<10 < 1 in Z\mathbb{Z}: 1=ι(1)1 = \iota(1) lies in the image of ι\iota, so 101 \ge 0, and 101 \ne 0 because ι\iota is injective and ι(0)=0\iota(0) = 0.

L5
1.2

Discreteness: if xZx \in \mathbb{Z} and 0<x0 < x then 1x1 \le x. Indeed x0x \ge 0, so x=ι(k)x = \iota(k) for some kk; k0k \ne 0 since ι(0)=0x\iota(0) = 0 \ne x; so 0<k0 < k in N\mathbb{N}, hence 1=σ(0)k1 = \sigma(0) \le k, and applying the order-preserving ι\iota gives 1x1 \le x.

L5L9
1.3

Let kNk \in \mathbb{N} and assume P(j)P(j) for every j<kj < k.

ih
2.1

Clause 2. Let TT be the set of rNr \in \mathbb{N} such that i<rpi1\prod_{i<r} p_i \ge 1 for every list p:rZp : r \to \mathbb{Z} of primes. Then 0T0 \in T, the empty product being 11. If rTr \in T and p:σ(r)Zp : \sigma(r) \to \mathbb{Z} is a list of primes, then i<σ(r)pi=(i<rpi)pr\prod_{i<\sigma(r)} p_i = \bigl(\prod_{i<r} p_i\bigr) p_r, where the restriction of pp to rr is again a list of primes, so the first factor is 1>0\ge 1 > 0; and pr>1>0p_r > 1 > 0; positives being closed under multiplication the product is >0> 0, hence 1\ge 1 by step 1.2. So σ(r)T\sigma(r) \in T, and T=NT = \mathbb{N}.

step 1.1step 1.2L1L4L6L7
2.2

P(0)P(0) holds vacuously: ι(0)=0\iota(0) = 0 and 010 \ge 1 is false, since 0<10 < 1.

basestep 1.1L5
2.3

Suppose ι(k)1\iota(k) \ge 1 and write n:=ι(k)n := \iota(k); by totality either n=1n = 1 or n>1n > 1. If n=1n = 1, take r:=0r := 0: the empty list is a list of primes and i<0pi=1=n\prod_{i<0} p_i = 1 = n, so P(k)P(k) holds.

step 1.1L1L7
3.1

Suppose instead n>1n > 1. Fix a prime qq with qnq \mid n and an integer mm with n=qmn = qm.

step 2.3L2L10choose
4.1

m>0m > 0: m=0m = 0 would give n=q0=0<1n = q \cdot 0 = 0 < 1, and m<0m < 0 would give m>0-m > 0, hence q(m)>0q(-m) > 0, that is n>0-n > 0 and n<0<1n < 0 < 1; both contradict n1n \ge 1. So m>0m > 0 and therefore m1m \ge 1 by step 1.2.

step 1.1step 1.2step 3.1L7L8
5.1

m<nm < n: since q>1q > 1 we have q1>0q - 1 > 0, and m>0m > 0, so (q1)m>0(q-1)m > 0; and (q1)m=qmm=nm(q-1)m = qm - m = n - m, whence nm>0n - m > 0 and m<nm < n.

step 3.1step 4.1L6L7L8
6.1

As m1>0m \ge 1 > 0, write m=ι(j)m = \iota(j) with jNj \in \mathbb{N}. Then j<kj < k: otherwise kjk \le j, and ι\iota preserving the order would give n=ι(k)ι(j)=mn = \iota(k) \le \iota(j) = m, contradicting step 5.1.

step 4.1step 5.1L5L7
7.1

By step 1.3 applied to jj there are sNs \in \mathbb{N} and a list p:sZp : s \to \mathbb{Z} of primes with m=i<spim = \prod_{i<s} p_i.

step 1.3step 4.1step 6.1
8.1

Define p:σ(s)Zp' : \sigma(s) \to \mathbb{Z} by pi:=pip'_i := p_i for i<si < s and ps:=qp'_s := q; every value is prime, and i<σ(s)pi=(i<spi)ps=mq=qm=n\prod_{i<\sigma(s)} p'_i = \bigl(\prod_{i<s} p'_i\bigr) \cdot p'_s = m q = q m = n, the middle equality because the product over i<si < s depends only on p0,,ps1p'_0,\dots,p'_{s-1}, which agree with pp. So P(k)P(k) holds with r:=σ(s)r := \sigma(s).

step 3.1step 7.1L1L8L9
9.1

Steps 2.3 and 8.1 cover the two possibilities for nn, so P(k)P(k) follows from the truth of PP below kk; with step 2.2 as the case k=0k = 0, strong induction gives P(k)P(k) for every kNk \in \mathbb{N}.

step 2.2step 2.3step 8.1L3
10.1

Finally, any n1n \ge 1 satisfies n>0n > 0, so n=ι(k)n = \iota(k) for some kNk \in \mathbb{N}, and P(k)P(k) is clause 1 for that nn; clause 2 is step 2.1.

step 1.1step 2.1step 9.1L5L7discharge-induction

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 74 results over 25 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources