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.
Bertrand's ballot problem: for the orderings in which the first candidate is strictly ahead throughout satisfy
Statement
Let with . A count in which the first candidate receives votes and the second votes, the votes being read in order, is recorded by a diagonal lattice path of length from whose step word has exactly letters , one for each vote for the first candidate; such a path ends at height (Diagonal lattice paths with steps and , and the height function). The first candidate is strictly ahead throughout when the height after each of the votes is at least . Write
Then is finite and, in ,
Facts & Assumptions
Given: natural numbers , so and ; and the set above.
A diagonal path of length from is the same datum as a function with and for ; with the number of up-steps its endpoint height is ; and it stays strictly above the level when for every (Diagonal lattice paths with steps and , and the height function).
For , and , : if divides and , and is the natural number with , then the set of paths in staying strictly above level is finite and its cardinality satisfies (The reflection principle: paths from to staying strictly above level are counted by a difference of two binomial coefficients, clause 2).
For with : in ( for ; hence , the quotient is a natural number, and ).
for every , and (The factorial and the falling factorial , defined by recursion in ).
For all with : if then (Cancellation for multiplication by a nonzero factor).
for , and (The set of -element subsets and the binomial coefficient ).
For : is a bijection if and only if there is a function with and ( is a bijection if and only if there is a function with and ; such a is unique, equals the inverse relation , and is itself a bijection).
If is finite and is a bijection then is finite and (The cardinality of a finite set).
Proof
For the first step is forced upward: and , while , so .
Two identities in , with . First, : since and , and since and , [L2] gives and ; multiplying the first by and using from [L3] makes both left sides equal, and cancelling the nonzero factor by [L3] and [L4] gives the identity. Second, : when both sides are , since then and by [L5]; and when then with , so [L2] gives and , and the same multiplication by and cancellation of gives it.
Shifting the index by one is a bijection from onto the set of paths in that stay strictly above the level : given , put for , so by step 1.1, , consecutive values differ by in absolute value, and ; conversely, given such an , put and for , which has and the remaining differences those of , ends at , and has for . The two constructions undo one another, so [L6] and [L7] apply and .
Apply [L1] with , , and : the hypotheses and hold because , and is even with , so and ; also since . Hence .
Multiplying step 3.1 by and substituting the two identities of step 1.2 gives , and since this is exactly . At it reads , so by [L4], matching the single all-up path; at , it reads , so , the one path with step word .
Remarks
-
The quotient form. The identity of the statement is an identity of natural numbers. Reading each natural number as its canonical natural in (The canonical natural of a field) and dividing by the nonzero real turns it into the familiar ; the multiplicative form is the one proved, and the division is legitimate only because , which needs or at least .
-
Why and not . With the height ends at , so the last vote brings the count level and the first candidate is not strictly ahead throughout; the count is then , while the right-hand side is as well, so the identity survives but says nothing. The interesting weak form, in which the first candidate is merely never behind, is a separate statement.
Depends on
- The reflection principle: paths from $(0,a)$ to $(n,b)$ staying strictly above level $c$ are counted by a difference of two binomial coefficients
- Diagonal lattice paths with steps $U=(1,1)$ and $D=(1,-1)$, and the height function
- $\binom{n}{k}\,k!\,(n-k)! = n!$ for $k \le n$; hence $\binom{n}{k}\,k! = n^{\underline{k}}$, the quotient $n!/(k!(n-k)!)$ is a natural number, and $\binom{n}{k} = \binom{n}{n-k}$
- The set $[A]^{k}$ of $k$-element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- Cancellation for multiplication by a nonzero factor
- $f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = \Delta_A$ and $f \circ g = \Delta_B$; such a $g$ is unique, equals the inverse relation $f^{-1}$, and is itself a bijection
- The cardinality $\lvert A\rvert$ of a finite set
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
Used by
Dependency tree · two levels
52 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
- C. Krattenthaler, "Lattice Path Enumeration", ch. 10 of the Handbook of Enumerative Combinatorics, §10.3 (standard reference, not scraped)
- A. Postnikov (notes by A. Lin), MIT 18.212 Algebraic Combinatorics, Spring 2019 (standard reference, not scraped)