LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)

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.

The divisibility poset is lower-finite, and each divisor interval factorises as a product of finite chains of prime exponents

Statement

The divisibility poset $\mathbb Z_{>0}$ is lower-finite. More precisely, if $a\mid b$ and $q:=b/a$ , choose the distinct prime divisors $p_0,\ldots,p_{r-1}$ of $q$ and put $e_i:=v_{p_i}(q)$ . Then

$[a,b]_{\mid}\cong\prod_{i<r}\{0,1,\ldots,e_i\}$

as posets, where the right side has coordinatewise order. The isomorphism sends $d=ac$ to $(v_{p_i}(c))_{i<r}$ . For $q=1$ the product is the one-point empty product.

Facts & Assumptions

Given: Positive integers $a\mid b$ , their positive quotient $q=b/a$ , and the divisibility poset of The divisibility poset of positive integers.

[L1]

A divisor $d$ of a nonzero integer $n$ satisfies $d\ne0$ and $|d|\le|n|$ , so a positive divisor $d$ of a positive integer $n$ satisfies $1\le d\le n$ (If $d \mid a$ and $a \ne 0$ then $d \ne 0$ and $|d| \le |a|$ ; hence the set of divisors of a nonzero integer is bounded above by $|a|$ ).

[L2]

Every nonnegative integer is the image of a unique natural number, and the embedding preserves order (The naturals embed in the integers).

[L3]

Subsets of finite sets are finite (A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$ , and equality holds if and only if $B = A$ ).

[L4]

Canonical prime factorisation expresses a positive integer as the product of its distinct prime powers, with the exponent $v_p$ uniquely determined (For $n \ge 1$ and any injective list $p : r \to \mathbb{Z}$ of primes containing every prime divisor of $n$ , one has $n = \prod_{i<r} p_i^{\,v_{p_i}(n)}$ ; the exponents are determined by $n$ , and $v_q(n) = 0$ for every prime $q$ outside the list, The $p$ -adic valuation $v_p(a)$ of a nonzero integer: the greatest $k \in \mathbb{N}$ with $p^{k} \mid a$ ).

[L5]

For positive integers $c,c'$ , $c\mid c'$ exactly when $v_p(c)\le v_p(c')$ for every prime $p$ (For positive integers $a$ and $b$ : $a \mid b$ if and only if $v_p(a) \le v_p(b)$ for every prime $p$ ).

[L6]

Finite Cartesian products of finite sets are finite (The product rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$ , and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$ ).

Proof

technique · direct

1.1

For a positive integer $n$ , every element of its principal ideal is a positive divisor $d$ with $1\le d\le n$ by [L1]. By [L2] these integers correspond to a subset of the finite natural initial segment through $n$ , hence form a finite set by [L3]. Thus the divisibility poset is lower-finite.

L1L2L3

1.2

Multiplication by $a$ gives an order isomorphism from $[1,q]_{\mid}$ to $[a,b]_{\mid}$ : if $c\mid q$ , then $ac\mid aq=b$ ; and if $a\mid d\mid b$ , write $d=ac$ and cancel $a$ from $b=aq=d t=act$ to get $q=ct$ .

givenconstruct

1.3

By [L4], every divisor $c$ of $q$ has the unique form $c=\prod_{i<r}p_i^{k_i}$ with $0\le k_i\le e_i$ , and every such exponent tuple gives a divisor of $q$ . Thus $c\mapsto(k_i)_{i<r}$ is a bijection from $[1,q]_{\mid}$ to the displayed finite Cartesian product.

L4L6

2.1

By [L5], $c\mid c'$ holds exactly when $k_i\le k'_i$ for every $i<r$ , so the bijection in step 1.3 preserves and reflects the order.

step 1.3L5

3.1

Composing steps 1.2 and 1.3 gives the asserted interval factorisation; step 2.1 makes it a poset isomorphism, and step 1.1 proves lower-finiteness.

step 1.1step 1.2step 1.3step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 98 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

R. Stanley, Enumerative Combinatorics, Volume 1, §§3.8.4–3.8.5 (standard reference, not scraped)