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.
for , and for
Statement
Let be the derangement numbers (The derangement number : the number of bijections of an -element set with no fixed point) and the canonical natural (The canonical natural of a field). Then:
- For every , in ,
- For every , in ,
All differences are the truncated ones (Finite sums and finite products of natural numbers, and in ), 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 and its consequence , both of which fail at under the truncated difference, where is ; so is its first legal index, and there it reads . Clause 2 is derived by applying clause 1 twice, at and at , so it needs ; its first legal index is , where it reads . Under the truncated difference the two displayed formulas happen also to be true at and at respectively, both sides being in the first case and in the second, but neither of those readings is proved here and neither is claimed.
Facts & Assumptions
Given: A natural number with in clause 1 and in clause 2; the abbreviation , so that (Order on the natural numbers, Finite sums and finite products of natural numbers, and in , Every nonzero natural number is a successor).
The derangement formula: for every (, with the term at equal to and ).
Recursion clause of the real finite sum: (Finite sums and finite products, by recursion, Laws of finite sums and finite products).
Factorials: , so when ; and for every (The factorial and the falling factorial , defined by recursion in ).
is additive and multiplicative with , and it is injective (Laws of finite sums and products in , and , clauses 0 and 7, The canonical natural of a field). In particular when , and .
Powers of : and (Integer powers ).
is an ordered field, so subtraction and division by a nonzero element are available (Ordered field, Field).
Proof
Let and put , so . Then by [L3], hence by [L4], and both and are nonzero.
The formula at . By [L1] and , .
Splitting the sum at its last index. By [L2], .
Clause 1. Multiplying step 1.3 by and using [L1] at , step 1.1 and step 1.2, .
Now let , so that and . Applying step 2.1 at in place of gives , hence ; and by [L5], so .
Clause 2. Substituting step 3.1 into step 2.1, , using from [L4]; the right-hand side is by the additivity and multiplicativity of , so by injectivity.
Remarks
-
Clause 2 is derived from clause 1 and not from the formula. Two instances of clause 1, at and at , are enough, and that is why clause 2 begins one index later: the second instance needs .
-
Why clause 1 is stated in and clause 2 in . Clause 1 carries the term , which is not a natural number when is odd. Clause 2 has no signs left in it, both sides are counts, and injectivity of carries the identity back into where it belongs.
-
The truncated difference is why the hypotheses have to be written out. Under it the symbols and never become ill formed: at the first reads and at the second reads as well. So a reader cannot tell from the shape of the formula where it stops being proved, and the ranges and have to be stated rather than inferred.
Depends on
- $\iota(D_n) = \iota(n!)\sum_{i<n+1}(-1)^{i}/\iota(i!)$, with the term at $i = 0$ equal to $1$ and $D_0 = 1$
- The derangement number $D_n$: the number of bijections of an $n$-element set with no fixed point
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
- Integer powers $a^m$
- Finite sums and finite products, by recursion
- Laws of finite sums and finite products
- Laws of finite sums and products in $\mathbb{N}$, and $\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k)$
- Order on the natural numbers
- Finite sums and finite products of natural numbers, $\sum_{k<n} a_k$ and $\prod_{k<n} a_k$ in $\mathbb{N}$
- Every nonzero natural number is a successor
- Ordered field
- Field
Used by
- All nine derangements of a four-element set listed, and the count checked against the formula and both recurrences Example
- The ratio ι(Dₙ)/ι(n!) computed for small n as a quotient of two counts, with no probability space claimed Example
- 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 Remark
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 89 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
- Derangement (Wikipedia) (standard reference, not scraped)
- Rencontres numbers (Wikipedia) (standard reference, not scraped)
- Principle of Inclusion and Exclusion (Open Math Books) (standard reference, not scraped)