Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-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 even and odd index maps and the alternating sequence: strictly increasing e,o with N their disjoint union, and the unique (sk) with s0=1, sσ(k)=−sk, which satisfies ∣sk∣=1, s∘e≡1 and s∘o≡−1

Statement

Let σ be the successor on N (The natural numbers N (von Neumann)). There are functions e,o:N→N and a sequence (sk) of reals (Sequences of reals: bounded, eventually, frequently, tails, subsequences) with the following properties.

  1. The index maps. e is the unique function with e0=0 and eσ(j)=σ(σ(ej)), and o the unique function with o0=σ(0) and oσ(j)=σ(σ(oj)). Both are strictly increasing.
  2. The partition. N is the disjoint union of the ranges of e and of o: every natural number is ei for exactly one i or oi for exactly one i, and never both.
  3. The alternating sequence. (sk) is the unique sequence of reals with s0=1,sσ(k)=−sk(k∈N).
  4. Its values. ∣sk∣=1 for every k, so (sk) is bounded; and sej=1,soj=−1(j∈N), that is s∘e is constantly 1 and s∘o constantly −1.

This is the sequence usually written sk=(−1)k, with ej=2j and oj=2j+1, presented by the recursions that its proofs actually use. It is collected here once because three separate items on this page and its companion need an alternating or interleaved witness, and rebuilding the recursion inside each of them is what this lemma exists to prevent.

Facts & Assumptions

Given: By the recursion theorem (The recursion theorem) applied to the set R, the element 1 and the function u↦−u, the unique sequence (sk) of reals with s0=1 and sσ(k)=−sk; applied to the set N, the element 0 and the function i↦σ(σ(i)), the unique e:N→N with e0=0 and eσ(j)=σ(σ(ej)); and applied to N, the element σ(0) and the same function, the unique o:N→N with o0=σ(0) and oσ(j)=σ(σ(oj)) (The natural numbers N (von Neumann), Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L1]

Recursion theorem, including its uniqueness clause (The recursion theorem).

[L2]
[L3]

Order on N: i<σ(i) for every i, since σ(i)=i+1 gives i≤σ(i) and σ(i)≠i; and the order is transitive and total (Order on the natural numbers, Addition of natural numbers, No natural number equals its own successor, ≤ is a linear order on N).

[L4]

Consecutive comparisons suffice: if ni<nσ(i) for every i then n is strictly increasing (A strictly increasing index map satisfies nk≥k).

[L5]

Absolute value and field arithmetic: ∣−u∣=∣u∣ (Basic properties of the absolute value); ∣v∣=v whenever v≥0 (Absolute value in an ordered field, Order on the reals); and −(−u)=u (Field).

[L6]

Order in R: 0<1 (The multiplicative identity is positive), sums of positives are positive and adding a constant preserves the order (Order is preserved by adding a constant and by adding inequalities, Complete ordered field (least-upper-bound property), Ordered field), so 1−(−1)=1+1>0 and hence −1<1; in particular 1≠−1.

Proof

technique · induction
1.1

Base case for claim 4: ∣s0∣=∣1∣=1, since 1>0 makes ∣1∣=1.

givenL5L6base
1.2

Inductive hypothesis: fix k∈N and assume ∣sk∣=1.

ih
1.3

Both index maps satisfy consecutive strict comparisons: ej<σ(ej)<σ(σ(ej))=eσ(j), and likewise oj<oσ(j), so e and o are strictly increasing and claim 1 holds, its uniqueness part being the uniqueness clause of the recursion theorem.

givenL1L3L4
1.4

By induction, sej=1 for every j: the base case is se0=s0=1, and if sej=1 then seσ(j)=sσ(σ(ej))=−sσ(ej)=−(−sej)=sej=1.

givenL1L2L5
1.5

By induction, soj=−1 for every j: the base case is so0=sσ(0)=−s0=−1, and if soj=−1 then soσ(j)=sσ(σ(oj))=−(−soj)=soj=−1.

givenL1L2L5
1.6

By induction on n, every natural number satisfies: either n=ei and σ(n)=oi for some i, or n=oi and σ(n)=eσ(i) for some i. The base case is 0=e0 with σ(0)=o0. For the successor step, if n=ei and σ(n)=oi then σ(n)=oi and σ(σ(n))=σ(σ(ei))=eσ(i), which is the second alternative at σ(n); and if n=oi and σ(n)=eσ(i) then σ(n)=eσ(i) and σ(σ(n))=σ(σ(oi))=oσ(i), which is the first alternative at σ(n).

givenL1L2
1.7

The sequence (sk) is the unique sequence of reals with s0=1 and sσ(k)=−sk, by the uniqueness clause of the recursion theorem: this is claim 3.

givenL1
2.1

Successor step for claim 4: ∣sσ(k)∣=∣−sk∣=∣sk∣=1.

step 1.2L5
2.2

In particular every natural number lies in the range of e or in the range of o, since each alternative of step 1.6 exhibits n as such a value.

step 1.6
2.3

The two ranges are disjoint: if ei=oj for some i,j then 1=sei=soj=−1, contradicting 1≠−1.

step 1.4step 1.5L6
2.4

Each of e and o is injective, being strictly increasing, so a natural number in the range of e is ei for exactly one i, and likewise for o.

step 1.3L3
3.1

By the induction principle, ∣sk∣=1 for every k∈N; hence ∣sk∣≤1 at every index and (sk) is bounded. Together with steps 1.4 and 1.5 this is claim 4.

step 1.1step 2.1step 1.4step 1.5L2
4.1

Claim 2 follows: by step 2.2 every natural is in one of the two ranges, by step 2.3 not in both, and by step 2.4 the index realising it is unique. Claims 1, 2, 3 and 4 are therefore all established.

step 2.2step 2.3step 3.1step 2.4step 1.3step 1.7discharge-induction∎

Remarks

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