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

For each start point the step word is a bijection onto Sn

Statement

Let S be a step set, PZ×Z and nN. The map sending a lattice path to its step word is a bijection

Φ:LS(P;n)Sn,

whose inverse sends w to the path vw traced by w from P (Lattice paths, step sets and step words). Consequently LS(P;n) is finite with

LS(P;n)=Sn,

the power being the natural-number exponentiation of Exponentiation of natural numbers, mn, and its agreement with the integer power in R.

Facts & Assumptions

Given: a step set S, a point PZ×Z and a natural number n.

[F1]

A lattice path of length n with steps in S from P is a function v:{0,1,,n}Z×Z with v(0)=P and v(i)v(i1)S for every i with 1in; its step word is the word wSn with wi1=v(i)v(i1); and the path traced by wSn from P satisfies vw(0)=P and vw(i)=vw(i1)+wi1 for 1in (Lattice paths, step sets and step words).

[L1]

For f:AB: f is a bijection if and only if there is a function g:BA with gf=ΔA and fg=ΔB, and such a g is then unique (f:AB is a bijection if and only if there is a function g:BA with gf=ΔA and fg=ΔB; such a g is unique, equals the inverse relation f1, and is itself a bijection).

[L2]

For finite sets A and B, the set AB of functions BA is finite and AB=AB (The set AB of functions BA between finite sets is finite, with AB=AB).

[L3]

A property that holds at 0 and passes from every natural number to its successor holds at every natural number: if a property P satisfies P(0) and (P(n)P(σ(n))) for all n, then P(n) holds for all nN (The principle of mathematical induction).

Proof

technique · direct
1.1

For vLS(P;n) and each i with 1in the difference v(i)v(i1) lies in S, so Φ(v) is a function {0,,n1}S, that is an element of Sn; for n=0 the domain is empty and Φ(v) is the empty word.

F1
2.1

Given wSn, the traced path vw lies in LS(P;n) and its step word has j-th letter vw(j+1)vw(j)=wj, so Φ(vw)=w; conversely, given vLS(P;n) with w=Φ(v), both v and vw take the value P at the index 0 and both satisfy u(i)=u(i1)+wi1 for 1in, so the set of indices at which they agree contains 0 and contains i whenever it contains i1, whence they agree throughout and vw=v. Thus wvw is a two-sided inverse of Φ and Φ is a bijection.

F1L1L3step 1.1
3.1

Since S is finite and {0,,n1} is finite with n elements, Sn is finite with Sn=Sn, and transporting along the bijection of step 2.1 gives that LS(P;n) is finite with the same cardinality. At n=0 both sides are 1, one empty path against the one empty word, and this holds also for S=; for S= and n1 both sides are 0.

L2step 2.1

Remarks

  • What the lemma is for. Every count on this page is obtained by counting words and transporting the answer along this bijection, so the correspondence is proved once here and cited rather than re-established.

  • The start point is fixed throughout. The map Φ forgets P, and a step word alone therefore determines a path only after a start point has been named.

Depends on

Used by

Dependency tree · two levels

39 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