ExampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

How statement and proof provenance work

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

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

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

The sieve run in full on three explicit finite sets and then on four, with every nonempty intersection listed

Example

Take the ambient set $X := 8 = \{0,1,2,3,4,5,6,7\}$ and the subsets

$A_0 := \{0,1,2,3\}, \qquad A_1 := \{2,3,4,5\}, \qquad A_2 := \{3,4,6\}, \qquad A_3 := \{5,6,7\}.$

First the family $(A_i)_{i \in 3}$ , a sieve family with ambient set $X$ and index set $I := 3$ (A finite family $(A_i)_{i \in I}$ of subsets of a finite set $X$ , the intersections $A_J$ for $J \subseteq I$ , and the convention $A_\varnothing = X$ ). Every intersection $A_J$ for $\varnothing \ne J \subseteq 3$ is listed:

$J$	$A_J$	$\lvert A_J\rvert$
$\{0\}$	$\{0,1,2,3\}$	$4$
$\{1\}$	$\{2,3,4,5\}$	$4$
$\{2\}$	$\{3,4,6\}$	$3$
$\{0,1\}$	$\{2,3\}$	$2$
$\{0,2\}$	$\{3\}$	$1$
$\{1,2\}$	$\{3,4\}$	$2$
$\{0,1,2\}$	$\{3\}$	$1$

The union is $A_0 \cup A_1 \cup A_2 = \{0,1,2,3,4,5,6\}$ , of size $7$ , and the sieve returns $(4+4+3) - (2+1+2) + 1 = 7$ . The complementary form returns $8 - (4+4+3) + (2+1+2) - 1 = 1$ , and indeed $X \setminus (A_0\cup A_1\cup A_2) = \{7\}$ .

Now the family $(A_i)_{i \in 4}$ , with $A_3$ adjoined and $I := 4$ :

$J$	$A_J$	$\lvert A_J\rvert$
$\{0\}$	$\{0,1,2,3\}$	$4$
$\{1\}$	$\{2,3,4,5\}$	$4$
$\{2\}$	$\{3,4,6\}$	$3$
$\{3\}$	$\{5,6,7\}$	$3$
$\{0,1\}$	$\{2,3\}$	$2$
$\{0,2\}$	$\{3\}$	$1$
$\{0,3\}$	$\varnothing$	$0$
$\{1,2\}$	$\{3,4\}$	$2$
$\{1,3\}$	$\{5\}$	$1$
$\{2,3\}$	$\{6\}$	$1$
$\{0,1,2\}$	$\{3\}$	$1$
$\{0,1,3\}$	$\varnothing$	$0$
$\{0,2,3\}$	$\varnothing$	$0$
$\{1,2,3\}$	$\varnothing$	$0$
$\{0,1,2,3\}$	$\varnothing$	$0$

The union is now all of $X$ , of size $8$ , and the sieve returns $(4+4+3+3) - (2+1+0+2+1+1) + (1+0+0+0) - 0 = 14 - 7 + 1 = 8$ . The complementary form returns $8 - 14 + 7 - 1 + 0 = 0$ , and indeed $X \setminus (A_0\cup A_1\cup A_2\cup A_3) = \varnothing$ .

Facts & Assumptions

Given: The ambient set $X = 8$ and the subsets $A_0, A_1, A_2, A_3$ above, together with the two index sets $I = 3$ and $I = 4$ and the canonical natural $\iota$ (The canonical natural $\iota(n) = n \cdot 1_F$ of a field).

[L1]

A listed set with distinct entries has as many elements as entries: if $x_0, \dots, x_{k-1}$ are distinct then $j \mapsto x_j$ is a bijection of $k$ onto $\{x_0,\dots,x_{k-1}\}$ , so that set is finite of cardinality $k$ (The cardinality $\lvert A\rvert$ of a finite set, clauses (a) and (c), Injection, surjection, bijection).

[L2]

For a sieve family with ambient set $X$ , finite index set $I$ , union $U=\bigcup_{i\in I}A_i$ and $A_\varnothing=X$ , the sieve identity and its complementary form are $\iota|U|=\sum_{\varnothing\ne J\subseteq I}(-1)^{|J|+1}\iota|A_J|, \qquad \iota|X\setminus U|=\sum_{J\subseteq I}(-1)^{|J|}\iota|A_J|$ (Inclusion and exclusion: $\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 $A_i$ , A finite family $(A_i)_{i \in I}$ of subsets of a finite set $X$ , the intersections $A_J$ for $J \subseteq I$ , and the convention $A_\varnothing = X$ ).

[L3]

Every $J\subseteq I$ is finite with a unique natural cardinality $|J|\le|I|$ , while $[I]^j=\{J\subseteq I:|J|=j\}$ ; hence the levels $[I]^j$ for $1\le j\le|I|$ are pairwise disjoint and have union $\mathcal P(I)\setminus\{\varnothing\}$ . The sign attached to $J$ is $(-1)^{|J|+1}$ , positive for odd $|J|$ and negative for even $|J|$ (The cardinality $\lvert A\rvert$ of a finite set, A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$ , and equality holds if and only if $B = A$ , The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$ , The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\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, The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form, Integer powers $a^m$ ).

