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 ratio computed for small as a quotient of two counts, with no probability space claimed
Example
For consider the real number
the quotient of the count of derangements of an -element set (The derangement number : the number of bijections of an -element set with no fixed point) by the count of all its bijections, (The factorial and the falling factorial , defined by recursion in ). The quotient is legitimate because . Dividing the derangement formula by gives
so is the truncated alternating sum itself. Its first values, obtained from , , and the first recurrence ( for , and for ), are
This is a ratio of two counts and nothing else. Nothing among this page's declared prerequisites defines a probability space, a measure or an expectation, so is not called a probability here and no statement about random behaviour is made. What is asserted is exactly that the numerator counts the fixed-point-free bijections, that the denominator counts all of them, and that the quotient is the displayed alternating sum.
Facts & Assumptions
Given: The derangement numbers , the factorials , and the canonical natural (The canonical natural of a field).
The derangement formula: (, with the term at equal to and ).
The first recurrence: for ; and , , ( for , and for , The derangement number : the number of bijections of an -element set with no fixed point).
is an ordered field, so division by a nonzero element is available and the displayed arithmetic is legitimate (Ordered field, Field); and (Integer powers ); and real finite sums obey the recursion clause (Finite sums and finite products, by recursion, Laws of finite sums and finite products).
Factorials: , , , , , , (The factorial and the falling factorial , defined by recursion in ).
Verification
The quotient form. Dividing the identity of [L1] by the nonzero gives for every .
The derangement numbers up to . From and [L3]: , , and ; since is injective these are the natural numbers , , , .
The tabulated ratios. Dividing the base values in [L3] and the values from step 1.2 by the factorials of [L5] gives , , , , , and .
A cross-check at through step 1.1: , which is .
So is the truncated alternating sum, and its values through are as tabulated.
Remarks
-
The alternation is visible in the table. is below , which is above , which is below ; each successive value differs from the previous one by the single term , whose sign alternates and whose size decreases.
-
No limit is claimed. The quotient is computed at each from two counts, and nothing here asserts convergence or names a limiting value; the exponential function that would be needed to state such a limit is not among this page's declared prerequisites.
-
Why the division is legitimate at every , including . The denominator is and is never , its recursion starting at and multiplying by nonzero successors.
Depends on
- The derangement number $D_n$: the number of bijections of an $n$-element set with no fixed point
- $\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$
- $\iota(D_n) = \iota(n)\,\iota(D_{n-1}) + (-1)^{n}$ for $n \ge 1$, and $D_n = (n-1)(D_{n-1} + D_{n-2})$ for $n \ge 2$
- 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
- Ordered field
- Field
- Laws of finite sums and products in $\mathbb{N}$, and $\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k)$
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: 89 results over 29 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)
- Derangements (OpenText at the University of Lethbridge) (standard reference, not scraped)