Alphabeta MathHow 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 Lehmer code gives again
Statement
For every ,
Facts & Assumptions
Given: The Lehmer-code bijection .
The Lehmer code is a bijection (The Lehmer code is a bijection ).
If and are finite then (The product rule: , and ).
Proof
By [L1], equals the cardinality of . The -th factor has cardinality , so repeated use of [L2] shows that the whole product has cardinality .
Therefore . For , both sides equal because the codomain is the empty product.
Depends on
- The Lehmer code is a bijection $S_n\to\prod_{i=1}^{n}\{0,\dots,i-1\}$
- The product rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$, and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
25 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Felix Gotti, MIT 18.211 Combinatorial Analysis, Lecture 5 (standard reference, not scraped)