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 number of diagonal paths from to is for the natural number with , and when no such exists
Statement
Let and , and let be the set of diagonal lattice paths of length from whose height function ends at (Diagonal lattice paths with steps and , and the height function).
-
Suppose divides and , and let be the natural number with ; then and
-
If either condition fails then , so its cardinality is .
In both cases the set is finite, and the count depends on and only through the difference .
Facts & Assumptions
Given: integers and and a natural number .
A diagonal path of length from has with and ; with the number of up-steps its endpoint height is ; and is nonempty exactly when divides and (Diagonal lattice paths with steps and , and the height function).
For and , replacing by and by is a bijection (The two step sets describe the same objects: , is a bijection matching the diagonal with the level ).
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 ; and a finite set has cardinality exactly when it is empty (The cardinality of a finite set).
is the number of -element subsets of the natural number , and (The set of -element subsets and the binomial coefficient ).
Proof
Subtracting the constant leaves every difference unchanged and sends to and to , and adding it back inverts the operation; so it is a bijection and the two sets have the same cardinality.
If does not divide , or if lies outside the range from to , then is empty and its cardinality is , which is clause 2.
If the two conditions hold, let be the natural number with and put . From and one gets , and because .
By step 2.2 and [L1] the set is in bijection with , which by [L2] is finite with elements; transporting along that bijection and along the translation of step 1.1 gives clause 1. At the conditions force and , and the one empty path is counted by ; at they force , and the one all-up path is counted by .
Remarks
-
The vanishing clause is used, not decorative. The reflection principle below subtracts one of these counts from another, and both the parity and the range conditions can fail for the reflected endpoint while holding for the original; the difference is correct only because the count is then rather than undefined.
-
Why the answer is stated through rather than as a quotient. The natural number with exists exactly under the stated hypotheses, and writing would name an element of a field where the hypothesis of the statement is that the halving is exact in .
Depends on
- The two step sets describe the same objects: $U\mapsto N$, $D\mapsto E$ is a bijection matching the diagonal $y=x$ with the level $0$
- $\lvert\mathcal{M}((0,0),(m,n))\rvert=\binom{m+n}{n}$
- Diagonal lattice paths with steps $U=(1,1)$ and $D=(1,-1)$, and the height function
- The set $[A]^{k}$ of $k$-element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$
- $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
Used by
Dependency tree · two levels
30 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)