Alphabeta Math
Session-authored (Fable 5 assisted)
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.

15 results · all verified · 7 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full by a delegated reviewing agent on the owner's instruction; the judge is an additional, independent cross-model AI review of the proofs. The 8 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Inclusion–Exclusion, the Pigeonhole Principle and Double Counting

1 · Prerequisites

2 · Summary

Finite cardinality, finite sums over arbitrary finite index sets, the sum and product rules, binomial coefficients, and the canonical embedding of the naturals into the reals supply the counting and arithmetic background. The alternating binomial-row identity controls signed subset sums, while ordered-field arithmetic permits subtraction and division after natural counts are embedded in R\mathbb{R}. A finite incidence relation supplies row and column fibres, and a finite family of subsets of a named ambient set supplies its intersections, including the empty intersection relative to that ambient set.

Counting a finite incidence relation by either fibre family yields double counting and the averaging principle; applying the same partition-of-fibres argument to a function gives the strong pigeonhole principle and its ceiling form. Pointwise alternating sums over traces give inclusion-exclusion, and partial binomial-row sums give the Bonferroni bounds. Sieving functions by omitted values counts surjections, while sieving permutations by fixed points gives the derangement formula and its recurrences. Finally, longest increasing and decreasing sublists ending at each position define an injective rank-pair map, proving the Erdős–Szekeres bound; decreasing blocks ordered increasingly supply the sharp examples of length mnmn.

3 · Logical flowchart

4 · Definitions, theorems and proofs

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

iSjTaij=(i,j)S×Taij=jTiSaij\sum_{i \in S}\sum_{j \in T} a_{ij} = \sum_{(i,j) \in S \times T} a_{ij} = \sum_{j \in T}\sum_{i \in S} a_{ij} for finite index sets SS and TT

Statement

Let SS and TT be finite sets and let a:S×TRa : S \times T \to \mathbb{R}, or a:S×TNa : S \times T \to \mathbb{N}, written aija_{ij} for a(i,j)a(i,j). Then S×TS \times T is finite and

iS(jTaij)  =  pS×Tap  =  jT(iSaij),\sum_{i \in S}\Big(\sum_{j \in T} a_{ij}\Big) \;=\; \sum_{p \in S \times T} a_p \;=\; \sum_{j \in T}\Big(\sum_{i \in S} a_{ij}\Big),

all three sums being the sums over a finite index set of The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form, carried by Finite sums and finite products, by recursion when the values are real and by Finite sums and finite products of natural numbers, k<nak\sum_{k<n} a_k and k<nak\prod_{k<n} a_k in N\mathbb{N} when they are natural.

This is not a clause of The sum rule: a finite disjoint union is finite with AB=A+B\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert and iIAi=iIAi\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert, and a sum over a finite index set splits along a partition. That theorem splits one sum along a partition of its own index set; the identity above exchanges the roles of two different index sets, and it is what an argument that counts a set of pairs in two ways needs. Both outer index sets may be empty, in which case all three quantities are 00 (respectively 11 for the product form of the underlying recursion), since a sum over the empty index set is the empty sum.

Facts & Assumptions

Given: Finite sets SS and TT, and a list aa defined on S×TS \times T with values in R\mathbb{R} or in N\mathbb{N}.

[L2]

Splitting along a partition: if PP is finite, JJ is finite, and (Pj)jJ(P_j)_{j \in J} are pairwise disjoint subsets of PP whose union is PP, then pPap=jJ(pPjap)\sum_{p \in P} a_p = \sum_{j \in J}\big(\sum_{p \in P_j} a_p\big), for real-valued and for natural-valued aa alike (The sum rule: a finite disjoint union is finite with AB=A+B\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert and iIAi=iIAi\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert, and a sum over a finite index set splits along a partition, clause 3).

[L3]

Reindexing along a bijection: if h:VPh : V \to P is a bijection of finite sets then vVah(v)=pPap\sum_{v \in V} a_{h(v)} = \sum_{p \in P} a_p (The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form, clause (b)).

[L4]

A map with a two-sided inverse is a bijection (Injection, surjection, bijection).

Proof

technique · direct
1.1

The row slices. For iSi \in S put Pi:={i}×TP_i := \{i\} \times T. Each PiP_i is a subset of the finite set S×TS \times T, hence finite; the family (Pi)iS(P_i)_{i \in S} is pairwise disjoint, because a point of PiP_i has first coordinate ii; and its union is S×TS \times T, because every pS×Tp \in S \times T is (i,j)(i,j) for some iSi \in S and jTj \in T.

L1construct
1.2

The column slices. For jTj \in T put Qj:=S×{j}Q_j := S \times \{j\}. The same three observations with the coordinates exchanged show that each QjQ_j is finite, that the family (Qj)jT(Q_j)_{j \in T} is pairwise disjoint, and that its union is S×TS \times T.

L1construct
1.3

The slice bijections. For iSi \in S the map hi:TPih_i : T \to P_i, hi(j):=(i,j)h_i(j) := (i,j), takes its values in PiP_i by definition and has the second-coordinate map as a two-sided inverse, so it is a bijection; likewise gj:SQjg_j : S \to Q_j, gj(i):=(i,j)g_j(i) := (i,j), is a bijection for each jTj \in T.

L3L4construct
2.1

Splitting the sum over S×TS \times T along the row slices gives pS×Tap=iS(pPiap)\sum_{p \in S \times T} a_p = \sum_{i \in S}\big(\sum_{p \in P_i} a_p\big).

step 1.1L2
2.2

Splitting it along the column slices gives pS×Tap=jT(pQjap)\sum_{p \in S \times T} a_p = \sum_{j \in T}\big(\sum_{p \in Q_j} a_p\big).

step 1.2L2
2.3

Reindexing each inner sum along the bijection of step 1.3 gives pPiap=jTahi(j)=jTaij\sum_{p \in P_i} a_p = \sum_{j \in T} a_{h_i(j)} = \sum_{j \in T} a_{ij} for every iSi \in S, and pQjap=iSaij\sum_{p \in Q_j} a_p = \sum_{i \in S} a_{ij} for every jTj \in T.

step 1.3L3
3.1

Substituting step 2.3 into step 2.1 and into step 2.2 gives iS(jTaij)=pS×Tap=jT(iSaij)\sum_{i \in S}\big(\sum_{j \in T} a_{ij}\big) = \sum_{p \in S \times T} a_p = \sum_{j \in T}\big(\sum_{i \in S} a_{ij}\big), which is the statement.

step 2.1step 2.2step 2.3

Remarks

  • What is actually used. Only the splitting clause and the reindexing clause, and each of them is stated for a real-valued and for a natural-valued summand. One argument therefore proves both readings, and nothing about subtraction or about the order enters.

  • Why the slices and not an induction. The two partitions of S×TS \times T are the same set cut two ways, so the identity is a statement about one sum, not a statement relating two recursions. That is why no induction appears and why the empty cases need no separate treatment: a sum over an empty index set is the empty sum, and the argument passes through it unchanged.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

A relation RX×YR \subseteq X \times Y between finite sets, its row fibres RxR_x and its column fibres RyR^y

Definition

Let XX and YY be finite sets (Finite, countably infinite, countable, uncountable, The cardinality A\lvert A\rvert of a finite set) and let RX×YR \subseteq X \times Y be a relation between them. For xXx \in X and yYy \in Y set

Rx:={yY : (x,y)R},Ry:={xX : (x,y)R},R_x := \{\, y \in Y \ :\ (x,y) \in R \,\}, \qquad R^{y} := \{\, x \in X \ :\ (x,y) \in R \,\},

the row fibre of RR at xx and the column fibre of RR at yy.

XYx1x2x3y1y2y3Sample:Rx2=fy2;y3gandRy2=fx1;x2g.

(a) Everything here is finite. X×YX \times Y is finite (The product rule: A×B=AB\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert, and i<mAi=i<mAi\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert, clause 1), so RR is finite as a subset of it, and RxYR_x \subseteq Y and RyXR^{y} \subseteq X are finite as subsets of finite sets (A subset of a finite set is finite, with BA\lvert B\rvert \le \lvert A\rvert, and equality holds if and only if B=AB = A, clause 1). Hence R\lvert R\rvert, Rx\lvert R_x\rvert and Ry\lvert R^{y}\rvert are all defined, and each is a natural number (The cardinality A\lvert A\rvert of a finite set).

(b) The fibres are the slices of RR, up to a bijection. For xXx \in X,

R({x}×Y)  =  {x}×Rx,R \cap (\{x\} \times Y) \;=\; \{x\} \times R_x ,

since (u,v)(u,v) lies in the left-hand side exactly when u=xu = x, vYv \in Y and (x,v)R(x,v) \in R, that is exactly when u=xu = x and vRxv \in R_x. The map y(x,y)y \mapsto (x,y) is a bijection of RxR_x onto {x}×Rx\{x\} \times R_x, its two-sided inverse being the second-coordinate map (Injection, surjection, bijection), so {x}×Rx=Rx\lvert\{x\} \times R_x\rvert = \lvert R_x\rvert by the transport clause (c) of The cardinality A\lvert A\rvert of a finite set. Symmetrically R(X×{y})=Ry×{y}R \cap (X \times \{y\}) = R^{y} \times \{y\} and Ry×{y}=Ry\lvert R^{y} \times \{y\}\rvert = \lvert R^{y}\rvert.

(c) The slices partition RR. The sets {x}×Rx\{x\} \times R_x, for xXx \in X, are pairwise disjoint, because a point of {x}×Rx\{x\} \times R_x has first coordinate xx; and their union is RR, because every (u,v)R(u,v) \in R has uXu \in X and vRuv \in R_u. Symmetrically the sets Ry×{y}R^{y} \times \{y\}, for yYy \in Y, are pairwise disjoint with union RR.

(d) Neighbours. When X=YX = Y and RR is symmetric ((x,y)R(x,y) \in R implies (y,x)R(y,x) \in R) and irreflexive ((x,x)R(x,x) \notin R for every xx), Rx=RxR_x = R^{x} and this common set is called the set of neighbours of xx; it is a subset of X{x}X \setminus \{x\}.

Remarks

  • A relation, not a matrix. The object counted here is a subset of a product of two finite sets. Nothing about arrays, entries or indices by position is used, and the two fibre families are the only structure the counting arguments need.

  • No graph vocabulary. Clause (d) fixes the words symmetric, irreflexive and neighbour for a relation on a single finite set. Nothing among this page's declared prerequisites defines a graph, and none of the results stated with clause (d) needs one.

  • Both fibre families are indexed by a finite set, which is what lets the cardinalities be summed at all: a sum over a finite index set is defined only when the index set is finite (The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form).

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

Double counting: xXRx=R=yYRy\sum_{x \in X}\lvert R_x\rvert = \lvert R\rvert = \sum_{y \in Y}\lvert R^y\rvert for a relation between finite sets

Statement

Let XX and YY be finite sets and let RX×YR \subseteq X \times Y, with row fibres RxR_x and column fibres RyR^{y} as in A relation RX×YR \subseteq X \times Y between finite sets, its row fibres RxR_x and its column fibres RyR^y. Then, in N\mathbb{N},

xXRx  =  R  =  yYRy,\sum_{x \in X}\lvert R_x\rvert \;=\; \lvert R\rvert \;=\; \sum_{y \in Y}\lvert R^{y}\rvert ,

the sums being those of The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form.

Both index sets may be empty. If X=X = \varnothing then R=R = \varnothing, every column fibre is empty, and all three quantities are 00; the same holds with the roles of XX and YY exchanged.

Facts & Assumptions

Given: Finite sets XX and YY, a relation RX×YR \subseteq X \times Y, and its fibres.

[L1]
[L2]

The row slices {x}×Rx\{x\}\times R_x and column slices Ry×{y}R^y\times\{y\} are pairwise disjoint within their respective families and each family has union RR by clause (c); they are finite because clause (b) bijects them with the finite fibres from [L1] (A relation RX×YR \subseteq X \times Y between finite sets, its row fibres RxR_x and its column fibres RyR^y, clauses (b) and (c), The cardinality A\lvert A\rvert of a finite set, clause (c)).

[L3]

{x}×Rx=Rx\lvert\{x\} \times R_x\rvert = \lvert R_x\rvert and Ry×{y}=Ry\lvert R^{y} \times \{y\}\rvert = \lvert R^{y}\rvert, by the slice bijections of clause (b) of A relation RX×YR \subseteq X \times Y between finite sets, its row fibres RxR_x and its column fibres RyR^y and the transport clause (c) of The cardinality A\lvert A\rvert of a finite set (Injection, surjection, bijection).

[L4]

The sum rule for a finite partition: if (Ci)iI(C_i)_{i \in I} is a family of pairwise disjoint finite sets indexed by a finite set II, then iICi\bigcup_{i \in I} C_i is finite with iICi=iICi\big\lvert\bigcup_{i \in I} C_i\big\rvert = \sum_{i \in I}\lvert C_i\rvert (The sum rule: a finite disjoint union is finite with AB=A+B\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert and iIAi=iIAi\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert, and a sum over a finite index set splits along a partition, clause 2, The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form).

Proof

technique · direct
1.1

The row slices form a family of pairwise disjoint finite sets indexed by the finite set XX, and their union is RR, so [L4] gives R=xX{x}×Rx\lvert R\rvert = \sum_{x \in X}\lvert \{x\} \times R_x\rvert.

L1L2L4
1.2

The column slices form a family of pairwise disjoint finite sets indexed by the finite set YY, and their union is RR, so [L4] gives R=yYRy×{y}\lvert R\rvert = \sum_{y \in Y}\lvert R^{y} \times \{y\}\rvert.

L1L2L4
2.1

Replacing each summand of step 1.1 by Rx\lvert R_x\rvert and each summand of step 1.2 by Ry\lvert R^{y}\rvert, which is legitimate by [L3] since the two lists have the same values at every index, gives xXRx=R=yYRy\sum_{x \in X}\lvert R_x\rvert = \lvert R\rvert = \sum_{y \in Y}\lvert R^{y}\rvert.

step 1.1step 1.2L3

Remarks

  • Where the hypotheses are spent. Finiteness of XX and of YY is what makes the two index sets legitimate index sets for a sum, and finiteness of RR is what makes R\lvert R\rvert defined. Disjointness of the slices is automatic, since a slice is determined by one coordinate of its points, which is why no hypothesis of that kind appears in the statement.

  • The count stays in N\mathbb{N}. Every quantity here is a cardinality, and the sums are the N\mathbb{N}-valued ones. Nothing is embedded into R\mathbb{R} until an identity with a subtraction or a division has to be written.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

If XX is nonempty, some row fibre is at least the average size and some row fibre is at most the average size

Statement

Let XX and YY be finite sets with XX \ne \varnothing, let RX×YR \subseteq X \times Y, and let RxR_x be its row fibres (A relation RX×YR \subseteq X \times Y between finite sets, its row fibres RxR_x and its column fibres RyR^y). Since X0\lvert X\rvert \ne 0, the real number

μ  :=  ι(R)ι(X)\mu \;:=\; \frac{\iota(\lvert R\rvert)}{\iota(\lvert X\rvert)}

is defined, where ι:NR\iota : \mathbb{N} \to \mathbb{R} is the canonical natural (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field). Then there are x+,xXx_{+}, x_{-} \in X with

ι(Rx+)  μandι(Rx)  μ.\iota(\lvert R_{x_{+}}\rvert) \ \ge\ \mu \qquad\text{and}\qquad \iota(\lvert R_{x_{-}}\rvert) \ \le\ \mu .

The two elements need not be distinct, and neither inequality need be an equality: μ\mu is a real number and a fibre size is a natural number, so no fibre need meet the average exactly.

Facts & Assumptions

Given: Finite sets XX \ne \varnothing and YY, a relation RX×YR \subseteq X \times Y with row fibres RxR_x, and a fixed enumeration φ:XX\varphi : \lvert X\rvert \to X of XX, which exists because XX is finite (The cardinality A\lvert A\rvert of a finite set).

[L2]

The bridge over a finite index set: for a finite SS and c:SNc : S \to \mathbb{N}, ι(iSci)=iSι(ci)\iota\big(\sum_{i \in S} c_i\big) = \sum_{i \in S}\iota(c_i). This is not a clause of The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form and is derived here: both sides are computed through one and the same enumeration ψ:SS\psi : \lvert S\rvert \to S, and ι(k<ncψ(k))=k<nι(cψ(k))\iota\big(\sum_{k<n} c_{\psi(k)}\big) = \sum_{k<n}\iota(c_{\psi(k)}) is clause 6 of Laws of finite sums and products in N\mathbb{N}, and ι(k<nak)=k<nι(ak)\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k).

[L3]

A constant real summand: iSλ=ι(S)λ\sum_{i \in S}\lambda = \iota(\lvert S\rvert)\,\lambda for λR\lambda \in \mathbb{R} (The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form, clause (c)).

[L4]

Additivity and the vanishing test over a finite index set: for u,v:SRu, v : S \to \mathbb{R} one has iS(ui+vi)=iSui+iSvi\sum_{i \in S}(u_i + v_i) = \sum_{i \in S}u_i + \sum_{i \in S}v_i; and if ui0u_i \ge 0 for every iSi \in S and iSui=0\sum_{i \in S}u_i = 0, then ui=0u_i = 0 for every iSi \in S. Both are clauses 1 and 4 of Laws of finite sums and finite products applied to the list kuψ(k)k \mapsto u_{\psi(k)} through an enumeration ψ\psi of SS (The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form, Finite sums and finite products, by recursion); for the second, ψ\psi is onto SS, so every value of uu is some uψ(k)u_{\psi(k)}.

