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.

The reflection principle: paths from $(0, a)$ to $(n, b)$ staying strictly above level $c$ are counted by a difference of two binomial coefficients

Statement

Let $c \in Z$ , let $n \in N$ and let $a, b \in Z$ with $a > c$ and $b > c$ . Write $A$ for the set of diagonal paths $v \in W ((0, a), (n, b))$ that stay strictly above the level $c$ , that is $h (i) > c$ for every $i$ with $0 \leq i \leq n$ (Diagonal lattice paths with steps $U = (1, 1)$ and $D = (1, - 1)$ , and the height function).

$A$ is finite and

$∣ A ∣ + ∣ W ((0, 2 c - a), (n, b)) ∣ = ∣ W ((0, a), (n, b)) ∣ .$
Suppose $2$ divides $n + b - a$ and $b - a \geq - n$ , and let $u \in N$ be the natural number with $2 u = n + b - a$ . Then $u + a - c$ is a natural number and

$∣ A ∣ + (\binom{n}{u + a - c}) = (\binom{n}{u}), so ∣ A ∣ = (\binom{n}{u}) - (\binom{n}{u + a - c}) .$
If $2$ does not divide $n + b - a$ , or $b - a < - n$ , or $b - a > n$ , then all three sets above are empty and all three counts are $0$ .

Facts & Assumptions

Given: an integer $c$ , a natural number $n$ , integers $a > c$ and $b > c$ , and the set $A$ of the statement.

[F1]

The height function of a diagonal path of length $n$ from $(0, a)$ satisfies $h (0) = a$ and $h (i) - h (i - 1) \in {1, - 1}$ ; the path touches the level $c$ when $h (i) = c$ for some $i \leq n$ , and stays strictly above $c$ when $h (i) > c$ for every $i \leq n$ ; and the restriction of the path to ${0, \dots, k}$ is a diagonal path of length $k$ (Diagonal lattice paths with steps $U = (1, 1)$ and $D = (1, - 1)$ , and the height function).

[L1]

If a diagonal path of length $n$ has $h (0) \leq c \leq h (n)$ or $h (n) \leq c \leq h (0)$ , then $h (i) = c$ for some $i$ with $0 \leq i \leq n$ (A diagonal path with $h (0) \leq c \leq h (n)$ or $h (n) \leq c \leq h (0)$ satisfies $h (i) = c$ for some $i$ ).

[L2]

If $A$ and $B$ are finite and disjoint, then $A \cup B$ is finite and $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition, clause 1).

[L3]

If $A$ is finite and $f : A \to B$ is a bijection then $B$ is finite and $∣ B ∣ = ∣ A ∣$ ; and a finite set has cardinality $0$ exactly when it is empty (The cardinality $∣ A ∣$ of a finite set).

[L4]

For $a > c$ and $b > c$ , reflecting the initial segment at the first visit to level $c$ is a bijection from the set of $v \in W ((0, a), (n, b))$ that touch the level $c$ onto $W ((0, 2 c - a), (n, b))$ (Reflecting the initial segment at the first visit to level $c$ ).

[L5]

$W ((0, α), (n, β))$ is finite; if $2$ divides $n + β - α$ and $- n \leq β - α \leq n$ then its cardinality is $(\binom{n}{u})$ for the natural number $u$ with $2 u = n + β - α$ , and otherwise the set is empty (The number of diagonal paths from $(0, a)$ to $(n, b)$ is $(\binom{n}{u})$ for the natural number $u$ with $2 u = n + b - a$ , and $0$ when no such $u$ exists).

[L6]

A subset of a finite set is finite (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , clause 1).

[L7]

$(\binom{n}{k}) = 0$ for $k > n$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

Proof

technique · direct

1.1F1L1

A path $v \in W ((0, a), (n, b))$ fails to touch the level $c$ if and only if it stays strictly above $c$ . If it stays strictly above $c$ then no height equals $c$ . Conversely, if $h (k) < c$ for some $k$ , then the restriction of $v$ to ${0, \dots, k}$ is a diagonal path whose height at the last index is $h (k) \leq c \leq a$ , the height at index $0$ , so [L1] gives an index $i \leq k$ with $h (i) = c$ and $v$ touches $c$ ; hence a path that does not touch $c$ has every height $\geq c$ and, none being equal to $c$ , every height $> c$ .

2.1L2L5L6step 1.1

Therefore $W ((0, a), (n, b))$ is the union of the set $T$ of paths that touch $c$ and the set $A$ , and these are disjoint. Both are subsets of the finite set $W ((0, a), (n, b))$ , hence finite by [L5] and [L6], so [L2] gives $∣ T ∣ + ∣ A ∣ = ∣ W ((0, a), (n, b)) ∣$ .

3.1L3L4step 2.1

By [L4] the set $T$ is in bijection with $W ((0, 2 c - a), (n, b))$ , so the two have the same cardinality by [L3], and substituting into step 2.1 gives clause 1.

4.1L3L5L7step 3.1algebra∎

For clause 2, put $u^{'} : = u + a - c$ , a natural number because $a - c \geq 1$ ; then $2 u^{'} = n + b - a + 2 (a - c) = n + b - (2 c - a)$ , so $u^{'}$ is the natural number attached by [L5] to the endpoint data of $W ((0, 2 c - a), (n, b))$ . If $u^{'} \leq n$ then [L5] gives $∣ W ((0, 2 c - a), (n, b)) ∣ = (\binom{n}{u^{'}})$ ; if $u^{'} > n$ then $b - (2 c - a) > n$ , so [L5] makes the set empty and [L7] makes $(\binom{n}{u^{'}})$ equal to $0$ as well. The same two readings apply to $∣ W ((0, a), (n, b)) ∣$ and $(\binom{n}{u})$ , and clause 1 then reads as the displayed identity, whose subtracted form follows because the identity holds in $N$ . For clause 3, [L5] makes $W ((0, a), (n, b))$ empty in each of the three listed cases, so its cardinality is $0$ by [L3] and clause 1 forces both summands to be $0$ , hence both those sets to be empty as well. As a check, $n = 0$ with $a = b$ gives $u = 0$ , $∣ A ∣ = 1$ and $(\binom{0}{a - c}) = 0$ since $a - c \geq 1$ .

Remarks

Where the two hypotheses are spent. The hypothesis $a > c$ is what makes the reflected starting height lie strictly below $c$ , so that every reflected path meets $c$ and the correspondence is onto; the hypothesis $b > c$ is what keeps the first visit strictly before the last index, so that reflection preserves the endpoint. Neither is a normalisation.
The identity is stated as a sum, and only then as a difference. The counting argument produces "touching plus avoiding equals all" in $N$ , and the difference form is legitimate only because that identity has already been proved; written the other way round the subtraction would need its own justification whenever the second coefficient vanishes.

Depends on

Used by

Dependency tree · two levels

38 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, Theorem 10.3.1 (standard reference, not scraped)

The reflection principle: paths from (0,a)(0,a) to (n,b)(n,b) staying strictly above level cc are counted by a difference of two binomial coefficients