Alphabeta Math
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.

A diagonal path with h(0)≤c≤h(n) or h(n)≤c≤h(0) satisfies h(i)=c for some i

Statement

Let v be a diagonal lattice path of length n from (0,a) with height function h (Diagonal lattice paths with steps U=(1,1) and D=(1,−1), and the height function), and let c∈Z. If

h(0)≤c≤h(n)orh(n)≤c≤h(0),

then h(i)=c for some i with 0≤i≤n; that is, v touches the level c.

Facts & Assumptions

Given: a diagonal path v of length n from (0,a) with height function h, an integer c, and the hypothesis that c lies weakly between h(0) and h(n) in one order or the other.

[F1]

The height function of a diagonal path of length n from (0,a) satisfies h(0)=a and h(i)−h(i−1)∈{1,−1} for 1≤i≤n, and v touches the level c when h(i)=c for some i with 0≤i≤n (Diagonal lattice paths with steps U=(1,1) and D=(1,−1), and the height function).

[L1]

Every nonempty subset S⊆N has a least element: there is ℓ∈S with ℓ≤s for all s∈S (The well-ordering principle).

Proof

technique · cases
1.1

Assume first that h(0)≤c≤h(n). The set I:={ i∈N:i≤n, h(i)≥c } contains n, so it is nonempty and has a least element τ.

F1L1assume-case up
1.2

Assume instead that h(n)≤c≤h(0). The set J:={ i∈N:i≤n, h(i)≤c } contains n, so it is nonempty and has a least element θ.

F1L1assume-case down
2.1

In the case h(0)≤c≤h(n) of step 1.1: if τ=0 then h(0)≥c and h(0)≤c, so h(0)=c; and if τ≥1 then τ−1 is not in I, so h(τ−1)<c≤h(τ), whence h(τ)−h(τ−1) is positive and therefore equal to 1, giving h(τ)=h(τ−1)+1≤c and so h(τ)=c.

F1step 1.1
2.2

In the case h(n)≤c≤h(0) of step 1.2: if θ=0 then h(0)≤c and c≤h(0), so h(0)=c; and if θ≥1 then θ−1 is not in J, so h(θ−1)>c≥h(θ), whence h(θ)−h(θ−1) is negative and therefore equal to −1, giving h(θ)=h(θ−1)−1≥c and so h(θ)=c.

F1step 1.2
3.1

The hypothesis puts c weakly between h(0) and h(n) in one of the two orders, so one of the two cases applies, and each produces an index at which the height is exactly c.

step 2.1step 2.2cases-exhaustive∎

Remarks

  • Where the step set is spent. The argument uses only that consecutive heights differ by exactly 1, and it fails for a step set whose steps change the height by more than one unit: such a path can pass from above a level to below it without ever meeting it. The companion page carries that witness.

  • Both orders are needed. The reflection argument applies the lemma once with the start above the level and the end below it, and once the other way round, so neither inequality may be dropped.

Depends on

Used by

Dependency tree · two levels

16 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