[L6]

X=0\lvert X\rvert = 0 if and only if X=X = \varnothing (The cardinality A\lvert A\rvert of a finite set, clause (b)).

[L7]

R\mathbb{R} is an ordered field: its order is total, a nonzero element has a multiplicative inverse, and a<ba < b is equivalent to ba>0b - a > 0 (Ordered field, Field).

Proof

technique · contradiction
1.1

Since XX \ne \varnothing, [L6] gives X0\lvert X\rvert \ne 0, hence X1\lvert X\rvert \ge 1 and ι(X)>0\iota(\lvert X\rvert) > 0 by [L5]; in particular ι(X)0\iota(\lvert X\rvert) \ne 0, so μ=ι(R)/ι(X)\mu = \iota(\lvert R\rvert)/\iota(\lvert X\rvert) names a single real number and ι(X)μ=ι(R)\iota(\lvert X\rvert)\,\mu = \iota(\lvert R\rvert).

givenL5L6L7
1.2

Applying [L2] to the list xRxx \mapsto \lvert R_x\rvert and then [L1] gives xXι(Rx)=ι(xXRx)=ι(R)\sum_{x \in X}\iota(\lvert R_x\rvert) = \iota\big(\sum_{x \in X}\lvert R_x\rvert\big) = \iota(\lvert R\rvert).

L1L2
1.3

A positive list over a nonempty finite index set has nonzero sum: if w:XRw : X \to \mathbb{R} has wx>0w_x > 0 for every xXx \in X and xXwx=0\sum_{x \in X}w_x = 0, then wx0w_x \ge 0 for every xx, so [L4] forces wx=0w_x = 0 for every xXx \in X; as XX has an element, its value is then both 00 and positive, which is impossible.

assume-contraL4L7
2.1

By [L3] with the constant μ\mu, xXμ=ι(X)μ=ι(R)\sum_{x \in X}\mu = \iota(\lvert X\rvert)\,\mu = \iota(\lvert R\rvert), the second equality by step 1.1.

step 1.1L3
3.1

Suppose there were no x+x_{+} with ι(Rx+)μ\iota(\lvert R_{x_{+}}\rvert) \ge \mu. Since the order of R\mathbb{R} is total, ι(Rx)<μ\iota(\lvert R_x\rvert) < \mu for every xXx \in X, so wx:=μι(Rx)w_x := \mu - \iota(\lvert R_x\rvert) is positive for every xx; and by additivity, step 1.2 and step 2.1, xXwx+xXι(Rx)=xXμ\sum_{x \in X}w_x + \sum_{x \in X}\iota(\lvert R_x\rvert) = \sum_{x \in X}\mu, that is xXwx=ι(R)ι(R)=0\sum_{x \in X}w_x = \iota(\lvert R\rvert) - \iota(\lvert R\rvert) = 0, contradicting step 1.3. So some x+Xx_{+} \in X has ι(Rx+)μ\iota(\lvert R_{x_{+}}\rvert) \ge \mu.

step 1.2step 1.3step 2.1L4L7
3.2

Suppose there were no xx_{-} with ι(Rx)μ\iota(\lvert R_{x_{-}}\rvert) \le \mu. Then ι(Rx)>μ\iota(\lvert R_x\rvert) > \mu for every xXx \in X, so wx:=ι(Rx)μw_x := \iota(\lvert R_x\rvert) - \mu is positive for every xx; the same computation gives xXwx=ι(R)ι(R)=0\sum_{x \in X}w_x = \iota(\lvert R\rvert) - \iota(\lvert R\rvert) = 0, again contradicting step 1.3. So some xXx_{-} \in X has ι(Rx)μ\iota(\lvert R_{x_{-}}\rvert) \le \mu.

step 1.2step 1.3step 2.1L4L7
4.1

Steps 3.1 and 3.2 are the two assertions of the statement.

step 3.1step 3.2discharge-contradiction

Remarks

  • Why XX \ne \varnothing is a hypothesis and not decoration. It is used twice: to make ι(X)\iota(\lvert X\rvert) invertible, so that μ\mu exists at all, and to produce the element at which the vanishing test is contradicted. With X=X = \varnothing there is no fibre to exhibit and no quotient to compare it to.

  • The average lives in R\mathbb{R} and the fibre sizes live in N\mathbb{N}. A quotient of two natural numbers is not in general a natural number, so the comparison has to be made after both sides are carried into R\mathbb{R} by ι\iota. This is the reason the statement is written with ι\iota throughout rather than as RxR/X\lvert R_x\rvert \ge \lvert R\rvert/\lvert X\rvert, which is not an inequality between elements of one ordered set.

  • Nothing is claimed about attainment. The proof produces an x+x_{+} and an xx_{-} and no more; a relation whose fibre sizes all differ from μ\mu exists, and it is exhibited on the companion page.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

m/n\lceil m/n \rceil for naturals mm and n1n \ge 1: the least qNq \in \mathbb{N} with mnqm \le n q

Definition

Let m,nNm, n \in \mathbb{N} with n1n \ge 1 (The natural numbers N\mathbb{N} (von Neumann), Order on the natural numbers, On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n), and put

Q(m,n)  :=  {qN : mnq},Q(m,n) \;:=\; \{\, q \in \mathbb{N} \ :\ m \le n\,q \,\} ,

the multiplication being that of N\mathbb{N} (Multiplication of natural numbers).

Q(m,n)Q(m,n) is nonempty, so the definition below has something to pick from. Since n0n \ne 0, Every nonzero natural number is a successor gives n=σ(d)n = \sigma(d) for some dNd \in \mathbb{N}, and then nm=σ(d)m=dm+m=m+dmn \cdot m = \sigma(d)\cdot m = d\cdot m + m = m + d\cdot m by the successor-left law of Distributivity and the successor law for multiplication and the commutativity of addition (Addition is commutative), so mnmm \le n\cdot m by the definition of the order (Order on the natural numbers), which asks for a natural jj with m+j=nmm + j = n m and is met by j=dmj = d\cdot m. Hence mQ(m,n)m \in Q(m,n).

Definition. m/n\big\lceil m/n \big\rceil is the least element of Q(m,n)Q(m,n), which exists by the well-ordering principle (The well-ordering principle) applied to the nonempty subset Q(m,n)Q(m,n) of N\mathbb{N}. It is a natural number, and it is defined for n1n \ge 1 only.

Four clauses, recorded here because they are what the notation is used for.

(a) mnm/nm \le n\big\lceil m/n\big\rceil. This is membership of m/n\big\lceil m/n\big\rceil in Q(m,n)Q(m,n).

(b) Minimality. If qNq \in \mathbb{N} satisfies mnqm \le n q then m/nq\big\lceil m/n\big\rceil \le q; equivalently, every qq with q<m/nq < \big\lceil m/n\big\rceil satisfies nq<mn q < m, by trichotomy (Trichotomy of the order on N\mathbb{N}).

(c) Two values read off directly. 0/n=0\big\lceil 0/n\big\rceil = 0, since 0n00 \le n\cdot 0 makes 00 the least element of N\mathbb{N} that qualifies; and m/1=m\big\lceil m/1\big\rceil = m, since m1m=mm \le 1\cdot m = m while m1qm \le 1\cdot q forces mqm \le q (Zero and one under multiplication, Multiplication is commutative).

(d) The reading in R\mathbb{R}. With ι:NR\iota : \mathbb{N} \to \mathbb{R} the canonical natural (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field), clause (a) gives ι(m)ι(n)ι(m/n)\iota(m) \le \iota(n)\,\iota\big(\lceil m/n\rceil\big) by the multiplicativity of ι\iota (clause 0 of Laws of finite sums and products in N\mathbb{N}, and ι(k<nak)=k<nι(ak)\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k)) and its strict monotonicity (clause 7); and ι(n)>0\iota(n) > 0 because n1n \ge 1. Since R\mathbb{R} is an ordered field (Ordered field, Field), dividing by ι(n)\iota(n) gives

ι(m)ι(n)  ι(m/n).\frac{\iota(m)}{\iota(n)} \ \le\ \iota\Big(\big\lceil m/n\big\rceil\Big) .

Remarks

  • This is not a floor and it is not a ceiling function. It is defined for a pair of natural numbers with n1n \ge 1, its value is a natural number, and it is fixed by one order property and one minimality property. It is not defined for a real argument, it does not extend to negative numbers, and it carries no division: the symbol m/nm/n inside the brackets is part of the notation and not an operation performed anywhere above.

  • Why it is introduced at all. The strong form of the pigeonhole principle says that some fibre has at least "the average, rounded up" elements, and that phrase needs a name for the rounding. The least qq with mnqm \le nq is exactly what the proof produces, and the well-ordering principle is exactly what makes it exist, so nothing stronger is required.

  • Nothing among this page's declared prerequisites supplies a division with remainder, and the definition above deliberately does not attempt one: no rr with m=nq+rm = nq + r and r<nr < n is produced or claimed here.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

If A>kB\lvert A\rvert > k\lvert B\rvert then every f:ABf : A \to B has a fibre with more than kk elements, and for nonempty BB some fibre has at least A/B\lceil \lvert A\rvert / \lvert B\rvert\rceil elements

Statement

Let AA and BB be finite sets, let kNk \in \mathbb{N}, let f:ABf : A \to B, and for bBb \in B write

f1[{b}]  :=  {aA : f(a)=b}f^{-1}[\{b\}] \;:=\; \{\, a \in A \ :\ f(a) = b \,\}

for the fibre of ff over bb (Injection, surjection, bijection). Then:

  1. The counting form. If A>kB\lvert A\rvert > k\,\lvert B\rvert then there is bBb \in B with f1[{b}]>k\lvert f^{-1}[\{b\}]\rvert > k.
  2. The ceiling form. If BB \ne \varnothing then there is bBb \in B with f1[{b}]A/B\lvert f^{-1}[\{b\}]\rvert \ge \big\lceil \lvert A\rvert/\lvert B\rvert\big\rceil (m/n\lceil m/n \rceil for naturals mm and n1n \ge 1: the least qNq \in \mathbb{N} with mnqm \le n q, which is defined because B1\lvert B\rvert \ge 1).

Every quantity here is a natural number and the comparisons are those of N\mathbb{N} (Order on the natural numbers). Clause 1 at k=0k = 0 says that a nonempty AA has a nonempty fibre. Clause 1 is vacuous when B=B = \varnothing, since then kB=0k\,\lvert B\rvert = 0, the hypothesis says AA \ne \varnothing, and there is no function from a nonempty set to \varnothing for the conclusion to be about. Clause 2 at A=A = \varnothing says only that some fibre has at least 00 elements, since 0/B=0\lceil 0/\lvert B\rvert\rceil = 0.

Facts & Assumptions

Given: Finite sets AA and BB, a natural number kk, a function f:ABf : A \to B, and the fibres f1[{b}]f^{-1}[\{b\}] for bBb \in B.

[L2]

Monotonicity over a finite index set: if c,d:SNc, d : S \to \mathbb{N} satisfy cidic_i \le d_i for every iSi \in S, then iSciiSdi\sum_{i \in S}c_i \le \sum_{i \in S}d_i. Both sums are computed through one enumeration ψ:SS\psi : \lvert S\rvert \to S (The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form), and cψ(j)dψ(j)c_{\psi(j)} \le d_{\psi(j)} for every j<Sj < \lvert S\rvert, so clause 4 of Laws of finite sums and products in N\mathbb{N}, and ι(k<nak)=k<nι(ak)\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k) applies (Finite sums and finite products, by recursion).

[L3]

A constant natural summand: iSk=Sk\sum_{i \in S}k = \lvert S\rvert\cdot k (The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form, clause (c)).

[L4]

Order and arithmetic of N\mathbb{N}: multiplication is commutative (Multiplication is commutative); exactly one of p<qp < q, p=qp = q, q<pq < p holds (Trichotomy of the order on N\mathbb{N}); p<qp < q if and only if σ(p)q\sigma(p) \le q (Discreteness: σ(n)\sigma(n) is the immediate successor); every nonzero natural is a successor (Every nonzero natural number is a successor); and 0p0 \le p for every pp (Order on the natural numbers).

[L5]

The ceiling (m/n\lceil m/n \rceil for naturals mm and n1n \ge 1: the least qNq \in \mathbb{N} with mnqm \le n q): for n1n \ge 1, m/n\lceil m/n\rceil is the least qNq \in \mathbb{N} with mnqm \le nq, so any q<m/nq < \lceil m/n\rceil satisfies nq<mnq < m.

[L6]

B=0\lvert B\rvert = 0 if and only if B=B = \varnothing (The cardinality A\lvert A\rvert of a finite set, clause (b)).

Proof

technique · contradiction
1.1

Suppose, for contradiction, that A>kB\lvert A\rvert > k\,\lvert B\rvert and yet f1[{b}]k\lvert f^{-1}[\{b\}]\rvert \le k for every bBb \in B.

assume-contra
1.2

By [L1], A=bBf1[{b}]\lvert A\rvert = \sum_{b \in B}\lvert f^{-1}[\{b\}]\rvert.

L1
1.3

For clause 2, assume BB \ne \varnothing; then B0\lvert B\rvert \ne 0 by [L6], so B1\lvert B\rvert \ge 1 and c:=A/Bc := \big\lceil\lvert A\rvert/\lvert B\rvert\big\rceil is defined, and BB has at least one element.

L4L5L6
2.1

Clause 1. Under the assumption of step 1.1, monotonicity and the constant sum give A=bBf1[{b}]bBk=Bk=kB\lvert A\rvert = \sum_{b \in B}\lvert f^{-1}[\{b\}]\rvert \le \sum_{b \in B}k = \lvert B\rvert\cdot k = k\,\lvert B\rvert, which contradicts A>kB\lvert A\rvert > k\,\lvert B\rvert by trichotomy. So the supposition of step 1.1 is untenable and clause 1 holds.

step 1.1step 1.2L2L3L4
2.2

Clause 2 when c=0c = 0. Choose any bBb \in B, available by step 1.3; then f1[{b}]0=c\lvert f^{-1}[\{b\}]\rvert \ge 0 = c by [L4].

step 1.3L4
3.1

Clause 2 when c0c \ne 0. Write c=σ(q)c = \sigma(q) by [L4]. Then q<cq < c, so [L5] gives Bq<A\lvert B\rvert\, q < \lvert A\rvert, that is A>qB\lvert A\rvert > q\,\lvert B\rvert by commutativity; clause 1, established in step 2.1, therefore produces bBb \in B with f1[{b}]>q\lvert f^{-1}[\{b\}]\rvert > q, and f1[{b}]σ(q)=c\lvert f^{-1}[\{b\}]\rvert \ge \sigma(q) = c by [L4].

step 1.3step 2.1L4L5
4.1

Clause 1 is step 2.1, and clause 2 is steps 2.2 and 3.1, whose two cases are exhaustive.

step 2.1step 2.2step 3.1discharge-contradiction

Remarks

  • Where the ceiling earns its keep. Clause 2 is not a separate argument: it is clause 1 applied at the single value qq with σ(q)=c\sigma(q) = c, and the only thing that has to be checked is that this qq satisfies A>qB\lvert A\rvert > q\lvert B\rvert, which is exactly the minimality of cc. That is the whole reason the ceiling was defined by minimality rather than by a division.

  • The case c=0c = 0 is not a degenerate nuisance. It occurs precisely when A=A = \varnothing, where the conclusion is empty of content but still needs an element of BB to be stated about, and that is where BB \ne \varnothing is spent in clause 2.

  • Disjointness of the fibres is free, since a fibre is determined by the value it lies over. This is what lets the sum rule be applied with no hypothesis beyond finiteness, in contrast to a union of arbitrary sets.

DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

A finite family (Ai)iI(A_i)_{i \in I} of subsets of a finite set XX, the intersections AJA_J for JIJ \subseteq I, and the convention A=XA_\varnothing = X

Definition

A sieve family consists of a finite set XX, called the ambient set, a finite set II, called the index set, and a family (Ai)iI(A_i)_{i \in I} of subsets of XX, that is a function IP(X)I \to \mathcal{P}(X) (Finite, countably infinite, countable, uncountable, The cardinality A\lvert A\rvert of a finite set). For JIJ \subseteq I set

