LemmaStatement: AI-adaptedProof: 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.

Reflecting the initial segment at the first visit to level $c$

Statement

Let $c \in Z$ , let $n \in N$ , and let $a, b \in Z$ with $a > c$ and $b > c$ . Write $T$ for the set of diagonal paths $v \in W ((0, a), (n, b))$ that touch the level $c$ (Diagonal lattice paths with steps $U = (1, 1)$ and $D = (1, - 1)$ , and the height function).

For $v \in T$ with height function $h$ , let $τ$ be the least index with $h (τ) = c$ and define $ρ (v)$ to be the diagonal path whose height function is

$h^{'} (i) : = {\begin{cases} 2 c - h (i), & 0 \leq i \leq τ, \\ h (i), & τ \leq i \leq n . \end{cases}$

The two clauses agree at $i = τ$ , and

$ρ : T ⟶ W ((0, 2 c - a), (n, b))$

is a bijection. Its inverse is given by the same recipe, applied to a path starting at height $2 c - a$ .

Facts & Assumptions

Given: an integer $c$ , a natural number $n$ , and integers $a > c$ and $b > c$ .

[F1]

A diagonal path of length $n$ from $(0, α)$ is the same datum as a function $h : {0, \dots, n} \to Z$ with $h (0) = α$ and $h (i) - h (i - 1) \in {1, - 1}$ for $1 \leq i \leq n$ ; it touches the level $c$ when $h (i) = c$ for some $i \leq n$ (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]

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

[L3]

Every nonempty subset $S \subseteq N$ has a least element: there is $ℓ \in S$ with $ℓ \leq s$ for all $s \in S$ (The well-ordering principle).

Proof

technique · direct

1.1F1L3construct

Let $α \in Z$ and let $v$ be a diagonal path of length $n$ from $(0, α)$ with height function $h$ and $h (n) = b$ , touching the level $c$ . The set of indices $i \leq n$ with $h (i) = c$ is a nonempty subset of $N$ , so it has a least element $τ$ , and $τ < n$ because $h (n) = b > c$ . The function $h^{'}$ displayed in the statement is well defined, since at $i = τ$ the first clause gives $2 c - h (τ) = c$ and the second gives $h (τ) = c$ ; it satisfies $h^{'} (0) = 2 c - α$ and $h^{'} (n) = h (n) = b$ ; and for $1 \leq i \leq τ$ one has $h^{'} (i) - h^{'} (i - 1) = - (h (i) - h (i - 1)) \in {1, - 1}$ while for $τ < i \leq n$ one has $h^{'} (i) - h^{'} (i - 1) = h (i) - h (i - 1) \in {1, - 1}$ . So $h^{'}$ is the height function of a diagonal path of length $n$ from $(0, 2 c - α)$ ending at $b$ .

1.2F1L1

Every $v^{'} \in W ((0, 2 c - a), (n, b))$ touches the level $c$ : its height function has $h^{'} (0) = 2 c - a < c$ because $a > c$ , and $h^{'} (n) = b > c$ , so $h^{'} (0) \leq c \leq h^{'} (n)$ and [L1] supplies an index with height $c$ . Likewise every $v \in W ((0, a), (n, b))$ that touches $c$ is in $T$ by definition.

2.1step 1.1algebra

The first visit to $c$ is at the same index for $v$ and for the path built in step 1.1: for $i < τ$ we have $h (i) \neq c$ , hence $h^{'} (i) = 2 c - h (i) \neq c$ , while $h^{'} (τ) = c$ .

3.1L2step 1.1step 1.2step 2.1algebra∎

Applying step 1.1 with $α = a$ shows $ρ$ maps $T$ into $W ((0, 2 c - a), (n, b))$ , and applying it with $α = 2 c - a$ , which is legitimate by step 1.2, shows the same recipe maps $W ((0, 2 c - a), (n, b))$ into $W ((0, a), (n, b))$ and, since the image touches $c$ , into $T$ . Applying the recipe twice returns the original path: by step 2.1 the first visit index is the same at both applications, and $2 c - (2 c - h (i)) = h (i)$ for $i \leq τ$ while the second segment is untouched. So the two maps are two-sided inverses of one another and $ρ$ is a bijection by [L2].

Remarks

The proof is the two-sided inverse, and that is deliberate. A count of the reflected paths that argued only that reflection produces a path of the right kind would not show that every such path arises, and it is exactly the surjectivity that step 1.2 supplies, from the intermediate-value lemma.
The endpoint hypothesis. The stated form assumes $b > c$ , as required by the reflection principle that uses it, and then the first visit satisfies $τ < n$ . The same construction also remains a bijection when $b = c$ ; in that boundary case the first visit may be the final index and reflection fixes that endpoint.

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.3 (standard reference, not scraped)

Reflecting the initial segment at the first visit to level cc