TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

$∣ M ((0, 0), (m, n)) ∣ = (\binom{m + n}{n})$

Statement

For all $m, n \in N$ the set $M ((0, 0), (m, n))$ of monotone lattice paths from $(0, 0)$ to $(m, n)$ (Monotone lattice paths with steps $E = (1, 0)$ and $N = (0, 1)$ ) is finite with

$∣ M ((0, 0), (m, n)) ∣ = (\binom{m + n}{n}),$

the binomial coefficient of The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ . More generally, if $a \leq c$ and $b \leq d$ in $Z$ and $m, n \in N$ are the natural numbers with $m = c - a$ and $n = d - b$ , then

$∣ M ((a, b), (c, d)) ∣ = (\binom{m + n}{n}) .$

Facts & Assumptions

Given: natural numbers $m$ and $n$ , and integers $a \leq c$ , $b \leq d$ in the second clause.

[F1]

A monotone lattice path is a lattice path whose steps lie in the step set ${E, N}$ with $E = (1, 0)$ and $N = (0, 1)$ (Monotone lattice paths with steps $E = (1, 0)$ and $N = (0, 1)$ ).

[F2]

For $v \in M ((a, b); ℓ)$ with step word $w$ and $ν (i) = ∣ {j \in N : j < i, w_{j} = N} ∣$ , one has $v (i) = (a + i - ν (i), b + ν (i))$ for $0 \leq i \leq ℓ$ ; hence $v (ℓ) = (c, d)$ if and only if $ν (ℓ) = d - b$ and $ℓ = (c - a) + (d - b)$ (Monotone lattice paths with steps $E = (1, 0)$ and $N = (0, 1)$ ).

[L1]

For a step set $S$ , a point $P$ and $ℓ \in N$ , the map sending a lattice path to its step word is a bijection $L_{S} (P; ℓ) \to S^{ℓ}$ (For each start point the step word is a bijection onto $S^{n}$ ).

[L2]

For a finite set $A$ and $k \in N$ , $[A]^{k}$ is the set of $k$ -element subsets of $A$ , it is finite, and $∣ [A]^{k} ∣ = (\binom{∣ A ∣}{k})$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

[L3]

For $f : A \to B$ : $f$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ( $f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ; such a $g$ is unique, equals the inverse relation $f^{- 1}$ , and is itself a bijection).

[L4]

If $A$ is finite and $f : A \to B$ is a bijection then $B$ is finite and $∣ B ∣ = ∣ A ∣$ (The cardinality $∣ A ∣$ of a finite set).

Proof

technique · direct

1.1F1F2L1

Every member of $M ((0, 0), (m, n))$ has length $m + n$ , and under the step-word bijection $Φ$ of [L1] with $S = {E, N}$ and $P = (0, 0)$ the set $M ((0, 0), (m, n))$ corresponds exactly to the set $W$ of words $w \in {E, N}^{m + n}$ with $∣ {j < m + n : w_{j} = N} ∣ = n$ .

2.1L2L3step 1.1construct

The map $w \mapsto T (w) : = {j \in N : j < m + n, w_{j} = N}$ carries $W$ into the set of $n$ -element subsets of ${0, \dots, m + n - 1}$ , and the map sending a subset $T$ to the word $w^{T}$ with $w_{j}^{T} = N$ for $j \in T$ and $w_{j}^{T} = E$ otherwise is a two-sided inverse of it, so it is a bijection of $W$ onto that set of subsets.

3.1L2L4step 2.1

The set ${0, \dots, m + n - 1}$ has $m + n$ elements, so its $n$ -element subsets number $(\binom{m + n}{n})$ , and transporting along the two bijections of steps 1.1 and 2.1 makes $M ((0, 0), (m, n))$ finite of that cardinality.

4.1L3L4step 3.1algebra∎

For general endpoints, $v \mapsto v - (a, b)$ is a bijection $M ((a, b), (c, d)) \to M ((0, 0), (m, n))$ : subtracting a constant leaves every difference $v (i) - v (i - 1)$ unchanged, sends $(a, b)$ to $(0, 0)$ and $(c, d)$ to $(m, n)$ , and $v \mapsto v + (a, b)$ inverts it; so the two sets have the same cardinality $(\binom{m + n}{n})$ . At $m = n = 0$ this is one empty path against $(\binom{0}{0}) = 1$ ; at $n = 0$ it is the single all- $E$ path against $(\binom{m}{0}) = 1$ ; at $n = 1$ it is the $m + 1$ paths differing in the position of the one $N$ step against $(\binom{m + 1}{1}) = m + 1$ .

Remarks

The general-endpoint clause is not decoration. Every later count on this page is a count of paths between two points neither of which is the origin, and it is obtained from this clause rather than by repeating the argument.
Where the monotonicity is spent. Only in [F2]: it makes the endpoint determine the numbers of $E$ - and $N$ -steps and hence the length. A fixed start and a fixed step word always determine one endpoint, for every step set; what can fail for a step set containing negative steps is the converse assertion that the endpoint determines the letter counts used by this binomial count.

Depends on

Used by

Dependency tree · two levels

26 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.2 (standard reference, not scraped)
D. Guichard, An Introduction to Combinatorics and Graph Theory, §3.5 (standard reference, not scraped)

∣M((0,0),(m,n))∣=(m+nn)∣M((0,0),(m,n))∣=(nm+n​)