AJ  :=  {iJAi,J,X,J=,A_J \;:=\; \begin{cases} \displaystyle\bigcap_{i \in J} A_i, & J \ne \varnothing,\\[4pt] X, & J = \varnothing,\end{cases}

and write U:=iIAiU := \bigcup_{i \in I} A_i for the union of the family.

Why the ambient set has to be named, and why A:=XA_\varnothing := X is a stipulation. For JJ \ne \varnothing the intersection iJAi\bigcap_{i \in J}A_i is the set of elements belonging to every AiA_i with iJi \in J, and it is determined by the family alone. For J=J = \varnothing that description is satisfied by every set whatsoever, so it determines nothing; an intersection of no subsets of XX is XX only relative to XX. Naming XX as part of the data and stipulating A=XA_\varnothing = X is what makes the symbol AJA_J defined for all JIJ \subseteq I, which is what the complementary form of the sieve identity requires.

(a) Every AJA_J is a finite subset of XX. For JJ \ne \varnothing pick iJi \in J; then AJAiXA_J \subseteq A_i \subseteq X. For J=J = \varnothing, AJ=XA_J = X. In both cases AJXA_J \subseteq X is finite by clause 1 of A subset of a finite set is finite, with BA\lvert B\rvert \le \lvert A\rvert, and equality holds if and only if B=AB = A, and so is UXU \subseteq X; hence AJ\lvert A_J\rvert and U\lvert U\rvert are natural numbers (The cardinality A\lvert A\rvert of a finite set).

(b) The index sets of the sieve's sums are finite. P(I)\mathcal{P}(I) is finite with P(I)=2I\lvert\mathcal{P}(I)\rvert = 2^{\lvert I\rvert} (P(A)=2A\lvert\mathcal{P}(A)\rvert = 2^{\lvert A\rvert} for finite AA); the set P(I){}\mathcal{P}(I) \setminus \{\varnothing\} of nonempty subsets of II and the set [I]j[I]^{j} of jj-element subsets of II are subsets of P(I)\mathcal{P}(I), hence finite (A subset of a finite set is finite, with BA\lvert B\rvert \le \lvert A\rvert, and equality holds if and only if B=AB = A), and [I]j=(Ij)\lvert [I]^{j}\rvert = \binom{\lvert I\rvert}{j} (The set [A]k[A]^{k} of kk-element subsets and the binomial coefficient (nk):=[n]k\binom{n}{k} := \lvert [n]^{k}\rvert).

(c) Monotonicity. If JJIJ \subseteq J' \subseteq I then AJAJA_{J'} \subseteq A_J. For J=J = \varnothing this is clause (a); otherwise an element lying in every AiA_i with iJi \in J' lies in every AiA_i with iJi \in J.

(d) The trace of a point. For xXx \in X put

T(x)  :=  {iI : xAi}I,T(x) \;:=\; \{\, i \in I \ :\ x \in A_i \,\} \subseteq I ,

a finite set. For every nonempty JIJ \subseteq I,

xAJ    JT(x),x \in A_J \iff J \subseteq T(x) ,

both sides saying that xAix \in A_i for every iJi \in J. And xUx \in U if and only if T(x)T(x) \ne \varnothing. Writing t(x):=T(x)t(x) := \lvert T(x)\rvert, clause (b) applied to T(x)T(x) gives [T(x)]j=(t(x)j)\lvert [T(x)]^{j}\rvert = \binom{t(x)}{j}, and for nonempty JJ the condition xAJx \in A_J with J=j\lvert J\rvert = j says exactly that J[T(x)]jJ \in [T(x)]^{j}.

XA0A1A2xx2Af0;2g;T(x)=f0;2g.

Remarks

  • The counts stay in N\mathbb{N}; the identities do not. Each AJ\lvert A_J\rvert is a natural number. Every identity that sieves them carries a minus sign, and N\mathbb{N} has no subtraction, so those identities are stated in R\mathbb{R} through the canonical natural and read back by its injectivity. That is a property of the identities, not of this definition, which introduces no arithmetic at all.

  • II is an arbitrary finite index set, not a natural number. Nothing below numbers the sets A0,A1,A_0, A_1, \dots; the subsets JIJ \subseteq I are the objects the sums run over, and J\lvert J\rvert rather than any position is what carries the sign.

  • The clause A=XA_\varnothing = X supplies every empty-subfamily term. In the complementary form at J=J = \varnothing it contributes X\lvert X\rvert; later sieve instances also use it when identifying the intersection at the empty subfamily. Removing the stipulation would leave those terms undefined.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-07-29 (claude-fable-5)Open item page →

Inclusion and exclusion: ιiIAi=JI(1)J+1ιAJ\iota\lvert\bigcup_{i \in I} A_i\rvert = \sum_{\varnothing \ne J \subseteq I}(-1)^{\lvert J\rvert + 1}\,\iota\lvert A_J\rvert, together with the complementary form counting the elements in none of the AiA_i

Statement

Let XX, II, (Ai)iI(A_i)_{i \in I} and the intersections AJA_J be a sieve family (A finite family (Ai)iI(A_i)_{i \in I} of subsets of a finite set XX, the intersections AJA_J for JIJ \subseteq I, and the convention A=XA_\varnothing = X), let U:=iIAiU := \bigcup_{i \in I}A_i, and let ι:NR\iota : \mathbb{N} \to \mathbb{R} be the canonical natural (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field). Then, in R\mathbb{R}:

  1. The sieve identity. ιU  =  JP(I){}(1)J+1ιAJ,\iota\lvert U\rvert \;=\; \sum_{J \in \mathcal{P}(I)\setminus\{\varnothing\}} (-1)^{\lvert J\rvert + 1}\,\iota\lvert A_J\rvert , the sum being over the finite index set of nonempty subsets of II.
  2. The complementary form. ιXU  =  JP(I)(1)JιAJ,\iota\lvert X \setminus U\rvert \;=\; \sum_{J \in \mathcal{P}(I)} (-1)^{\lvert J\rvert}\,\iota\lvert A_J\rvert , the sum now being over all subsets of II, its term at J=J = \varnothing being ιX\iota\lvert X\rvert by the stipulation A=XA_\varnothing = X.

The identities are stated in R\mathbb{R} because their terms carry signs and N\mathbb{N} has no subtraction; every cardinality appearing is a natural number carried into R\mathbb{R} by ι\iota, and ι\iota is injective, so an identity between two of them may be read back in N\mathbb{N} (Laws of finite sums and products in N\mathbb{N}, and ι(k<nak)=k<nι(ak)\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k), clause 7).

Both readings at I=I = \varnothing are part of the statement. Then U=U = \varnothing and clause 1 reads 0=00 = 0, the index set of its sum being empty. Clause 2 reads ιX=ιA\iota\lvert X\rvert = \iota\lvert A_\varnothing\rvert, its sum having the single term at J=J = \varnothing. At J=1\lvert J\rvert = 1 the sign in clause 1 is (1)2=1(-1)^{2} = 1 and A{i}=AiA_{\{i\}} = A_i, so the singleton terms enter with a plus sign.

Facts & Assumptions

Given: A sieve family XX, II, (Ai)iI(A_i)_{i \in I} with intersections AJA_J, union UU, traces T(x)T(x) and t(x):=T(x)t(x) := \lvert T(x)\rvert, all as in A finite family (Ai)iI(A_i)_{i \in I} of subsets of a finite set XX, the intersections AJA_J for JIJ \subseteq I, and the convention A=XA_\varnothing = X; the abbreviation J:=P(I){}\mathcal{J} := \mathcal{P}(I)\setminus\{\varnothing\}; and, for VXV \subseteq X, the indicator 1V:XR\mathbf{1}_V : X \to \mathbb{R} with 1V(x)=1\mathbf{1}_V(x) = 1 for xVx \in V and 1V(x)=0\mathbf{1}_V(x) = 0 otherwise.

[L3]

Sums over a finite index set (The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form): the value is independent of the enumeration used; inai=i<nai\sum_{i \in n}a_i = \sum_{i<n}a_i (clause (a)); a sum over \varnothing is 00 and a constant real summand gives iSλ=ι(S)λ\sum_{i \in S}\lambda = \iota(\lvert S\rvert)\,\lambda (clause (c)).

[L5]

Additivity and scaling of a real finite sum over a finite index set: iS(ui+vi)=iSui+iSvi\sum_{i \in S}(u_i + v_i) = \sum_{i \in S}u_i + \sum_{i \in S}v_i and iSλui=λiSui\sum_{i \in S}\lambda u_i = \lambda\sum_{i \in S}u_i. Both are clauses 1 and 2 of Laws of finite sums and finite products read through an enumeration of SS (The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form, Finite sums and finite products, by recursion).

[L6]

Partition of a power set by cardinality: for a finite SS with N:=SN := \lvert S\rvert, the sets [S]j[S]^{j} for jσ(N)j \in \sigma(N) are pairwise disjoint with union P(S)\mathcal{P}(S), since a subset of SS has exactly one cardinality and that cardinality is at most NN (A subset of a finite set is finite, with BA\lvert B\rvert \le \lvert A\rvert, and equality holds if and only if B=AB = A, clause 2).

[L7]

Powers of 1-1 and the alternating row sum: (1)0=1(-1)^{0} = 1 and (1)p+1=(1)p(-1)^{p+1} = -(-1)^{p} (Integer powers ama^m); and j<t+1(1)jι(tj)=0\sum_{j<t+1}(-1)^{j}\,\iota\binom{t}{j} = 0 for every t1t \ge 1 (k<n+1(nk)=2n\sum_{k<n+1}\binom{n}{k} = 2^{n}, and k<n+1(1)kι ⁣(nk)=0\sum_{k<n+1}(-1)^{k}\iota\!\binom{n}{k} = 0 for n1n \ge 1, clause 2). The hypothesis t1t \ge 1 there is not decoration: at t=0t = 0 that sum is 11.

[L8]

ι\iota is additive and injective (Laws of finite sums and products in N\mathbb{N}, and ι(k<nak)=k<nι(ak)\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k), clauses 0 and 7), and R\mathbb{R} is an ordered field, so subtraction is available (Ordered field, Field).

Proof

technique · direct
1.1

Indicator sums. For every VXV \subseteq X one has xX1V(x)=ιV\sum_{x \in X}\mathbf{1}_V(x) = \iota\lvert V\rvert: the sets VV and XVX \setminus V are disjoint finite sets with union XX, so [L2] splits the sum into xV1+xXV0\sum_{x \in V}1 + \sum_{x \in X\setminus V}0, which is ιV1+ιXV0=ιV\iota\lvert V\rvert\cdot 1 + \iota\lvert X\setminus V\rvert\cdot 0 = \iota\lvert V\rvert by the constant clause of [L3].

L1L2L3construct
1.2

The double list. Define h:J×XRh : \mathcal{J} \times X \to \mathbb{R} by h(J,x):=(1)J+11AJ(x)h(J,x) := (-1)^{\lvert J\rvert + 1}\,\mathbf{1}_{A_J}(x); both J\mathcal{J} and XX are finite by [L1], so both iterated sums of hh are defined.

L1construct
1.3

Fix xXx \in X and write t:=t(x)t := t(x). The sets J1:={JJ:JT(x)}\mathcal{J}_1 := \{\,J \in \mathcal{J} : J \subseteq T(x)\,\} and JJ1\mathcal{J}\setminus\mathcal{J}_1 are disjoint with union J\mathcal{J}; by [L1] we have 1AJ(x)=1\mathbf{1}_{A_J}(x) = 1 for JJ1J \in \mathcal{J}_1 and 1AJ(x)=0\mathbf{1}_{A_J}(x) = 0 for JJJ1J \in \mathcal{J}\setminus\mathcal{J}_1, so splitting by [L2] gives JJh(J,x)=JJ1(1)J+1\sum_{J \in \mathcal{J}}h(J,x) = \sum_{J \in \mathcal{J}_1}(-1)^{\lvert J\rvert + 1}, and J1=P(T(x)){}\mathcal{J}_1 = \mathcal{P}(T(x))\setminus\{\varnothing\}.

L1L2L3
1.4

Grouping the subsets of T(x)T(x) by size. By [L6] applied to T(x)T(x), then the constant clause of [L3] on each block, then scaling by 1-1 and (1)j+1=(1)j(-1)^{j+1} = -(-1)^{j} from [L7], JP(T(x))(1)J+1=j<t+1(J[T(x)]j(1)j+1)=j<t+1ι(tj)(1)j+1=j<t+1(1)jι(tj).\sum_{J \in \mathcal{P}(T(x))}(-1)^{\lvert J\rvert + 1} = \sum_{j<t+1}\Big(\sum_{J \in [T(x)]^{j}}(-1)^{j+1}\Big) = \sum_{j<t+1}\iota\binom{t}{j}\,(-1)^{j+1} = -\sum_{j<t+1}(-1)^{j}\,\iota\binom{t}{j}.

L1L2L3L5L6L7
1.5

Splitting off the empty subset. {}\{\varnothing\} and P(T(x)){}\mathcal{P}(T(x))\setminus\{\varnothing\} are disjoint with union P(T(x))\mathcal{P}(T(x)), so [L2] and [L7] give JP(T(x))(1)J+1=(1)0+1+JP(T(x)){}(1)J+1=1+JP(T(x)){}(1)J+1\sum_{J \in \mathcal{P}(T(x))}(-1)^{\lvert J\rvert + 1} = (-1)^{0+1} + \sum_{J \in \mathcal{P}(T(x))\setminus\{\varnothing\}}(-1)^{\lvert J\rvert + 1} = -1 + \sum_{J \in \mathcal{P}(T(x))\setminus\{\varnothing\}}(-1)^{\lvert J\rvert + 1}.

L2L3L7
2.1

The inner sum is the indicator of UU. If t1t \ge 1 then [L7] makes the right-hand side of step 1.4 zero, so step 1.5 gives JP(T(x)){}(1)J+1=1\sum_{J \in \mathcal{P}(T(x))\setminus\{\varnothing\}}(-1)^{\lvert J\rvert + 1} = 1. If t=0t = 0 then T(x)=T(x) = \varnothing, so P(T(x)){}=\mathcal{P}(T(x))\setminus\{\varnothing\} = \varnothing and that sum is 00 by [L3]. Since xUx \in U exactly when t1t \ge 1 by [L1], step 1.3 gives JJh(J,x)=1U(x)\sum_{J \in \mathcal{J}}h(J,x) = \mathbf{1}_U(x) for every xXx \in X.

step 1.3step 1.4step 1.5L1L3L7
2.2

The outer sum recovers the sieve terms. Scaling by the constant (1)J+1(-1)^{\lvert J\rvert+1} and applying step 1.1 to V=AJV = A_J gives xXh(J,x)=(1)J+1ιAJ\sum_{x \in X}h(J,x) = (-1)^{\lvert J\rvert + 1}\,\iota\lvert A_J\rvert for every JJJ \in \mathcal{J}.

step 1.1L5
3.1

Clause 1. Summing step 2.2 over J\mathcal{J}, interchanging by [L4], and then using step 2.1 and step 1.1 with V=UV = U: JJ(1)J+1ιAJ=JJxXh(J,x)=xXJJh(J,x)=xX1U(x)=ιU.\sum_{J \in \mathcal{J}}(-1)^{\lvert J\rvert + 1}\iota\lvert A_J\rvert = \sum_{J \in \mathcal{J}}\sum_{x \in X}h(J,x) = \sum_{x \in X}\sum_{J \in \mathcal{J}}h(J,x) = \sum_{x \in X}\mathbf{1}_U(x) = \iota\lvert U\rvert .

step 1.1step 2.1step 2.2L4
4.1

Clause 2. The sets UU and XUX \setminus U are disjoint finite sets with union XX, so X=U+XU\lvert X\rvert = \lvert U\rvert + \lvert X\setminus U\rvert by [L2] and hence ιXU=ιXιU\iota\lvert X\setminus U\rvert = \iota\lvert X\rvert - \iota\lvert U\rvert by the additivity of ι\iota in [L8]. On the other side, {}\{\varnothing\} and J\mathcal{J} are disjoint with union P(I)\mathcal{P}(I), so [L2], [L3] and [L7] give JP(I)(1)JιAJ=ιA+JJ(1)JιAJ=ιXJJ(1)J+1ιAJ\sum_{J \in \mathcal{P}(I)}(-1)^{\lvert J\rvert}\iota\lvert A_J\rvert = \iota\lvert A_\varnothing\rvert + \sum_{J \in \mathcal{J}}(-1)^{\lvert J\rvert}\iota\lvert A_J\rvert = \iota\lvert X\rvert - \sum_{J \in \mathcal{J}}(-1)^{\lvert J\rvert+1}\iota\lvert A_J\rvert, which by step 3.1 is ιXιU\iota\lvert X\rvert - \iota\lvert U\rvert. The two right-hand sides agree, which is clause 2.

step 3.1L2L3L5L7L8

Remarks

  • Where the alternating row sum is spent, and why its hypothesis matters. The whole content of the proof is that each xx contributes 11 to the right-hand side when it lies in some AiA_i and 00 otherwise. The first case is the vanishing of the full alternating row sum of t(x)t(x), which holds only for t(x)1t(x) \ge 1; the second case is not that identity at all but the emptiness of the index set. Applying the identity at t(x)=0t(x) = 0 would give 11, not 00, and would make the theorem false.

  • The empty intersection is used once. Only in clause 2, at the term J=J = \varnothing, where A=XA_\varnothing = X contributes ιX\iota\lvert X\rvert. Clause 1 never mentions it.

  • No choice principle is used. A sum over a finite index set is defined because all its enumerations agree, not by selecting one, and the family (Ai)iI(A_i)_{i \in I} is given as a function.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

j<m+1(1)jι(tj)=(1)mι(t1m)\sum_{j<m+1}(-1)^{j}\,\iota\binom{t}{j} = (-1)^{m}\,\iota\binom{t-1}{m} for every t1t \ge 1 and every mm

Statement

Let tNt \in \mathbb{N} with t1t \ge 1 and let mNm \in \mathbb{N}. Then, in R\mathbb{R},

j<m+1(1)jι(tj)  =  (1)mι(t1m),\sum_{j<m+1}(-1)^{j}\,\iota\binom{t}{j} \;=\; (-1)^{m}\,\iota\binom{t-1}{m},