[L4]

$\iota$ is additive and injective, so the arithmetic of the displayed sums may be carried out on the natural numbers and read in $\mathbb{R}$ (Laws of finite sums and products in $\mathbb{N}$ , and $\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k)$ , clauses 0 and 7, Ordered field).

Verification

technique · direct

1.1

The three-set family. $A_0$ , $A_1$ , $A_2$ are subsets of $X = 8$ with $\lvert A_0\rvert = 4$ , $\lvert A_1\rvert = 4$ and $\lvert A_2\rvert = 3$ by [L1], each entry list being strictly increasing and so having distinct entries.

givenL1

1.2

Its intersections. Intersecting the listed sets entry by entry gives $A_{\{0,1\}} = \{2,3\}$ , $A_{\{0,2\}} = \{3\}$ , $A_{\{1,2\}} = \{3,4\}$ and $A_{\{0,1,2\}} = \{3\}$ , of sizes $2$ , $1$ , $2$ and $1$ by [L1].

givenL1

1.3

Its union and complement. An element of $X$ lies in $A_0\cup A_1\cup A_2$ unless it is $7$ , since $0,1,2,3 \in A_0$ , $4,5 \in A_1$ and $6 \in A_2$ while $7$ belongs to none of the three listed sets; so the union is $\{0,1,2,3,4,5,6\}$ , of size $7$ , and its complement in $X$ is $\{7\}$ , of size $1$ .

givenL1

1.4

The four-set family. Adjoining $A_3 = \{5,6,7\}$ , of size $3$ , the remaining intersections are $A_{\{0,3\}} = \varnothing$ , $A_{\{1,3\}} = \{5\}$ , $A_{\{2,3\}} = \{6\}$ , $A_{\{0,1,3\}} = A_{\{0,2,3\}} = A_{\{1,2,3\}} = \varnothing$ and $A_{\{0,1,2,3\}} = \varnothing$ , of sizes $0$ , $1$ , $1$ , $0$ , $0$ , $0$ and $0$ by [L1] and clause (b) of The cardinality $\lvert A\rvert$ of a finite set.

givenL1

1.5

The four-set union. Now $7 \in A_3$ , so the union is all of $X$ , of size $8$ , and its complement in $X$ is empty, of size $0$ .

givenL1

2.1

The sieve for three sets. Grouping by size as in [L3], clause 1 of [L2] reads $\iota\lvert A_0\cup A_1\cup A_2\rvert = \iota(4+4+3) - \iota(2+1+2) + \iota(1) = \iota(11) - \iota(5) + \iota(1) = \iota(7)$ , which matches step 1.3.

step 1.1step 1.2step 1.3L2L3L4

2.2

The complementary form for three sets. Clause 2 of [L2] adds the term at $J = \varnothing$ , which is $\iota\lvert A_\varnothing\rvert = \iota\lvert X\rvert = \iota(8)$ , and reverses every sign, giving $\iota(8) - \iota(11) + \iota(5) - \iota(1) = \iota(1)$ , which matches the complement computed in step 1.3.

step 1.1step 1.2step 1.3L2L3L4

2.3

The sieve for four sets. The singleton terms now sum to $4+4+3+3 = 14$ , the pair terms to $2+1+0+2+1+1 = 7$ , the triple terms to $1+0+0+0 = 1$ and the single four-element term is $0$ ; so clause 1 of [L2] reads $\iota(14) - \iota(7) + \iota(1) - \iota(0) = \iota(8)$ , which matches step 1.5, and clause 2 reads $\iota(8) - \iota(14) + \iota(7) - \iota(1) + \iota(0) = \iota(0)$ , again matching.

step 1.1step 1.2step 1.4step 1.5L2L3L4

3.1

Both families therefore satisfy both forms of the identity, with every intersection exhibited rather than inferred.

step 2.1step 2.2step 2.3∎

Remarks

Adjoining one set changes every level of the sum. Passing from three sets to four adds a singleton term, three pair terms, three triple terms and one four-element term, and the totals at each level move accordingly; what stays fixed is that the alternating combination reproduces the size of the union.
The terms that vanish are not omitted. $A_{\{0,3\}}$ and the three four-element-family triples are empty, so their terms are $0$ ; they are still terms of the sum, and writing them keeps the count of terms at each level equal to the number of subsets of that size, which is what the grouping in [L3] asserts.
Where the complementary form gets its extra term. It runs over all subsets of the index set, including $\varnothing$ , whose term is $\iota\lvert X\rvert$ . That is the only place the ambient set enters the arithmetic, and it is why the ambient set has to be named as part of the family.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

Sources

Inclusion-exclusion principle (Wikipedia) (standard reference, not scraped)
Cardinality (Wikipedia) (standard reference, not scraped)
Guichard, The Inclusion-Exclusion Formula (LibreTexts) (standard reference, not scraped)