LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 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$

Statement

Let $u, d \in N$ and put $n : = u + d$ . Replacing each letter $U$ of a step word by $N$ and each letter $D$ by $E$ induces a bijection

$Λ : W ((0, 0), (n, u - d)) ⟶ M ((0, 0), (d, u))$

from the diagonal paths of length $n$ from $(0, 0)$ ending at height $u - d$ (Diagonal lattice paths with steps $U = (1, 1)$ and $D = (1, - 1)$ , and the height function) onto the monotone paths from $(0, 0)$ to $(d, u)$ (Monotone lattice paths with steps $E = (1, 0)$ and $N = (0, 1)$ ).

Moreover the two pictures agree step by step: if $v$ has height function $h$ and $Λ (v) (i) = (x_{i}, y_{i})$ , then

$h (i) = y_{i} - x_{i} (0 \leq i \leq n) .$

Consequently, for every $c \in Z$ and every $i$ , the height inequality $h (i) \geq c$ holds if and only if $y_{i} - x_{i} \geq c$ ; in particular staying weakly above the level $0$ corresponds to staying weakly above the diagonal $y = x$ .

Facts & Assumptions

Given: natural numbers $u$ and $d$ , and $n = u + d$ .

[F1]

A diagonal lattice path is a lattice path whose steps lie in the step set ${U, D}$ with $U = (1, 1)$ , $D = (1, - 1)$ ; a diagonal path of length $n$ from $(0, 0)$ has $v (i) = (i, h (i))$ , and with $μ (i)$ the number of up-steps among the first $i$ its height is $h (i) = 2 μ (i) - i$ when $a = 0$ (Diagonal lattice paths with steps $U = (1, 1)$ and $D = (1, - 1)$ , and the height function).

[F2]

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)$ ; for such a path from $(a, b)$ with step word $w$ and $ν (i)$ the number of $N$ letters among the first $i$ , one has $v (i) = (a + i - ν (i), b + ν (i))$ (Monotone lattice paths with steps $E = (1, 0)$ and $N = (0, 1)$ ).

[L1]

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).

[L2]

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}$ ).

Proof

technique · direct

1.1

The letter map $λ : {U, D} \to {E, N}$ with $λ (U) = N$ and $λ (D) = E$ has the two-sided inverse $N \mapsto U$ , $E \mapsto D$ , so composing a word with $λ$ carries ${U, D}^{n}$ to ${E, N}^{n}$ and composing with the inverse letter map carries it back; a word $w$ with $μ (n) = u$ up-steps is carried to a word with $ν (n) = u$ letters $N$ and $d$ letters $E$ . Hence a diagonal path of length $n$ from $(0, 0)$ ending at height $u - d$ is carried to a monotone path from $(0, 0)$ ending at $(d, u)$ , and conversely.

F1F2

2.1

Define $Λ$ as the composite: take the step word of a diagonal path by [L2], compose it with $λ$ , and trace the resulting word from $(0, 0)$ ; define $Λ^{'}$ the same way with the inverse letter map. Each of the three constituents of $Λ$ is a bijection with the corresponding constituent of $Λ^{'}$ as inverse, by [L2] and step 1.1, so $Λ^{'} \circ Λ$ and $Λ \circ Λ^{'}$ are the respective identities and $Λ$ is a bijection.

L1L2step 1.1

3.1

For $0 \leq i \leq n$ the count of up-steps among the first $i$ letters of $w$ equals the count of letters $N$ among the first $i$ letters of $λ \circ w$ , that is $μ (i) = ν (i)$ ; so $y_{i} - x_{i} = ν (i) - (i - ν (i)) = 2 μ (i) - i = h (i)$ , and the two sides of the height inequality are the same integer, whence each holds exactly when the other does. Taking $c = 0$ gives the statement about the diagonal $y = x$ , and at $i = 0$ both sides are $0$ .

F1F2step 1.1algebra∎

Remarks

Why this is a lemma and not a convention. The page uses the rectangular picture for the binomial count and the diagonal picture for heights, levels and reflections. The sources use one or the other and state no correspondence, so a page using both must prove they agree once. Every later statement that moves between the pictures cites this lemma and does not restate it.
What the correspondence does not do. It matches the two step sets and the two positions, and nothing else. The number of steps is preserved and the two endpoints determine each other, but a level in one picture is a diagonal line in the other, which is why the level statements below are made in the diagonal picture only.

Depends on

Used by

Dependency tree · two levels

20 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–10.3 (standard reference, not scraped)

The two step sets describe the same objects: U↦NU↦N, D↦ED↦E is a bijection matching the diagonal y=xy=x with the level 00