where ι\iota is the canonical natural (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field), the binomial coefficients are the counts of The set [A]k[A]^{k} of kk-element subsets and the binomial coefficient (nk):=[n]k\binom{n}{k} := \lvert [n]^{k}\rvert, and t1t-1 is the truncated difference of Finite sums and finite products of natural numbers, k<nak\sum_{k<n} a_k and k<nak\prod_{k<n} a_k in N\mathbb{N}, which for t1t \ge 1 is the ordinary one, so that (t1)+1=t(t-1) + 1 = t.

The hypothesis t1t \ge 1 is part of the statement. At t=0t = 0 and m=1m = 1 the left-hand side is ι(00)ι(01)=1\iota\binom{0}{0} - \iota\binom{0}{1} = 1, while the truncated difference gives t1=0t - 1 = 0 and the right-hand side is ι(01)=0-\iota\binom{0}{1} = 0.

Two readings worth recording. At m=0m = 0 both sides are 11, since (t0)=(t10)=1\binom{t}{0} = \binom{t-1}{0} = 1. For mtm \ge t both sides are 00: the terms of the left-hand side with j>tj > t vanish and the remaining sum is the full alternating row sum of tt, which vanishes because t1t \ge 1, while (t1m)=0\binom{t-1}{m} = 0 because m>t1m > t-1.

Facts & Assumptions

Given: Naturals t1t \ge 1 and mm; the abbreviation s:=t1s := t-1, so that s+1=ts+1 = t (Finite sums and finite products of natural numbers, k<nak\sum_{k<n} a_k and k<nak\prod_{k<n} a_k in N\mathbb{N}, Order on the natural numbers); the real finite sum of Finite sums and finite products, by recursion; and integer powers (Integer powers ama^m) in the ordered field R\mathbb{R} (Ordered field, Field).

[L1]

Induction: a property holding at 00 and inherited by successors holds at every natural (The principle of mathematical induction).

[L2]

Recursion clauses of the real finite sum: j<0uj=0\sum_{j<0}u_j = 0 and j<p+1uj=j<puj+up\sum_{j<p+1}u_j = \sum_{j<p}u_j + u_p (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L3]

Pascal's rule, with no restriction relating the two indices: (n+1k+1)=(nk)+(nk+1)\binom{n+1}{k+1} = \binom{n}{k} + \binom{n}{k+1} for all n,kNn, k \in \mathbb{N} (Pascal's rule (n+1k+1)=(nk)+(nk+1)\binom{n+1}{k+1} = \binom{n}{k} + \binom{n}{k+1}, and the hockey-stick identity in(ik)=(n+1k+1)\sum_{i \le n}\binom{i}{k} = \binom{n+1}{k+1}, clause 1).

[L5]

Powers of 1-1: (1)0=1(-1)^{0} = 1 and (1)p+1=(1)p(1)=(1)p(-1)^{p+1} = (-1)^{p}\cdot(-1) = -(-1)^{p} (Integer powers ama^m).

Proof

technique · induction
1.1

Fix t1t \ge 1 and write s:=t1s := t-1, so that s+1=ts+1 = t; the claim is proved by induction on mm, for this fixed tt.

given
1.2

Base case m=0m = 0. By [L2] the left-hand side is the single term (1)0ι(t0)(-1)^{0}\iota\binom{t}{0}, which is 11 by [L4] and [L5]; and the right-hand side is (1)0ι(s0)=1(-1)^{0}\iota\binom{s}{0} = 1 for the same reason.

baseL2L4L5
1.3

Inductive hypothesis: fix mm and assume j<m+1(1)jι(tj)=(1)mι(sm)\sum_{j<m+1}(-1)^{j}\iota\binom{t}{j} = (-1)^{m}\iota\binom{s}{m}.

ih
1.4

Pascal's rule at n=sn = s and k=mk = m, together with s+1=ts+1 = t, gives (tm+1)=(sm)+(sm+1)\binom{t}{m+1} = \binom{s}{m} + \binom{s}{m+1}, hence ι(tm+1)=ι(sm)+ι(sm+1)\iota\binom{t}{m+1} = \iota\binom{s}{m} + \iota\binom{s}{m+1} by the additivity of ι\iota.

L3L4
2.1

By the recursion clause of [L2] and the hypothesis of step 1.3, j<m+2(1)jι(tj)=(1)mι(sm)+(1)m+1ι(tm+1)\sum_{j<m+2}(-1)^{j}\iota\binom{t}{j} = (-1)^{m}\iota\binom{s}{m} + (-1)^{m+1}\iota\binom{t}{m+1}.

step 1.3L2
3.1

Substituting step 1.4 into step 2.1 and using (1)m+1=(1)m(-1)^{m+1} = -(-1)^{m} from [L5]: (1)mι(sm)+(1)m+1(ι(sm)+ι(sm+1))=(1)mι(sm)(1)mι(sm)+(1)m+1ι(sm+1)=(1)m+1ι(sm+1)(-1)^{m}\iota\binom{s}{m} + (-1)^{m+1}\big(\iota\binom{s}{m} + \iota\binom{s}{m+1}\big) = (-1)^{m}\iota\binom{s}{m} - (-1)^{m}\iota\binom{s}{m} + (-1)^{m+1}\iota\binom{s}{m+1} = (-1)^{m+1}\iota\binom{s}{m+1}.

step 1.4step 2.1L5algebra
4.1

So the claim holds at m+1m+1 whenever it holds at mm, and it holds at m=0m = 0; by [L1] it holds for every mNm \in \mathbb{N}, for the fixed t1t \ge 1, which was arbitrary.

step 1.2step 1.3step 3.1L1discharge-induction

Remarks

  • Where t1t \ge 1 is spent. In exactly one place: the identity s+1=ts+1 = t, which is what lets Pascal's rule be applied with upper index s+1s+1. Under the truncated difference the equation s+1=ts+1 = t fails at t=0t = 0, where s=0s = 0 and s+1=1s+1 = 1, and the statement fails there too.

  • Why not the full alternating row sum. The published corollary of the binomial theorem gives the sum over the whole row, and only for t1t \ge 1. A truncation of that row is a different quantity, and the identity above is what says how far a truncation misses: by exactly one binomial coefficient of the row above, with the sign of the last term kept.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

Truncating the sieve at an odd depth over-estimates the size of the union and truncating it at an even depth under-estimates it

Statement

Let XX, II, (Ai)iI(A_i)_{i \in I} and the intersections AJA_J be a sieve family (A finite family (Ai)iI(A_i)_{i \in I} of subsets of a finite set XX, the intersections AJA_J for JIJ \subseteq I, and the convention A=XA_\varnothing = X), let U:=iIAiU := \bigcup_{i \in I}A_i, put N:=IN := \lvert I\rvert, and let ι\iota be the canonical natural (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field). For jNj \in \mathbb{N} and mNm \in \mathbb{N} set

Sj  :=  J[I]jιAJ,Tm  :=  i<m(1)iSi+1,S_j \;:=\; \sum_{J \in [I]^{j}} \iota\lvert A_J\rvert, \qquad T_m \;:=\; \sum_{i<m}(-1)^{i}\,S_{i+1},

the first sum being over the finite set of jj-element subsets of II and the second the real finite sum of Finite sums and finite products, by recursion. Thus T0=0T_0 = 0, T1=S1T_1 = S_1 and T2=S1S2T_2 = S_1 - S_2. Then, in R\mathbb{R}:

  1. Odd truncation over-estimates. ιUT2r+1\iota\lvert U\rvert \le T_{2r+1} for every rNr \in \mathbb{N}.
  2. Even truncation under-estimates. ιUT2r\iota\lvert U\rvert \ge T_{2r} for every rNr \in \mathbb{N}.
  3. Both are equalities once the truncation reaches I\lvert I\rvert. Tm=ιUT_m = \iota\lvert U\rvert for every mNm \ge N.

Clause 1 at r=0r = 0 is the union bound ιUS1\iota\lvert U\rvert \le S_1, and clause 2 at r=0r = 0 is the trivial ιUT0=0\iota\lvert U\rvert \ge T_0 = 0; the first substantial even case is r=1r = 1, where T2=S1S2T_2 = S_1 - S_2.

Facts & Assumptions

Given: A sieve family XX, II, (Ai)iI(A_i)_{i \in I} with intersections AJA_J, union UU, traces T(x)T(x) and t(x):=T(x)t(x) := \lvert T(x)\rvert (A finite family (Ai)iI(A_i)_{i \in I} of subsets of a finite set XX, the intersections AJA_J for JIJ \subseteq I, and the convention A=XA_\varnothing = X); N:=IN := \lvert I\rvert; the quantities SjS_j and TmT_m of the Statement; and, for VXV \subseteq X, the indicator 1V:XR\mathbf{1}_V : X \to \mathbb{R} with value 11 on VV and 00 off it.

[L5]

Real finite-sum laws, read over a finite index set through an enumeration (The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form): additivity, scaling, splitting at an index and monotonicity (Laws of finite sums and finite products, clauses 1 to 4, Finite sums and finite products, by recursion).

[L6]

The partial alternating row sum: j<M+1(1)jι(tj)=(1)Mι(t1M)\sum_{j<M+1}(-1)^{j}\iota\binom{t}{j} = (-1)^{M}\iota\binom{t-1}{M} for every t1t \ge 1 and every MM (j<m+1(1)jι(tj)=(1)mι(t1m)\sum_{j<m+1}(-1)^{j}\,\iota\binom{t}{j} = (-1)^{m}\,\iota\binom{t-1}{m} for every t1t \ge 1 and every mm).

[L7]

Powers of 1-1: (1)0=1(-1)^{0} = 1 and (1)p+1=(1)p(-1)^{p+1} = -(-1)^{p} (Integer powers ama^m); and (1)2r=1(-1)^{2r} = 1, (1)2r+1=1(-1)^{2r+1} = -1. For the last two, (1)2r=((1)2)r=1r(-1)^{2r} = \big((-1)^{2}\big)^{r} = 1^{r} by clause 1 of Laws of integer exponents, and 1r=ι(1)r=ι(1r)=ι(1)=11^{r} = \iota(1)^{r} = \iota(1^{r}) = \iota(1) = 1 by clauses (b) and (d) of Exponentiation of natural numbers, mnm^{n}, and its agreement with the integer power in R\mathbb{R} with The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field; then (1)2r+1=(1)2r(1)=1(-1)^{2r+1} = (-1)^{2r}\cdot(-1) = -1.

[L9]

Boundary values of a binomial coefficient: (n0)=1\binom{n}{0}=1 for every nn, while (nj)=0\binom{n}{j} = 0 whenever j>nj > n, so in particular (0j)=0\binom{0}{j} = 0 for j1j \ge 1 (The set [A]k[A]^{k} of kk-element subsets and the binomial coefficient (nk):=[n]k\binom{n}{k} := \lvert [n]^{k}\rvert); ι(0)=0\iota(0) = 0 and ι(p)0\iota(p) \ge 0 for every natural pp, ι\iota being strictly increasing with ι(0)=0\iota(0) = 0 (Laws of finite sums and products in N\mathbb{N}, and ι(k<nak)=k<nι(ak)\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k), clause 7).

[L10]

R\mathbb{R} is an ordered field (Ordered field, Field).

Proof

technique · direct
1.1

Each SjS_j with j1j \ge 1 counted pointwise. By [L1], ιAJ=xX1AJ(x)\iota\lvert A_J\rvert = \sum_{x \in X}\mathbf{1}_{A_J}(x) for every JIJ \subseteq I; interchanging the resulting double sum by [L4] gives Sj=xX(J[I]j1AJ(x))S_j = \sum_{x \in X}\big(\sum_{J \in [I]^{j}}\mathbf{1}_{A_J}(x)\big). For j1j \ge 1 every J[I]jJ \in [I]^{j} is nonempty, so by [L2] the inner sum is ι\iota of the number of J[I]jJ \in [I]^{j} with JT(x)J \subseteq T(x), that is ι[T(x)]j=ι(t(x)j)\iota\lvert [T(x)]^{j}\rvert = \iota\binom{t(x)}{j}. Hence Sj=xXι(t(x)j)S_j = \sum_{x \in X}\iota\binom{t(x)}{j} for every j1j \ge 1.

L1L2L4
1.2

The pointwise truncation. For xXx \in X and mNm \in \mathbb{N} put cm(x):=i<m(1)iι(t(x)i+1)c_m(x) := \sum_{i<m}(-1)^{i}\,\iota\binom{t(x)}{i+1}.

construct
1.3

A closed form for cm(x)c_m(x). Splitting j<m+1(1)jι(t(x)j)\sum_{j<m+1}(-1)^{j}\iota\binom{t(x)}{j} at the index 11 by [L5] gives (1)0ι(t(x)0)+i<m(1)1+iι(t(x)1+i)(-1)^{0}\iota\binom{t(x)}{0} + \sum_{i<m}(-1)^{1+i}\iota\binom{t(x)}{1+i}, which by [L7] and scaling is 1cm(x)1 - c_m(x); hence cm(x)=1j<m+1(1)jι(t(x)j)c_m(x) = 1 - \sum_{j<m+1}(-1)^{j}\iota\binom{t(x)}{j}. So cm(x)=1(1)mι(t(x)1m)c_m(x) = 1 - (-1)^{m}\iota\binom{t(x)-1}{m} when t(x)1t(x) \ge 1, by [L6]. When t(x)=0t(x) = 0 every term of cm(x)c_m(x) is ι(0i+1)=0\iota\binom{0}{i+1} = 0 by [L9], so cm(x)=0c_m(x) = 0.

L5L6L7L9
2.1

TmT_m counted pointwise. Scaling step 1.1 by (1)i(-1)^{i} gives (1)iSi+1=xX(1)iι(t(x)i+1)(-1)^{i}S_{i+1} = \sum_{x \in X}(-1)^{i}\iota\binom{t(x)}{i+1} for every ii; summing over imi \in m, using im=i<m\sum_{i \in m} = \sum_{i<m} from [L3] and interchanging by [L4], gives Tm=xXcm(x)T_m = \sum_{x \in X}c_m(x) for every mNm \in \mathbb{N}.

step 1.1step 1.2L3L4L5
2.2

The pointwise comparison. Let xXx \in X and rNr \in \mathbb{N}. If xUx \notin U then t(x)=0t(x) = 0 by [L2], so c2r(x)=c2r+1(x)=0=1U(x)c_{2r}(x) = c_{2r+1}(x) = 0 = \mathbf{1}_U(x) by step 1.3. If xUx \in U then t(x)1t(x) \ge 1, and step 1.3 with [L7] gives c2r+1(x)=1+ι(t(x)12r+1)1=1U(x)c_{2r+1}(x) = 1 + \iota\binom{t(x)-1}{2r+1} \ge 1 = \mathbf{1}_U(x) and c2r(x)=1ι(t(x)12r)1=1U(x)c_{2r}(x) = 1 - \iota\binom{t(x)-1}{2r} \le 1 = \mathbf{1}_U(x), since ι\iota of a natural number is at least 00 by [L9]. So c2r+1(x)1U(x)c2r(x)c_{2r+1}(x) \ge \mathbf{1}_U(x) \ge c_{2r}(x) for every xXx \in X.

step 1.3L2L7L9L10
3.1

Clauses 1 and 2. Monotonicity of a finite sum over the index set XX, applied to step 2.2, gives xXc2r(x)xX1U(x)xXc2r+1(x)\sum_{x \in X}c_{2r}(x) \le \sum_{x \in X}\mathbf{1}_U(x) \le \sum_{x \in X}c_{2r+1}(x); the middle term is ιU\iota\lvert U\rvert by [L1] and the outer two are T2rT_{2r} and T2r+1T_{2r+1} by step 2.1.

step 2.1step 2.2L1L5
4.1

Clause 3. The sets [I]i+1[I]^{i+1} for iNi \in N are pairwise disjoint with union P(I){}\mathcal{P}(I)\setminus\{\varnothing\}, since a nonempty JIJ \subseteq I has exactly one cardinality and it satisfies 1JN1 \le \lvert J\rvert \le N by [L2]; splitting the sieve sum along this partition, and using (1)J+1=(1)i+2=(1)i(-1)^{\lvert J\rvert + 1} = (-1)^{i+2} = (-1)^{i} for J[I]i+1J \in [I]^{i+1} from [L7], gives JP(I){}(1)J+1ιAJ=i<N(1)iSi+1=TN\sum_{J \in \mathcal{P}(I)\setminus\{\varnothing\}}(-1)^{\lvert J\rvert+1}\iota\lvert A_J\rvert = \sum_{i<N}(-1)^{i}S_{i+1} = T_N, which equals ιU\iota\lvert U\rvert by [L8]. For mNm \ge N, splitting TmT_m at the index NN by [L5] and noting that iNi \ge N forces i+1>Ni+1 > N, hence [I]i+1=[I]^{i+1} = \varnothing and Si+1=0S_{i+1} = 0 by [L2], [L3] and [L9], gives Tm=TN=ιUT_m = T_N = \iota\lvert U\rvert; with step 3.1 this completes all three clauses.

step 3.1L2L3L5L7L8L9

Remarks

  • Why the parity is written as 2r2r and 2r+12r+1. Nothing among this page's declared prerequisites defines the words even and odd, and the statement needs only the two families of truncation depths, which the two displayed forms name directly. The sign facts (1)2r=1(-1)^{2r} = 1 and (1)2r+1=1(-1)^{2r+1} = -1 are then the whole use of parity in the proof.

  • Where the error term comes from. Step 1.3 says that a truncation at depth mm misses the indicator of UU at a point of trace size t1t \ge 1 by exactly (1)mι(t1m)(-1)^{m}\iota\binom{t-1}{m}, a single binomial coefficient. The sign of that term is what makes the inequality go one way for one parity and the other way for the other, and its nonnegativity is what makes the inequality hold at all.

  • A point outside the union contributes nothing at any depth, which is why no hypothesis relating XX to UU appears. The ambient set may be much larger than the union without affecting either side.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The number of surjections from an nn-element set onto a kk-element set is i<k+1(1)i(ki)(ki)n\sum_{i<k+1}(-1)^{i}\binom{k}{i}(k-i)^{n}, read in R\mathbb{R} through ι\iota

Statement

Let AA and BB be finite sets, n:=An := \lvert A\rvert and k:=Bk := \lvert B\rvert, and write

Surj(A,B):={f:f is a surjection AB}\operatorname{Surj}(A,B) := \{\, f : f \text{ is a surjection } A \to B \,\}

(Injection, surjection, bijection). Then Surj(A,B)\operatorname{Surj}(A,B) is finite and, in R\mathbb{R},

ιSurj(A,B)  =  i<k+1(1)iι(ki)ι((ki)n),\iota\lvert \operatorname{Surj}(A,B)\rvert \;=\; \sum_{i<k+1}(-1)^{i}\,\iota\binom{k}{i}\,\iota\big((k-i)^{\,n}\big),

where ι\iota is the canonical natural (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field), (ki)n(k-i)^{n} is the N\mathbb{N}-valued power of Exponentiation of natural numbers, mnm^{n}, and its agreement with the integer power in R\mathbb{R}, and kik-i is the truncated difference of Finite sums and finite products of natural numbers, k<nak\sum_{k<n} a_k and k<nak\prod_{k<n} a_k in N\mathbb{N}, which is the ordinary one throughout the range iki \le k of the sum.

All three degenerate readings are part of the statement, and each is computed rather than stipulated.

Facts & Assumptions

Given: Finite sets AA and BB with n:=An := \lvert A\rvert and k:=Bk := \lvert B\rvert; the set Map(A,B)\operatorname{Map}(A,B) of all functions ABA \to B; and, for bBb \in B, the set Fb:={fMap(A,B):bf[A]}F_b := \{\, f \in \operatorname{Map}(A,B) : b \notin f[A] \,\} of functions missing the value bb.

[L1]

Map(A,B)\operatorname{Map}(A,B) is finite with Map(A,B)=kn\lvert\operatorname{Map}(A,B)\rvert = k^{\,n}. This is The set ABA^{B} of functions BAB \to A between finite sets is finite, with AB=AB\lvert A^{B}\rvert = \lvert A\rvert^{\lvert B\rvert} with its AA taken to be BB and its BB taken to be AA, so that its ABA^{B} is the set of functions ABA \to B and its formula reads BA=kn\lvert B\rvert^{\lvert A\rvert} = k^{\,n} (Exponentiation of natural numbers, mnm^{n}, and its agreement with the integer power in R\mathbb{R}).

[L2]

(Fb)bB(F_b)_{b \in B} is a family of subsets of the finite set X:=Map(A,B)X := \operatorname{Map}(A,B) indexed by the finite set BB, hence a sieve family with ambient set XX, and its intersections FJF_J for JBJ \subseteq B satisfy F=XF_\varnothing = X (A finite family (Ai)iI(A_i)_{i \in I} of subsets of a finite set XX, the intersections AJA_J for JIJ \subseteq I, and the convention A=XA_\varnothing = X, A subset of a finite set is finite, with BA\lvert B\rvert \le \lvert A\rvert, and equality holds if and only if B=AB = A, The cardinality A\lvert A\rvert of a finite set).

[L3]

fMap(A,B)f \in \operatorname{Map}(A,B) is a surjection exactly when f[A]=Bf[A] = B, that is exactly when there is no bBb \in B with bf[A]b \notin f[A] (Injection, surjection, bijection). Hence Surj(A,B)=XbBFb\operatorname{Surj}(A,B) = X \setminus \bigcup_{b \in B}F_b, and it is finite as a subset of XX (A subset of a finite set is finite, with BA\lvert B\rvert \le \lvert A\rvert, and equality holds if and only if B=AB = A).

[L4]

For a finite sieve family (Fb)bB(F_b)_{b\in B} in XX with F=XF_\varnothing=X, the complementary identity is ιXbBFb=JP(B)(1)JιFJ\iota|X\setminus\bigcup_{b\in B}F_b|=\sum_{J\in\mathcal P(B)}(-1)^{|J|}\iota|F_J| (Inclusion and exclusion: ιiIAi=JI(1)J+1ιAJ\iota\lvert\bigcup_{i \in I} A_i\rvert = \sum_{\varnothing \ne J \subseteq I}(-1)^{\lvert J\rvert + 1}\,\iota\lvert A_J\rvert, together with the complementary form counting the elements in none of the AiA_i, clause 2).

[L6]

Partition of a power set by cardinality: the sets [B]i[B]^{i} for iσ(k)i \in \sigma(k) are pairwise disjoint with union P(B)\mathcal{P}(B), since a subset of BB has exactly one cardinality and it is at most kk; and [B]i=(ki)\lvert [B]^{i}\rvert = \binom{k}{i} (A subset of a finite set is finite, with BA\lvert B\rvert \le \lvert A\rvert, and equality holds if and only if B=AB = A, clause 2, The set [A]k[A]^{k} of kk-element subsets and the binomial coefficient (nk):=[n]k\binom{n}{k} := \lvert [n]^{k}\rvert, P(A)=2A\lvert\mathcal{P}(A)\rvert = 2^{\lvert A\rvert} for finite AA).

[L7]

Splitting a sum along a partition of its index set (The sum rule: a finite disjoint union is finite with AB=A+B\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert and iIAi=iIAi\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert, and a sum over a finite index set splits along a partition, clause 3); a constant real summand pSλ=ι(S)λ\sum_{p \in S}\lambda = \iota(\lvert S\rvert)\lambda and the bridge inui=i<nui\sum_{i \in n}u_i = \sum_{i<n}u_i (The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form, clauses (a) and (c)); and the real finite sum itself (Finite sums and finite products, by recursion).

Proof

technique · direct
1.1

The ambient set. Put X:=Map(A,B)X := \operatorname{Map}(A,B); it is finite with X=kn\lvert X\rvert = k^{\,n} by [L1].

L1
1.2

The sieve family. For bBb \in B the set FbF_b of functions missing bb is a subset of XX, and by [L3] a function fXf \in X is a surjection exactly when fbBFbf \notin \bigcup_{b \in B}F_b; so Surj(A,B)=XbBFb\operatorname{Surj}(A,B) = X \setminus \bigcup_{b \in B}F_b is the complement of the union of the sieve family (Fb)bB(F_b)_{b \in B} inside XX.

L2L3construct
1.3

The intersections are function sets. For every JBJ \subseteq B, FJ=Map(A,BJ)F_J = \operatorname{Map}(A, B\setminus J): for JJ \ne \varnothing, fFJf \in F_J says that ff misses every bJb \in J, that is that ff takes all its values in BJB \setminus J; and for J=J = \varnothing both sides are Map(A,B)\operatorname{Map}(A,B), the left by the stipulation F=XF_\varnothing = X of [L2]. Hence FJ=BJn=(kJ)n\lvert F_J\rvert = \lvert B\setminus J\rvert^{\,n} = (k - \lvert J\rvert)^{\,n} by [L1] applied to BJB \setminus J and by [L5].

L1L2L5
2.1

The sieve. Applying [L4] to the family of step 1.2 and substituting step 1.3, ιSurj(A,B)=JP(B)(1)JιFJ=JP(B)(1)Jι((kJ)n)\iota\lvert\operatorname{Surj}(A,B)\rvert = \sum_{J \in \mathcal{P}(B)}(-1)^{\lvert J\rvert}\,\iota\lvert F_J\rvert = \sum_{J \in \mathcal{P}(B)}(-1)^{\lvert J\rvert}\,\iota\big((k-\lvert J\rvert)^{\,n}\big).

step 1.2step 1.3L4
3.1

Grouping the subsets of BB by size. Splitting the last sum along the partition of [L6] and using the constant clause of [L7] on each block, where the summand depends on JJ only through J=i\lvert J\rvert = i, gives JP(B)(1)Jι((kJ)n)=i<k+1ι(ki)(1)iι((ki)n)\sum_{J \in \mathcal{P}(B)}(-1)^{\lvert J\rvert}\iota\big((k-\lvert J\rvert)^{\,n}\big) = \sum_{i<k+1}\iota\binom{k}{i}\,(-1)^{i}\,\iota\big((k-i)^{\,n}\big).

step 2.1L6L7
4.1

Combining steps 2.1 and 3.1 gives ιSurj(A,B)=i<k+1(1)iι(ki)ι((ki)n)\iota\lvert\operatorname{Surj}(A,B)\rvert = \sum_{i<k+1}(-1)^{i}\,\iota\binom{k}{i}\,\iota\big((k-i)^{\,n}\big), and Surj(A,B)\operatorname{Surj}(A,B) is finite by [L3]; since ι\iota is injective, the identity determines the count in N\mathbb{N}.

step 2.1step 3.1L3L8

Remarks

  • The convention 00=10^{0} = 1 is load bearing exactly once, at n=0n = 0 and k=0k = 0, where the formula returns ι(00)\iota(0^{0}) and the truth is that the empty function is a surjection onto the empty set. It is not a convenience: it is the base clause of the recursion defining natural exponentiation, and changing it would make the formula false at that single point.

  • Why the family is indexed by BB and not by AA. The sieve removes the functions that miss a value, and there is one condition per element of the codomain. This is also why the alternating sum runs to kk and not to nn.

  • The count is a natural number. The identity is stated in R\mathbb{R} because it carries signs, and ι\iota is injective, so it pins down the natural number Surj(A,B)\lvert\operatorname{Surj}(A,B)\rvert exactly.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

The derangement number DnD_n: the number of bijections of an nn-element set with no fixed point

Definition

Let AA be a finite set. A derangement of AA is a bijection f:AAf : A \to A with f(a)af(a) \ne a for every aAa \in A (Injection, surjection, bijection). Write

Der(A):={fBij(A) : f(a)a for every aA},\operatorname{Der}(A) := \{\, f \in \operatorname{Bij}(A) \ :\ f(a) \ne a \text{ for every } a \in A \,\},

where Bij(A)\operatorname{Bij}(A) is the set of bijections of AA onto itself.

Der(A)\operatorname{Der}(A) is finite. Bij(A)\operatorname{Bij}(A) is finite with Bij(A)=A!\lvert\operatorname{Bij}(A)\rvert = \lvert A\rvert! (A finite set AA with A=n\lvert A\rvert = n has exactly n!n! bijections onto itself, and n!n! bijections onto any set of the same cardinality, The factorial n!n! and the falling factorial nkn^{\underline{k}}, defined by recursion in N\mathbb{N}), and Der(A)\operatorname{Der}(A) is a subset of it, hence finite (A subset of a finite set is finite, with BA\lvert B\rvert \le \lvert A\rvert, and equality holds if and only if B=AB = A, clause 1). So Der(A)\lvert\operatorname{Der}(A)\rvert is a natural number (The cardinality A\lvert A\rvert of a finite set).

The count depends only on A\lvert A\rvert. Let h:AAh : A \to A' be a bijection of finite sets. The map fhfh1f \mapsto h \circ f \circ h^{-1} sends Bij(A)\operatorname{Bij}(A) into Bij(A)\operatorname{Bij}(A'), since composites and inverses of bijections are bijections, and it sends Der(A)\operatorname{Der}(A) into Der(A)\operatorname{Der}(A'): if h(f(h1(a)))=ah(f(h^{-1}(a'))) = a' for some aAa' \in A' then, applying h1h^{-1} and writing a:=h1(a)a := h^{-1}(a'), we get f(a)=af(a) = a. The map gh1ghg \mapsto h^{-1} \circ g \circ h is a two-sided inverse, so Der(A)Der(A)\operatorname{Der}(A) \approx \operatorname{Der}(A') and the two sets have the same cardinality by the transport clause (c) of The cardinality A\lvert A\rvert of a finite set.

Definition. For nNn \in \mathbb{N} (The natural numbers N\mathbb{N} (von Neumann)) set

Dn  :=  Der(n)N,D_n \;:=\; \big\lvert \operatorname{Der}(n) \big\rvert \in \mathbb{N},

the derangement number. Since n=n\lvert n\rvert = n, the previous paragraph gives Der(A)=DA\lvert\operatorname{Der}(A)\rvert = D_{\lvert A\rvert} for every finite set AA.

Three values, read off the definition and not stipulated.

  • D0=1D_0 = 1. Here 0=0 = \varnothing, the only function \varnothing \to \varnothing is the empty function, it is a bijection, and the condition "f(a)af(a) \ne a for every aa \in \varnothing" holds vacuously. So Der()={}\operatorname{Der}(\varnothing) = \{\varnothing\}.
  • D1=0D_1 = 0. Here 1={0}1 = \{0\} and the only bijection of {0}\{0\} is the identity, which fixes 00.
  • D2=1D_2 = 1. Here 2={0,1}2 = \{0,1\}, the two bijections are the identity and the exchange of 00 and 11, and only the second is fixed-point free.

Remarks

  • A set of bijections, with no group vocabulary. The object counted is a set of functions. Nothing among this page's declared prerequisites defines a symmetric group, a permutation cycle or a conjugacy class, and no result about DnD_n stated here needs one.

  • D0=1D_0 = 1 is not a convention. It is what the definition returns at n=0n = 0, and it is the value that makes the closed formula and the first recurrence true at their first legal index. A text that sets D0=1D_0 = 1 "by convention" is stipulating what is here computed.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

ι(Dn)=ι(n!)i<n+1(1)i/ι(i!)\iota(D_n) = \iota(n!)\sum_{i<n+1}(-1)^{i}/\iota(i!), with the term at i=0i = 0 equal to 11 and D0=1D_0 = 1

Statement

For every nNn \in \mathbb{N}, in R\mathbb{R},

ι(Dn)  =  ι(n!)i<n+1(1)iι(i!),\iota(D_n) \;=\; \iota(n!)\sum_{i<n+1}\frac{(-1)^{i}}{\iota(i!)},

where DnD_n is the derangement number (The derangement number DnD_n: the number of bijections of an nn-element set with no fixed point), n!n! the factorial (The factorial n!n! and the falling factorial nkn^{\underline{k}}, defined by recursion in N\mathbb{N}) and ι\iota the canonical natural (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field). Each division is legitimate because i!0i! \ne 0, hence ι(i!)0\iota(i!) \ne 0.

The index runs from 00, and the term at i=0i = 0 is (1)0/ι(0!)=1(-1)^{0}/\iota(0!) = 1. At n=0n = 0 the identity reads ι(D0)=ι(0!)1=1\iota(D_0) = \iota(0!)\cdot 1 = 1, which agrees with D0=1D_0 = 1; at n=1n = 1 it reads ι(D1)=1(11)=0\iota(D_1) = 1\cdot(1-1) = 0; and at n=2n = 2 it reads ι(D2)=2(11+1/2)=1\iota(D_2) = 2\cdot(1-1+1/2) = 1.

Since ι\iota is injective, the identity determines DnD_n as a natural number (Laws of finite sums and products in N\mathbb{N}, and ι(k<nak)=k<nι(ak)\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k), clause 7).

Facts & Assumptions

Given: A natural number nn, the set X:=Bij(n)X := \operatorname{Bij}(n) of bijections of nn onto itself, and, for ana \in n, the set Aa:={fX:f(a)=a}A_a := \{\, f \in X : f(a) = a \,\} of bijections fixing aa.

[L1]

Bij(S)\operatorname{Bij}(S) is finite with Bij(S)=S!\lvert\operatorname{Bij}(S)\rvert = \lvert S\rvert! for every finite SS (A finite set AA with A=n\lvert A\rvert = n has exactly n!n! bijections onto itself, and n!n! bijections onto any set of the same cardinality, The factorial n!n! and the falling factorial nkn^{\underline{k}}, defined by recursion in N\mathbb{N}); in particular X=n!\lvert X\rvert = n! and n=n\lvert n\rvert = n (The cardinality A\lvert A\rvert of a finite set).

[L3]

Der(n)=XanAa\operatorname{Der}(n) = X \setminus \bigcup_{a \in n}A_a, since a bijection of nn is a derangement exactly when it fixes no point (The derangement number DnD_n: the number of bijections of an nn-element set with no fixed point, Injection, surjection, bijection).

[L4]

For a finite sieve family (Aa)an(A_a)_{a\in n} in XX with A=XA_\varnothing=X, the complementary identity is ιXanAa=JP(n)(1)JιAJ\iota|X\setminus\bigcup_{a\in n}A_a|=\sum_{J\in\mathcal P(n)}(-1)^{|J|}\iota|A_J| (Inclusion and exclusion: ιiIAi=JI(1)J+1ιAJ\iota\lvert\bigcup_{i \in I} A_i\rvert = \sum_{\varnothing \ne J \subseteq I}(-1)^{\lvert J\rvert + 1}\,\iota\lvert A_J\rvert, together with the complementary form counting the elements in none of the AiA_i, clause 2).

[L9]

R\mathbb{R} is an ordered field, so division by a nonzero element is available (Ordered field, Field); and (1)0=1(-1)^{0} = 1 (Integer powers ama^m).

Proof

technique · direct
1.1

The ambient set and the sieve family. X=Bij(n)X = \operatorname{Bij}(n) is finite with X=n!\lvert X\rvert = n! by [L1], the sets AaA_a for ana \in n are subsets of XX, and Der(n)\operatorname{Der}(n) is the complement in XX of their union by [L3].

L1L2L3construct
1.2

The intersections are bijection sets of a smaller set. For JnJ \subseteq n the map ff ⁣ ⁣(nJ)f \mapsto f\!\restriction\!(n\setminus J) is a bijection of AJA_J onto Bij(nJ)\operatorname{Bij}(n\setminus J). Indeed a bijection ff of nn fixing every point of JJ has f[J]=Jf[J] = J, hence f[nJ]=nJf[n\setminus J] = n \setminus J by injectivity, so its restriction is a bijection of nJn\setminus J; conversely a bijection gg of nJn\setminus J extends by the identity on JJ to a bijection of nn fixing every point of JJ, and the two constructions are mutually inverse. For J=J = \varnothing both sides are XX, by the stipulation of [L2].

L1L2L3construct
1.3

Hence AJ=nJ!=(nJ)!\lvert A_J\rvert = \lvert n\setminus J\rvert! = (n - \lvert J\rvert)! for every JnJ \subseteq n, by [L1] applied to nJn\setminus J and by [L7].

L1L7
2.1

The sieve. Applying [L4] to the family of step 1.1 and substituting step 1.3, ι(Dn)=ιDer(n)=JP(n)(1)Jι((nJ)!)\iota(D_n) = \iota\lvert\operatorname{Der}(n)\rvert = \sum_{J \in \mathcal{P}(n)}(-1)^{\lvert J\rvert}\,\iota\big((n-\lvert J\rvert)!\big).

step 1.1step 1.2step 1.3L4
3.1

Grouping the subsets of nn by size. Splitting along the partition of [L5] and using the constant clause of [L6] on each block, where the summand depends on JJ only through J=i\lvert J\rvert = i, gives ι(Dn)=i<n+1ι(ni)(1)iι((ni)!)\iota(D_n) = \sum_{i<n+1}\iota\binom{n}{i}\,(-1)^{i}\,\iota\big((n-i)!\big).

step 2.1L5L6
4.1

Each coefficient collapses. For i<n+1i < n+1, that is ini \le n, [L8] gives ι(ni)ι((ni)!)=ι(n!)/ι(i!)\iota\binom{n}{i}\,\iota\big((n-i)!\big) = \iota(n!)/\iota(i!), so the ii-th summand of step 3.1 is (1)iι(n!)/ι(i!)(-1)^{i}\,\iota(n!)/\iota(i!); scaling the sum by the constant ι(n!)\iota(n!) through [L6] gives ι(Dn)=ι(n!)i<n+1(1)i/ι(i!)\iota(D_n) = \iota(n!)\sum_{i<n+1}(-1)^{i}/\iota(i!).

step 3.1L6L8L9

Remarks

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

ι(Dn)=ι(n)ι(Dn1)+(1)n\iota(D_n) = \iota(n)\,\iota(D_{n-1}) + (-1)^{n} for n1n \ge 1, and Dn=(n1)(Dn1+Dn2)D_n = (n-1)(D_{n-1} + D_{n-2}) for n2n \ge 2

Statement

Let DnD_n be the derangement numbers (The derangement number DnD_n: the number of bijections of an nn-element set with no fixed point) and ι\iota the canonical natural (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field). Then:

  1. For every n1n \ge 1, in R\mathbb{R}, ι(Dn)  =  ι(n)ι(Dn1)+(1)n.\iota(D_n) \;=\; \iota(n)\,\iota(D_{n-1}) + (-1)^{n} .
  2. For every n2n \ge 2, in N\mathbb{N}, Dn  =  (n1)(Dn1+Dn2).D_n \;=\; (n-1)\,\big(D_{n-1} + D_{n-2}\big).

All differences are the truncated ones (Finite sums and finite products of natural numbers, k<nak\sum_{k<n} a_k and k<nak\prod_{k<n} a_k in N\mathbb{N}), which in the stated ranges are the ordinary ones.

Both hypotheses are exactly what the proofs need, and nothing is asserted outside them. Clause 1 is proved from the identity n=(n1)+1n = (n-1)+1 and its consequence n!=(n1)!nn! = (n-1)!\cdot n, both of which fail at n=0n = 0 under the truncated difference, where n1n-1 is 00; so n=1n = 1 is its first legal index, and there it reads ι(D1)=ι(1)ι(D0)1=0\iota(D_1) = \iota(1)\,\iota(D_0) - 1 = 0. Clause 2 is derived by applying clause 1 twice, at nn and at n1n-1, so it needs n11n - 1 \ge 1; its first legal index is n=2n = 2, where it reads D2=1(D1+D0)=1D_2 = 1\cdot(D_1 + D_0) = 1. Under the truncated difference the two displayed formulas happen also to be true at n=0n = 0 and at n=1n = 1 respectively, both sides being 11 in the first case and 00 in the second, but neither of those readings is proved here and neither is claimed.

Facts & Assumptions

Given: A natural number nn with n1n \ge 1 in clause 1 and n2n \ge 2 in clause 2; the abbreviation p:=n1p := n-1, so that p+1=np + 1 = n (Order on the natural numbers, Finite sums and finite products of natural numbers, k<nak\sum_{k<n} a_k and k<nak\prod_{k<n} a_k in N\mathbb{N}, Every nonzero natural number is a successor).

[L1]

The derangement formula: ι(Dm)=ι(m!)i<m+1(1)i/ι(i!)\iota(D_m) = \iota(m!)\sum_{i<m+1}(-1)^{i}/\iota(i!) for every mNm \in \mathbb{N} (ι(Dn)=ι(n!)i<n+1(1)i/ι(i!)\iota(D_n) = \iota(n!)\sum_{i<n+1}(-1)^{i}/\iota(i!), with the term at i=0i = 0 equal to 11 and D0=1D_0 = 1).

[L2]

Recursion clause of the real finite sum: i<q+1ui=i<qui+uq\sum_{i<q+1}u_i = \sum_{i<q}u_i + u_q (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L3]

Factorials: σ(m)!=m!σ(m)\sigma(m)! = m!\cdot\sigma(m), so n!=p!nn! = p!\cdot n when p+1=np+1 = n; and m!0m! \ne 0 for every mm (The factorial n!n! and the falling factorial nkn^{\underline{k}}, defined by recursion in N\mathbb{N}).

[L4]

ι\iota is additive and multiplicative with ι(1)=1\iota(1) = 1, and it is injective (Laws of finite sums and products in N\mathbb{N}, and ι(k<nak)=k<nι(ak)\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k), clauses 0 and 7, The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field). In particular ι(n)1=ι(p)\iota(n) - 1 = \iota(p) when p+1=np+1 = n, and ι(m!)0\iota(m!) \ne 0.

[L5]

Powers of 1-1: (1)0=1(-1)^{0} = 1 and (1)q+1=(1)q(-1)^{q+1} = -(-1)^{q} (Integer powers ama^m).

[L6]

R\mathbb{R} is an ordered field, so subtraction and division by a nonzero element are available (Ordered field, Field).

Proof

technique · direct
1.1

Let n1n \ge 1 and put p:=n1p := n-1, so p+1=np+1 = n. Then n!=p!nn! = p!\cdot n by [L3], hence ι(n!)=ι(p!)ι(n)\iota(n!) = \iota(p!)\,\iota(n) by [L4], and both ι(n!)\iota(n!) and ι(p!)\iota(p!) are nonzero.

givenL3L4
1.2

The formula at pp. By [L1] and p+1=np+1 = n, ι(Dp)=ι(p!)i<n(1)i/ι(i!)\iota(D_p) = \iota(p!)\sum_{i<n}(-1)^{i}/\iota(i!).

L1
1.3

Splitting the sum at its last index. By [L2], i<n+1(1)i/ι(i!)=i<n(1)i/ι(i!)+(1)n/ι(n!)\sum_{i<n+1}(-1)^{i}/\iota(i!) = \sum_{i<n}(-1)^{i}/\iota(i!) + (-1)^{n}/\iota(n!).

L2
2.1

Clause 1. Multiplying step 1.3 by ι(n!)\iota(n!) and using [L1] at m=nm = n, step 1.1 and step 1.2, ι(Dn)=ι(n!)i<n(1)i/ι(i!)+(1)n=ι(n)ι(p!)i<n(1)i/ι(i!)+(1)n=ι(n)ι(Dp)+(1)n\iota(D_n) = \iota(n!)\sum_{i<n}(-1)^{i}/\iota(i!) + (-1)^{n} = \iota(n)\,\iota(p!)\sum_{i<n}(-1)^{i}/\iota(i!) + (-1)^{n} = \iota(n)\,\iota(D_p) + (-1)^{n}.

step 1.1step 1.2step 1.3L1L6
3.1

Now let n2n \ge 2, so that p=n11p = n-1 \ge 1 and p1=n2p - 1 = n-2. Applying step 2.1 at pp in place of nn gives ι(Dp)=ι(p)ι(Dn2)+(1)p\iota(D_p) = \iota(p)\,\iota(D_{n-2}) + (-1)^{p}, hence (1)p=ι(Dp)ι(p)ι(Dn2)(-1)^{p} = \iota(D_p) - \iota(p)\,\iota(D_{n-2}); and (1)n=(1)p+1=(1)p(-1)^{n} = (-1)^{p+1} = -(-1)^{p} by [L5], so (1)n=ι(p)ι(Dn2)ι(Dp)(-1)^{n} = \iota(p)\,\iota(D_{n-2}) - \iota(D_p).

step 2.1L5L6
4.1

Clause 2. Substituting step 3.1 into step 2.1, ι(Dn)=ι(n)ι(Dp)ι(Dp)+ι(p)ι(Dn2)=(ι(n)1)ι(Dp)+ι(p)ι(Dn2)=ι(p)(ι(Dp)+ι(Dn2))\iota(D_n) = \iota(n)\,\iota(D_p) - \iota(D_p) + \iota(p)\,\iota(D_{n-2}) = \big(\iota(n)-1\big)\iota(D_p) + \iota(p)\,\iota(D_{n-2}) = \iota(p)\big(\iota(D_p) + \iota(D_{n-2})\big), using ι(n)1=ι(p)\iota(n)-1 = \iota(p) from [L4]; the right-hand side is ι(p(Dn1+Dn2))\iota\big(p\,(D_{n-1} + D_{n-2})\big) by the additivity and multiplicativity of ι\iota, so Dn=(n1)(Dn1+Dn2)D_n = (n-1)(D_{n-1} + D_{n-2}) by injectivity.

step 2.1step 3.1L4L6algebra

Remarks

  • Clause 2 is derived from clause 1 and not from the formula. Two instances of clause 1, at nn and at n1n-1, are enough, and that is why clause 2 begins one index later: the second instance needs n11n-1 \ge 1.

  • Why clause 1 is stated in R\mathbb{R} and clause 2 in N\mathbb{N}. Clause 1 carries the term (1)n(-1)^{n}, which is not a natural number when nn is odd. Clause 2 has no signs left in it, both sides are counts, and injectivity of ι\iota carries the identity back into N\mathbb{N} where it belongs.

  • The truncated difference is why the hypotheses have to be written out. Under it the symbols Dn1D_{n-1} and Dn2D_{n-2} never become ill formed: at n=0n = 0 the first reads D0D_0 and at n=1n = 1 the second reads D0D_0 as well. So a reader cannot tell from the shape of the formula where it stops being proved, and the ranges n1n \ge 1 and n2n \ge 2 have to be stated rather than inferred.

DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

A finite list of reals, and its strictly increasing and strictly decreasing sublists

Definition

Let NNN \in \mathbb{N} (The natural numbers N\mathbb{N} (von Neumann)). A finite list of reals of length NN is a function a:NRa : N \to \mathbb{R}, written aia_i for a(i)a(i); here N={i:i<N}N = \{\, i : i < N\,\} is the von Neumann natural itself (On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n, Order on the natural numbers), so the indices are 0,1,,N10, 1, \dots, N-1 and the list of length 00 is the empty function. The list is pairwise distinct when aa is injective, that is when aiaja_i \ne a_j whenever iji \ne j (Injection, surjection, bijection).

A sublist of aa of length LL, for LNL \in \mathbb{N}, is a function s:LNs : L \to N that is strictly increasing on indices, meaning s(p)<s(q)s(p) < s(q) whenever p<q<Lp < q < L; its terms are as(0),,as(L1)a_{s(0)}, \dots, a_{s(L-1)}. Such an ss is injective, since natural-order trichotomy gives p<qp<q or q<pq<p when pqp\ne q, and hence s(p)s(q)s(p)\ne s(q) (Trichotomy of the order on N\mathbb{N}).

The sublist ss is

  • strictly increasing when as(p)<as(q)a_{s(p)} < a_{s(q)} for all p<q<Lp < q < L;
  • strictly decreasing when as(p)>as(q)a_{s(p)} > a_{s(q)} for all p<q<Lp < q < L,

the order being that of the ordered field R\mathbb{R} (Ordered field).

Boundary readings, which are part of the definition and not exceptions. A sublist of length 00 or 11 has no pair p<q<Lp < q < L at all, so it is both strictly increasing and strictly decreasing, vacuously. A list of length NN has a sublist of length 11 exactly when N1N \ge 1, namely s(0):=is(0) := i for any i<Ni < N; and it has no sublist of length LL with L>NL > N, since ss would be an injection of LL into NN, contrary to the finite pigeonhole principle (The pigeonhole principle on N\mathbb{N}, clause 2).

Every count here is a natural number. The length of a list and the length of a sublist are naturals, and no cardinality of an infinite set is used; a list is a function on a natural number, so it is finite in the sense of The cardinality A\lvert A\rvert of a finite set.

Remarks

  • A sublist is a choice of positions, not a choice of values. Two positions carrying equal values are different sublists of length 11. This is why the monotonicity conditions are stated on as(p)a_{s(p)} and as(q)a_{s(q)} rather than on a set of values, and why the pairwise-distinctness hypothesis has to be imposed separately when a result needs it.

  • Strictness on both sides. The indices increase strictly, so a sublist reads the list left to right without repeating a position; the values increase or decrease strictly, so no two terms of a monotone sublist are equal. Neither strictness is redundant: a list may repeat a value, and then a nondecreasing sublist could be longer than any strictly increasing one.

  • The empty list. At N=0N = 0 the only sublists are the empty one, of length 00. Any statement asserting the existence of a sublist of length 11 is therefore false at N=0N = 0, and any statement about lists of length mn+1mn+1 has content at m=0m = 0 or n=0n = 0 precisely because mn+11mn+1 \ge 1.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

Every list of mn+1mn+1 pairwise distinct reals has a strictly increasing sublist of length m+1m+1 or a strictly decreasing sublist of length n+1n+1

Statement

Let m,nNm, n \in \mathbb{N} and let a:(mn+1)Ra : (mn+1) \to \mathbb{R} be a pairwise distinct finite list of reals of length mn+1mn+1 (A finite list of reals, and its strictly increasing and strictly decreasing sublists). Then aa has a strictly increasing sublist of length m+1m+1 or a strictly decreasing sublist of length n+1n+1.

The length mn+1mn+1 is at least 11 for all mm and nn, so the statement has content at every pair of indices. At m=0m = 0 the list has one term and the required increasing sublist has length 11, which the single position supplies; at n=0n = 0 the same reading holds for the decreasing sublist, and the increasing one of length 11 is also available.

Facts & Assumptions

Given: Naturals mm and nn, the length N:=mn+1N := mn+1, and a pairwise distinct list a:NRa : N \to \mathbb{R}. For i<Ni < N and L1L \ge 1, call s:LNs : L \to N an increasing run ending at ii when ss is a strictly increasing sublist of aa (in both senses of A finite list of reals, and its strictly increasing and strictly decreasing sublists) with s(L1)=is(L-1) = i, and define a decreasing run ending at ii in the same way with the values strictly decreasing.

[L1]

A nonempty subset of N\mathbb{N} with an upper bound has a greatest element. Let ENE \subseteq \mathbb{N} be nonempty with Eσ(M)E \subseteq \sigma(M) for some MM. Every eEe\in E then satisfies eMe\le M by On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n, so the set C:={cN:ec for every eE}C := \{\, c \in \mathbb{N} : e \le c \text{ for every } e \in E \,\} contains MM and has a least element c0c_0 by The well-ordering principle. If c0Ec_0 \notin E then every eEe \in E satisfies ec0e \le c_0 and ec0e \ne c_0, hence e<c0e < c_0 and σ(e)c0\sigma(e) \le c_0 by Discreteness: σ(n)\sigma(n) is the immediate successor; since EE is nonempty, c00c_0 \ne 0, so c0=σ(c1)c_0 = \sigma(c_1) for some c1c_1 (Every nonzero natural number is a successor) and ec1e \le c_1 for every eEe \in E, putting c1Cc_1 \in C below c0c_0 and contradicting minimality. So c0Ec_0 \in E and c0c_0 is the greatest element of EE.

[L2]

For every i<Ni < N there is an increasing run and a decreasing run ending at ii, both of length 11: take s:1Ns : 1 \to N with s(0)=is(0) = i, which is vacuously monotone in both senses (A finite list of reals, and its strictly increasing and strictly decreasing sublists).

[L3]

Every run has length at most NN: a run of length LL is injective into NN, and there is no injection of LL into NN when N<LN < L (The pigeonhole principle on N\mathbb{N}, clause 2, Injection, surjection, bijection, A finite list of reals, and its strictly increasing and strictly decreasing sublists).

[L4]

Order facts in N\mathbb{N}: k<N    kNk < N \iff k \in N, N={k:k<N}N = \{k : k<N\} and k<σ(M)    kMk < \sigma(M) \iff k \le M (On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n, Order on the natural numbers, The natural numbers N\mathbb{N} (von Neumann)); exactly one of p<qp<q, p=qp=q, q<pq<p holds (Trichotomy of the order on N\mathbb{N}); p<q    σ(p)qp<q \iff \sigma(p) \le q (Discreteness: σ(n)\sigma(n) is the immediate successor); every nonzero natural is a successor (Every nonzero natural number is a successor); and the truncated difference of Finite sums and finite products of natural numbers, k<nak\sum_{k<n} a_k and k<nak\prod_{k<n} a_k in N\mathbb{N}, for which 1L1 \le L gives (L1)+1=L(L-1)+1 = L.

[L5]

m×n=mn\lvert m \times n\rvert = m\,n and N=N\lvert N\rvert = N (The product rule: A×B=AB\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert, and i<mAi=i<mAi\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert, clause 1, The cardinality A\lvert A\rvert of a finite set); and there is no injection σ(K)K\sigma(K) \to K for any KNK \in \mathbb{N} (The pigeonhole principle on N\mathbb{N}, clause 1). A bijection m×nmnm \times n \to mn exists because the two sets have the same cardinality (The cardinality A\lvert A\rvert of a finite set, clause (d)).

[L6]

R\mathbb{R} is an ordered field, so its order is total and aiaja_i \ne a_j gives ai<aja_i < a_j or ai>aja_i > a_j (Ordered field, Field).

Proof

technique · contradiction
1.1

If m=0m=0 or n=0n=0, then N=mn+1=1N=mn+1=1, and the one-term sublist ending at 00 supplied by [L2] has the required length 1=m+11=m+1 or 1=n+11=n+1, respectively. Hence assume m,n1m,n\ge1 and suppose, for contradiction, that aa has neither required sublist.

L2casesassume-contra
1.2

The two run lengths. For i<Ni < N let Inc(i)\mathrm{Inc}(i) be the set of lengths of increasing runs ending at ii and Dec(i)\mathrm{Dec}(i) the set of lengths of decreasing runs ending at ii. Both are nonempty by [L2] and both are contained in σ(N)\sigma(N) by [L3] and [L4], so both have a greatest element by [L1]; write inc(i)\mathrm{inc}(i) and dec(i)\mathrm{dec}(i) for those greatest elements. Both are at least 11.

L1L2L3L4construct
2.1

The bound imposed by the supposition. If some inc(i)\mathrm{inc}(i) were at least m+1m+1, truncating a longest increasing run ending at ii to its first m+1m+1 positions would give a strictly increasing sublist of length m+1m+1; so inc(i)m\mathrm{inc}(i) \le m for every i<Ni < N by [L4], and likewise dec(i)n\mathrm{dec}(i) \le n. Combined with inc(i)1\mathrm{inc}(i) \ge 1 and dec(i)1\mathrm{dec}(i) \ge 1 from step 1.2, this gives inc(i)1<m\mathrm{inc}(i)-1 < m and dec(i)1<n\mathrm{dec}(i)-1 < n, so the map Φ(i):=(inc(i)1, dec(i)1)\Phi(i) := \big(\mathrm{inc}(i)-1,\ \mathrm{dec}(i)-1\big) sends NN into m×nm \times n.

step 1.1step 1.2L4construct
2.2

Extending a run. Let i<j<Ni < j < N. If ai<aja_i < a_j and ss is an increasing run of length L:=inc(i)L := \mathrm{inc}(i) ending at ii, then s:L+1Ns' : L+1 \to N defined by s ⁣ ⁣L:=ss'\!\restriction\!L := s and s(L):=js'(L) := j is again a strictly increasing sublist: its indices increase because s(L1)=i<js(L-1) = i < j, and its values increase because as(p)<as(L1)=ai<aja_{s(p)} < a_{s(L-1)} = a_i < a_j for p<L1p < L-1. So L+1Inc(j)L+1 \in \mathrm{Inc}(j) and inc(j)L+1>inc(i)\mathrm{inc}(j) \ge L+1 > \mathrm{inc}(i). Symmetrically, if ai>aja_i > a_j then dec(j)>dec(i)\mathrm{dec}(j) > \mathrm{dec}(i).

step 1.2L4L6construct
3.1

Φ\Phi is injective. Let i<j<Ni < j < N; since aa is pairwise distinct, aiaja_i \ne a_j, so ai<aja_i < a_j or ai>aja_i > a_j by [L6]. In the first case step 2.2 gives inc(i)inc(j)\mathrm{inc}(i) \ne \mathrm{inc}(j), in the second dec(i)dec(j)\mathrm{dec}(i) \ne \mathrm{dec}(j); either way Φ(i)Φ(j)\Phi(i) \ne \Phi(j), because both run lengths are at least 11, so inc(i)=(inc(i)1)+1\mathrm{inc}(i) = (\mathrm{inc}(i)-1)+1 by [L4] and equal first coordinates would force equal run lengths, and likewise for the second coordinate. As ii and jj were an arbitrary pair of distinct indices, Φ\Phi is injective.

step 2.1step 2.2L4L6
4.1

The contradiction. Composing Φ\Phi with a bijection m×nmnm \times n \to mn from [L5] gives an injection of N=σ(mn)N = \sigma(mn) into mnmn, which [L5] forbids. So the supposition of step 1.1 is untenable, and aa has a strictly increasing sublist of length m+1m+1 or a strictly decreasing sublist of length n+1n+1.

step 2.1step 3.1L5discharge-contradiction

Remarks

  • Where pairwise distinctness is spent. Only in step 3.1, to force one of the two strict comparisons between aia_i and aja_j. Without it a list may repeat a value, and then two positions carrying that value force neither run length to increase.

  • Why a greatest element exists at all. The lengths of runs ending at a fixed position form a nonempty set of naturals bounded by the length of the list, and a nonempty bounded set of naturals has a greatest element; that is derived in the facts from the well-ordering principle alone. No maximum of a finite set of reals is involved, and no choice principle is used, since inc(i)\mathrm{inc}(i) and dec(i)\mathrm{dec}(i) are determined by ii rather than selected.

  • The bound mn+1mn+1 is not improvable, and the witness is a list of mnmn distinct reals with neither long sublist; it is constructed in For all mm and nn there is a list of mnmn pairwise distinct reals with no strictly increasing sublist of length m+1m+1 and no strictly decreasing sublist of length n+1n+1.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

For all mm and nn there is a list of mnmn pairwise distinct reals with no strictly increasing sublist of length m+1m+1 and no strictly decreasing sublist of length n+1n+1

Statement

Let m,nNm, n \in \mathbb{N}. Then there is a pairwise distinct finite list of reals a:(mn)Ra : (mn) \to \mathbb{R} (A finite list of reals, and its strictly increasing and strictly decreasing sublists) with no strictly increasing sublist of length m+1m+1 and no strictly decreasing sublist of length n+1n+1.

Together with the bound mn+1mn+1, this says that mn+1mn+1 is the least length at which the two alternatives become unavoidable.

At m=0m = 0 or n=0n = 0 the list is empty, and there is no sublist of any positive length at all, so the assertion holds for the trivial reason that both required sublists have length at least 11.

Facts & Assumptions

Given: Naturals mm and nn, the finite sets m×nm \times n and mnmn, and the ordered field R\mathbb{R} with the canonical natural ι:NR\iota : \mathbb{N} \to \mathbb{R} (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field).

[L1]

Arithmetic and order of N\mathbb{N}: addition and multiplication are as in Addition of natural numbers and Multiplication of natural numbers; pqp \le q means p+j=qp + j = q for a unique jj, written qpq - p (Order on the natural numbers, Addition is cancellative, Finite sums and finite products of natural numbers, k<nak\sum_{k<n} a_k and k<nak\prod_{k<n} a_k in N\mathbb{N}), and \le is transitive (\le is a linear order on N\mathbb{N}); p<qp<q if and only if p+1qp+1\le q (Discreteness: σ(n)\sigma(n) is the immediate successor); p+k<q+k    p<qp + k < q + k \iff p < q (Order is compatible with addition); addition is commutative (Addition is commutative); σ(b)n=bn+n\sigma(b)\cdot n = b\cdot n + n (Distributivity and the successor law for multiplication); multiplication is monotone in its first factor, since p+d=qp + d = q gives qn=nq=np+nd=pn+dnq\,n = n\,q = n\,p + n\,d = p\,n + d\,n by commutativity and distributivity (Multiplication is commutative, Distributivity and the successor law for multiplication), so pqp \le q implies pnqnp\,n \le q\,n; exactly one of p<qp<q, p=qp=q, q<pq<p holds (Trichotomy of the order on N\mathbb{N}); and k<N    kNk < N \iff k \in N (On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n).

[L3]

An injection between finite sets of equal cardinality is a bijection: it is a bijection onto its image, the image has the same cardinality as the domain, and clause 3 of A subset of a finite set is finite, with BA\lvert B\rvert \le \lvert A\rvert, and equality holds if and only if B=AB = A then makes the image the whole codomain (The cardinality A\lvert A\rvert of a finite set, Injection, surjection, bijection).

[L4]

There is no injection of LL into KK when K<LK < L (The pigeonhole principle on N\mathbb{N}, clause 2).

[L6]

Sublists (A finite list of reals, and its strictly increasing and strictly decreasing sublists): a sublist of length LL is a strictly increasing s:Lmns : L \to mn, hence injective; it is strictly increasing, respectively decreasing, when its values do the same.

Proof

technique · constructive
1.1

If m=0m=0 or n=0n=0, then mn=0mn=0 and the empty list has no sublist of the positive lengths m+1m+1 and n+1n+1, proving the assertion in these boundary cases. Hence for the construction below assume m,n1m,n\ge1.

givenL1L2
1.2

The index bijection. Define β:m×nN\beta : m \times n \to \mathbb{N} by β(b,j):=bn+j\beta(b,j) := b\,n + j. Its values lie in mnmn: from j<nj < n and b<mb < m we get j+1nj + 1 \le n and b+1mb + 1 \le m, so β(b,j)+1=bn+(j+1)bn+n=σ(b)nmn\beta(b,j) + 1 = bn + (j+1) \le bn + n = \sigma(b)\cdot n \le mn by [L1], whence β(b,j)<mn\beta(b,j) < mn.

L1construct
1.3

β\beta is injective. Suppose β(b,j)=β(b,j)\beta(b,j) = \beta(b',j') with (b,j),(b,j)m×n(b,j), (b',j') \in m \times n. If b<bb < b' then σ(b)b\sigma(b) \le b', so β(b,j)<bn+n=σ(b)nbnβ(b,j)\beta(b,j) < bn + n = \sigma(b)\,n \le b'n \le \beta(b',j') by [L1], a contradiction; symmetrically b<bb' < b is impossible, so b=bb = b' by [L1], and then j=jj = j' by cancellation.

L1construct
2.1

The list. By [L2] and [L3], the injection β\beta of step 1.3 is a bijection of m×nm \times n onto mnmn, so every index i<mni < mn is β(b,j)\beta(b,j) for exactly one pair, and aβ(b,j)  :=  ι(bn+nj)(b<m, j<n)a_{\beta(b,j)} \;:=\; \iota\big(b\,n + n - j\big) \qquad (b<m,\ j<n) defines a list a:(mn)Ra : (mn) \to \mathbb{R}. Write blk(β(b,j)):=b\mathrm{blk}(\beta(b,j)) := b for the block of an index.

step 1.2step 1.3L2L3construct
3.1

Inside a block the values decrease. Let b<mb < m and j<j<nj < j' < n. Then β(b,j)<β(b,j)\beta(b,j) < \beta(b,j') by [L1], while nj1n - j' \ge 1 and nj=(nj)+(jj)n - j = (n-j') + (j'-j) with jj1j'-j \ge 1, so nj<njn-j' < n-j and hence aβ(b,j)<aβ(b,j)a_{\beta(b,j')} < a_{\beta(b,j)} by [L1] and [L5].

step 2.1L1L5
3.2

Across blocks the values increase, and the block is monotone in the index. Let b<b<mb < b' < m and j,j<nj, j' < n. Then bn+njbn+n=σ(b)nbn<bn+(nj)bn + n - j \le bn + n = \sigma(b)\,n \le b'n < b'n + (n - j'), the last step because nj1n - j' \ge 1; so aβ(b,j)<aβ(b,j)a_{\beta(b,j)} < a_{\beta(b',j')} by [L5]. Moreover β(b,j)<β(b,j)\beta(b,j) < \beta(b',j'), by the computation of step 1.3; equivalently, blk\mathrm{blk} is nondecreasing along the index order.

step 1.3step 2.1L1L5
4.1

The list is pairwise distinct. Two indices with different blocks carry different values by step 3.2, and two indices in the same block carry different values by step 3.1; since every index has exactly one block by step 2.1, distinct indices carry distinct values.

step 2.1step 3.1step 3.2
4.2

No strictly increasing sublist of length m+1m+1. Let s:Lmns : L \to mn be a strictly increasing sublist. The map blks:Lm\mathrm{blk}\circ s : L \to m is injective: if p<q<Lp < q < L had blk(s(p))=blk(s(q))\mathrm{blk}(s(p)) = \mathrm{blk}(s(q)), then s(p)<s(q)s(p) < s(q) lie in one block, so as(p)>as(q)a_{s(p)} > a_{s(q)} by step 3.1, contradicting that the sublist increases. Hence LmL \le m by [L4] and natural-order trichotomy, so Lm+1L \ne m+1.

step 2.1step 3.1L1L4L6
4.3

No strictly decreasing sublist of length n+1n+1. Let s:Lmns : L \to mn be a strictly decreasing sublist and let p<q<Lp < q < L. Then s(p)<s(q)s(p) < s(q), so blk(s(p))blk(s(q))\mathrm{blk}(s(p)) \le \mathrm{blk}(s(q)) by step 3.2; and blk(s(p))<blk(s(q))\mathrm{blk}(s(p)) < \mathrm{blk}(s(q)) would give as(p)<as(q)a_{s(p)} < a_{s(q)} by step 3.2, contradicting that the sublist decreases. Thus, if L>0L>0, all the s(p)s(p) lie in the block of s(0)s(0), say s(p)=β(b,jp)s(p)=\beta(b,j_p), and pjpp\mapsto j_p is injective into nn because ss is injective and β\beta is a bijection. If L=0L=0, the empty map is already an injection LnL\to n. In either case [L4] and natural-order trichotomy give LnL\le n, so Ln+1L\ne n+1.

step 1.1step 2.1step 3.2L1L4L6
5.1

Together with the boundary cases in step 1.1, the list of step 2.1 is therefore a pairwise distinct list of mnmn reals with no strictly increasing sublist of length m+1m+1 and no strictly decreasing sublist of length n+1n+1, which is the assertion.

step 1.1step 4.1step 4.2step 4.3discharge-construct

Remarks

  • The two block counts are not interchangeable. The construction uses mm blocks of nn terms each. An increasing sublist meets each block at most once, so its length is bounded by the number of blocks, mm; a decreasing sublist lies inside one block, so its length is bounded by the block size, nn. Exchanging the roles would bound the increasing sublists by nn and the decreasing ones by mm, which is the sharpness statement for the pair (n,m)(n,m) and not for (m,n)(m,n).

  • Why the values are written through ι\iota. The terms of a list of reals are real numbers, and bn+njbn+n-j is a natural number, which is a set and not an element of R\mathbb{R}. The strict monotonicity of ι\iota is what transports the comparisons between the naturals into comparisons between the terms.

  • The degenerate cases are discharged first. If m=0m = 0 or n=0n = 0 then m×nm \times n and mnmn are both empty, and step 1.1 proves directly that the empty list has neither required positive-length sublist.

RemarkRemark: AI-generatedProof: Not applicableverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

The conventions this page fixes: the empty intersection, where the counts live, the first index of every sum, and what the declared prerequisites do not supply

This item is the page's ledger: every convention the page fixes, with the item that fixes it, and a statement of what this page's declared prerequisites do not supply. It continues Conventions fixed on this page, and what counting is deliberately not done here, the same kind of ledger for the page finite-counting-and-binomial-coefficients, which is this page's declared prerequisite.

Conventions fixed here

The empty intersection is the ambient set, and the ambient set is part of the data. A finite family (Ai)iI(A_i)_{i \in I} of subsets of a finite set XX, the intersections AJA_J for JIJ \subseteq I, and the convention A=XA_\varnothing = X fixes a finite XX together with the family (Ai)iI(A_i)_{i \in I} and stipulates A=XA_\varnothing = X. This is a stipulation and not a theorem: for nonempty JJ the intersection is determined by the family, and for J=J = \varnothing the description "belongs to every AiA_i with iJi \in J" is satisfied by everything, so it determines nothing without an ambient set to be relative to. The clause supplies the J=J = \varnothing term in the complementary form of Inclusion and exclusion: ιiIAi=JI(1)J+1ιAJ\iota\lvert\bigcup_{i \in I} A_i\rvert = \sum_{\varnothing \ne J \subseteq I}(-1)^{\lvert J\rvert + 1}\,\iota\lvert A_J\rvert, together with the complementary form counting the elements in none of the AiA_i and in later sieves whenever an intersection must also be identified at the empty subfamily.

Counts live in N\mathbb{N}; every alternating identity lives in R\mathbb{R}. A cardinality is a natural number, a natural number here is a set, and a set is not an element of R\mathbb{R}. Every identity on this page that uses a negative summand, and every one that divides counts, is therefore stated in R\mathbb{R} with the counts carried across by the canonical natural ι\iota (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field), and read back through the injectivity of ι\iota where the conclusion is about natural numbers. Truncated natural differences such as n1n-1 and n2n-2 remain in N\mathbb N and are not negative summands.

Every index range starts at 00, and the lower-bound hypotheses on this page exist only because of it. j<m+1(1)jι(tj)=(1)mι(t1m)\sum_{j<m+1}(-1)^{j}\,\iota\binom{t}{j} = (-1)^{m}\,\iota\binom{t-1}{m} for every t1t \ge 1 and every mm carries t1t \ge 1; without it the identity fails at t=0t = 0 and m=1m = 1. ι(Dn)=ι(n)ι(Dn1)+(1)n\iota(D_n) = \iota(n)\,\iota(D_{n-1}) + (-1)^{n} for n1n \ge 1, and Dn=(n1)(Dn1+Dn2)D_n = (n-1)(D_{n-1} + D_{n-2}) for n2n \ge 2 carries n1n \ge 1 in its first clause, because the identity n!=(n1)!nn! = (n-1)!\cdot n that proves it fails at n=0n = 0 under the truncated difference, and n2n \ge 2 in its second, because that clause applies the first one at n1n-1. m/n\lceil m/n \rceil for naturals mm and n1n \ge 1: the least qNq \in \mathbb{N} with mnqm \le n q carries n1n \ge 1, without which the set it takes a least element of can be empty.

00=10^{0} = 1, and the place it is spent is named. The convention is the base clause of the recursion in Exponentiation of natural numbers, mnm^{n}, and its agreement with the integer power in R\mathbb{R}, not an import. In The number of surjections from an nn-element set onto a kk-element set is i<k+1(1)i(ki)(ki)n\sum_{i<k+1}(-1)^{i}\binom{k}{i}(k-i)^{n}, read in R\mathbb{R} through ι\iota it is what makes the formula correct at n=0n = 0 and k=0k = 0, where the empty function is the unique surjection \varnothing \to \varnothing and the formula returns ι(00)\iota(0^{0}). At n=0n = 0 with k1k \ge 1 the same formula returns the full alternating row sum, which vanishes only because k1k \ge 1; and at k=0k = 0 with n1n \ge 1 it returns ι(0n)\iota(0^{n}), which is 00 for the same reason read the other way. Powers of 1-1 are the real powers of Integer powers ama^m throughout, since 1-1 is not a natural number.

A sum over a finite index set is what all of this is written in. The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form is the notion used for every sum whose index set is a set of subsets, a set of elements or a relation's fibre family, and its value is independent of the enumeration chosen. The facts about it that are used constantly and are not clauses of it are the bridge ι(N)=Rι\iota\big(\sum^{\mathbb{N}}\big) = \sum^{\mathbb{R}}\iota over such an index set, and the additivity, scaling and monotonicity laws over such an index set. Both are derived, in the Facts of the items that use them, from the corresponding clauses about a sum over an initial segment together with the enumeration that defines the sum over an index set.

A relation, not a matrix. A relation RX×YR \subseteq X \times Y between finite sets, its row fibres RxR_x and its column fibres RyR^y sets up a subset of a product of two finite sets, its two fibre families and their slice partitions. Double counting: xXRx=R=yYRy\sum_{x \in X}\lvert R_x\rvert = \lvert R\rvert = \sum_{y \in Y}\lvert R^y\rvert for a relation between finite sets states the resulting equality of the two fibre sums with the size of the relation, and nothing more.

Fibres of a function. If A>kB\lvert A\rvert > k\lvert B\rvert then every f:ABf : A \to B has a fibre with more than kk elements, and for nonempty BB some fibre has at least A/B\lceil \lvert A\rvert / \lvert B\rvert\rceil elements is stated about the fibres f1[{b}]f^{-1}[\{b\}] of a function between finite sets. Its two clauses are one argument: the ceiling form is the counting form applied at the single index below the ceiling, which is why the ceiling was defined by minimality.

What this page's declared prerequisites do not supply

Each of the following is a statement about what this page may cite, and about nothing else.

  • No floor and no ceiling as general notions, and no division with remainder. m/n\lceil m/n \rceil for naturals mm and n1n \ge 1: the least qNq \in \mathbb{N} with mnqm \le n q defines only the least qq with mnqm \le nq, for naturals mm and n1n \ge 1. It is not defined for a real argument, it produces no remainder, and nothing here extends it.

  • No divisibility. No result on this page is stated in terms of one natural number dividing another, and no argument uses such a relation.

  • No graph vocabulary. Nothing among this page's declared prerequisites defines a graph, a vertex or an edge. The results that would usually be stated about graphs are stated instead about a finite set carrying a symmetric irreflexive relation, which is exactly what their proofs use.

  • No probability. Nothing among this page's declared prerequisites defines a probability space, a measure or an expectation. The averaging principle is a statement about a quotient of two counts, and the hat-check ratio on the companion page is a quotient of two counts; neither is called a probability and neither is treated as one.

  • No symmetric group. The derangement number DnD_n: the number of bijections of an nn-element set with no fixed point counts a set of bijections. No group structure on that set is defined or used.

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-07-29 (claude-fable-5)Open item page →

FALSE: the real-valued three-set inclusion-exclusion identity remains true after deleting the triple-intersection term

Statement

FALSE. The statement

for all finite sets AA, BB, CC, in R\mathbb{R}, ιABC=ιA+ιB+ιCιABιACιBC.\iota\lvert A \cup B \cup C\rvert = \iota\lvert A\rvert + \iota\lvert B\rvert + \iota\lvert C\rvert - \iota\lvert A \cap B\rvert - \iota\lvert A \cap C\rvert - \iota\lvert B \cap C\rvert .

This is the sieve identity of Inclusion and exclusion: ιiIAi=JI(1)J+1ιAJ\iota\lvert\bigcup_{i \in I} A_i\rvert = \sum_{\varnothing \ne J \subseteq I}(-1)^{\lvert J\rvert + 1}\,\iota\lvert A_J\rvert, together with the complementary form counting the elements in none of the AiA_i for a family of three sets with the term at the triple intersection deleted. The identity is correct only when the triple term +ιABC+\,\iota\lvert A \cap B \cap C\rvert is present, and the claim above is refuted by a family in which that term is not 00.

Facts & Assumptions

Given: The one-element set A:=B:=C:={0}A := B := C := \{0\}, taken inside the ambient set X:={0}X := \{0\}, and the canonical natural ι\iota (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field).

[L1]
[L3]

(1)0=1(-1)^{0} = 1 and (1)p+1=(1)p(-1)^{p+1} = -(-1)^{p}, so (1)2=1(-1)^{2} = 1, (1)3=1(-1)^{3} = -1 and (1)4=1(-1)^{4} = 1 (Integer powers ama^m).

[L4]

R\mathbb{R} is an ordered field, so 101 \ne 0 and its arithmetic is available (Ordered field, Field).

Refutation

technique · constructive
1.1

Take I:=3={0,1,2}I := 3 = \{0,1,2\}, X:={0}X := \{0\} and A0:=A1:=A2:={0}A_0 := A_1 := A_2 := \{0\}, so that the family of the displayed claim is A=A0A = A_0, B=A1B = A_1, C=A2C = A_2. Every intersection of a nonempty subfamily is {0}\{0\}, and the union is {0}\{0\}.

givenconstruct
1.2

Every set occurring in the computation is {0}\{0\}, so by [L1] each of ιA\iota\lvert A\rvert, ιB\iota\lvert B\rvert, ιC\iota\lvert C\rvert, ιAB\iota\lvert A \cap B\rvert, ιAC\iota\lvert A \cap C\rvert, ιBC\iota\lvert B \cap C\rvert, ιABC\iota\lvert A \cap B \cap C\rvert and ιABC\iota\lvert A \cup B \cup C\rvert equals 11.

L1
2.1

The right-hand side of the displayed claim is therefore 1+1+1111=01 + 1 + 1 - 1 - 1 - 1 = 0, while its left-hand side is 11. Since 101 \ne 0 in R\mathbb{R} by [L4], the claim is false at this family.

step 1.1step 1.2L4
3.1

The true identity at the same family. By [L2] the sieve sum has the three singleton terms with sign (1)2=1(-1)^{2} = 1, the three two-element terms with sign (1)3=1(-1)^{3} = -1 and the one three-element term with sign (1)4=1(-1)^{4} = 1, so it reads 1+1+1111+1=11+1+1-1-1-1+1 = 1, which is ιABC\iota\lvert A \cup B \cup C\rvert. The deleted triple term is exactly the discrepancy found in step 2.1.

step 1.2step 2.1L2L3discharge-construct

Remarks

  • The claim is the sieve truncated at depth 22, and the Bonferroni inequalities say what such a truncation does in general: an even truncation under-estimates. Here it under-estimates by 11, and the claim asserts equality, so the failure is in the direction the inequality predicts.

  • The witness is as small as it can be. Three sets are needed for a triple intersection to exist, and the discrepancy is the size of that intersection, so any family with a nonempty triple intersection refutes the claim. Taking all three sets equal to a single point makes every cardinality in the computation equal to 11.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)Open item page →

FALSE: truncating the sieve at a fixed depth of at least two gives the exact size of the union

Statement

FALSE. The statement

for every sieve family XX, II, (Ai)iI(A_i)_{i \in I} and every m2m \ge 2, ιiIAi=Tm,\iota\Big\lvert\bigcup_{i \in I}A_i\Big\rvert = T_m,

with SjS_j and TmT_m as in Truncating the sieve at an odd depth over-estimates the size of the union and truncating it at an even depth under-estimates it.

The claim reads the Bonferroni inequalities as if a truncation at any depth beyond the first were already exact. What is true is that the truncation is an over-estimate at an odd depth and an under-estimate at an even depth, and that it is guaranteed to become exact once the depth reaches I\lvert I\rvert, though special families may become exact earlier; the hypothesis m2m \ge 2 does nothing to close that gap when I\lvert I\rvert exceeds mm.

Facts & Assumptions

Given: The ambient set X:={0}X := \{0\}, the index set I:=3={0,1,2}I := 3 = \{0,1,2\}, the family A0:=A1:=A2:={0}A_0 := A_1 := A_2 := \{0\}, and the truncation depth m:=2m := 2.

[L1]

{0}=1\lvert\{0\}\rvert = 1, ι(1)=1\iota(1) = 1 and ι(3)=3\iota(3) = 3 (The cardinality A\lvert A\rvert of a finite set, The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field).

[L3]

Sj=J[I]jιAJS_j = \sum_{J \in [I]^{j}}\iota\lvert A_J\rvert and Tm=i<m(1)iSi+1T_m = \sum_{i<m}(-1)^{i}S_{i+1}; a constant real summand gives pSλ=ι(S)λ\sum_{p \in S}\lambda = \iota(\lvert S\rvert)\lambda (Truncating the sieve at an odd depth over-estimates the size of the union and truncating it at an even depth under-estimates it, The sum iSai\sum_{i \in S} a_i over a finite index set, and its product form, clause (c), Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L4]

(1)0=1(-1)^{0} = 1 and (1)1=1(-1)^{1} = -1 (Integer powers ama^m); R\mathbb{R} is an ordered field, so 101 \ne 0 (Ordered field, Field).

[L5]

Clause 3 of Truncating the sieve at an odd depth over-estimates the size of the union and truncating it at an even depth under-estimates it, which says Tm=ιiIAiT_m = \iota\lvert\bigcup_{i \in I}A_i\rvert once mIm \ge \lvert I\rvert.

Refutation

technique · constructive
1.1

The witness. With X={0}X = \{0\} and A0=A1=A2={0}A_0 = A_1 = A_2 = \{0\}, every AJA_J with JIJ \subseteq I is {0}\{0\}, and the union is {0}\{0\}, so ιiIAi=1\iota\lvert\bigcup_{i \in I}A_i\rvert = 1 by [L1].

givenconstruct
2.1

The first two truncation levels. Each summand ιAJ\iota\lvert A_J\rvert is 11 by step 1.1, so S1=ι[I]11=3S_1 = \iota\lvert [I]^{1}\rvert\cdot 1 = 3 and S2=ι[I]21=3S_2 = \iota\lvert [I]^{2}\rvert\cdot 1 = 3 by [L2] and the constant clause of [L3]; likewise S3=1S_3 = 1.

L1L2L3
3.1

Therefore T2=(1)0S1+(1)1S2=33=0T_2 = (-1)^{0}S_1 + (-1)^{1}S_2 = 3 - 3 = 0, while ιiIAi=1\iota\lvert\bigcup_{i \in I}A_i\rvert = 1. Since 101 \ne 0 by [L4], the displayed claim fails at this family and at m=2m = 2, which satisfies its hypothesis m2m \ge 2.

step 1.1step 2.1L3L4
4.1

What is true here instead. Clause 2 of Truncating the sieve at an odd depth over-estimates the size of the union and truncating it at an even depth under-estimates it gives ιiAiT2\iota\lvert\bigcup_i A_i\rvert \ge T_2, and indeed 101 \ge 0; and T3=33+1=1T_3 = 3 - 3 + 1 = 1, which is the exact value, in agreement with clause 3 of that theorem at m=3=Im = 3 = \lvert I\rvert. So the truncation becomes exact one level later than the claim asserts, and the gap at depth 22 is the whole content of the failure.

step 2.1step 3.1L3L4L5discharge-construct

Remarks

  • The claim is not repaired by raising the fixed depth. For any fixed mm the same all-equal family with II taken to have more than mm elements refutes it again; clause 3 guarantees exactness once the depth reaches I\lvert I\rvert, while other families may already be exact sooner. That is why the true uniform guarantee fixes the depth relative to I\lvert I\rvert rather than absolutely.

  • The direction of the error is not accidental. Depth 22 is an even truncation, and an even truncation under-estimates, so the truncated value is below the truth rather than above it. A witness at depth 33 would over-shoot instead.

False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)verified 2026-07-29 (claude-fable-5)Open item page →

FALSE: every list of mnmn pairwise distinct reals has a strictly increasing sublist of length m+1m+1 or a strictly decreasing sublist of length n+1n+1

Statement

FALSE. The statement

for all m,nNm, n \in \mathbb{N}, every pairwise distinct finite list of reals of length mnmn has a strictly increasing sublist of length m+1m+1 or a strictly decreasing sublist of length n+1n+1 (A finite list of reals, and its strictly increasing and strictly decreasing sublists).

This is Every list of mn+1mn+1 pairwise distinct reals has a strictly increasing sublist of length m+1m+1 or a strictly decreasing sublist of length n+1n+1 with the length lowered from mn+1mn+1 to mnmn. The true theorem is sharp, so lowering the length by one destroys it, and it does so at every pair (m,n)(m,n) rather than at some exceptional pair.

Facts & Assumptions

Given: The naturals mm and nn, and lists of reals with their sublists as in A finite list of reals, and its strictly increasing and strictly decreasing sublists.

[L1]

For all m,nNm, n \in \mathbb{N} there is a pairwise distinct list of reals of length mnmn with no strictly increasing sublist of length m+1m+1 and no strictly decreasing sublist of length n+1n+1 (For all mm and nn there is a list of mnmn pairwise distinct reals with no strictly increasing sublist of length m+1m+1 and no strictly decreasing sublist of length n+1n+1).

[L2]

Every pairwise distinct list of reals of length mn+1mn+1 has a strictly increasing sublist of length m+1m+1 or a strictly decreasing sublist of length n+1n+1 (Every list of mn+1mn+1 pairwise distinct reals has a strictly increasing sublist of length m+1m+1 or a strictly decreasing sublist of length n+1n+1).

[L3]

22=42 \cdot 2 = 4 (Multiplication of natural numbers, Order on the natural numbers), and the terms of a list are elements of the ordered field R\mathbb{R} (Ordered field).

Refutation

technique · constructive
1.1

Read the displayed claim at m=n=2m = n = 2: every pairwise distinct list of reals of length 44 would have a strictly increasing sublist of length 33 or a strictly decreasing sublist of length 33.

givenL3
1.2

By [L1] at m=n=2m = n = 2 there is a pairwise distinct list of reals of length 22=42\cdot 2 = 4 with no strictly increasing sublist of length 33 and no strictly decreasing sublist of length 33.

L1L3construct
2.1

That list refutes the reading of step 1.1, so the displayed claim is false. The same argument runs at every pair (m,n)(m,n), since [L1] produces a witness for each of them; the claim therefore fails everywhere, not at an exceptional pair.

step 1.1step 1.2L1
3.1

What survives is [L2]: the conclusion holds once the length is raised to mn+1mn+1. So the least length at which the alternative becomes unavoidable is mn+1mn+1, and the claim above is exactly the assertion that it is mnmn.

step 2.1L1L2discharge-construct

Remarks

Sources