LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (openai/gpt-5.4)audited 2026-07-25

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.

Canonical naturals are positive and strictly increasing

Statement

Let $F$ be an ordered field, with field structure as in Field, and for $n \ge 1$ let $n \cdot 1_F$ denote the canonical natural number $\underbrace{1_F + \cdots + 1_F}_{n}$ , defined recursively by $1 \cdot 1_F = 1_F$ and $(n+1) \cdot 1_F = n \cdot 1_F + 1_F$ . Then for every $n \ge 1$ :

$n \cdot 1_F > 0$ and $(n+1) \cdot 1_F > n \cdot 1_F$ ;
the map $n \mapsto n \cdot 1_F$ is strictly increasing, hence injective, on $\{1, 2, 3, \dots\}$ ;
$(m+n) \cdot 1_F = m \cdot 1_F + n \cdot 1_F$ and $(mn) \cdot 1_F = (m \cdot 1_F)(n \cdot 1_F)$ for all $m, n \ge 1$ .

Facts & Assumptions

Given: An ordered field $F$ whose canonical naturals are defined recursively by $1 \cdot 1_F = 1_F$ and $(n+1) \cdot 1_F = n \cdot 1_F + 1_F$ , with $0 \cdot 1_F = 0$ .

[L1]

$0 < 1_F$ in every ordered field (The multiplicative identity is positive).

[L2]

The order is compatible with addition and positives are closed under addition: $a < b$ implies $a + c < b + c$ , and $a > 0$ , $b > 0$ imply $a + b > 0$ (Order is preserved by adding a constant and by adding inequalities).

Proof

technique · induction

1.1

Base case $n = 1$ : by definition $1 \cdot 1_F = 1_F$ , and $1_F > 0$ .

L1base

1.2

Inductive hypothesis: assume $n \cdot 1_F > 0$ for some fixed $n \ge 1$ .

1.3

By the recursion, $(n+1) \cdot 1_F - n \cdot 1_F = 1_F > 0$ , so $(n+1) \cdot 1_F > n \cdot 1_F$ .

givenL1

1.4

Additive identity: fix $m$ and induct on $n$ ; at $n = 1$ , $(m+1) \cdot 1_F = m \cdot 1_F + 1_F$ by the recursion, and if $(m+n) \cdot 1_F = m \cdot 1_F + n \cdot 1_F$ then $(m+n+1) \cdot 1_F = (m+n) \cdot 1_F + 1_F = m \cdot 1_F + n \cdot 1_F + 1_F = m \cdot 1_F + (n+1) \cdot 1_F$ .

givenalgebra

2.1

Inductive step: $(n+1) \cdot 1_F = n \cdot 1_F + 1_F$ is a sum of two positives, by the hypothesis and $1_F > 0$ , hence $(n+1) \cdot 1_F > 0$ .

step 1.2L1L2

2.2

Iterating 1.3, for $m < n$ one has $m \cdot 1_F < n \cdot 1_F$ , so $n \mapsto n \cdot 1_F$ is strictly increasing and therefore injective on $\{1, 2, 3, \dots\}$ .

step 1.3L2

2.3

Multiplicative identity: fix $m$ and induct on $n$ ; at $n = 1$ , $(m \cdot 1) \cdot 1_F = m \cdot 1_F = (m \cdot 1_F)(1 \cdot 1_F)$ , and the step $(m(n+1)) \cdot 1_F = (mn + m) \cdot 1_F = (mn) \cdot 1_F + m \cdot 1_F = (m \cdot 1_F)(n \cdot 1_F) + (m \cdot 1_F)(1_F) = (m \cdot 1_F)((n+1) \cdot 1_F)$ uses 1.4 and distributivity.

step 1.4algebra

3.1

By induction on 1.1, 1.2, 2.1, $n \cdot 1_F > 0$ for every $n \ge 1$ ; with the strict increase 2.2 and the identities 1.4, 2.3, every claim holds.

step 2.1step 2.2step 1.4step 2.3discharge-induction∎

Depends on

Used by

…and 190 more results.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 6 results over 4 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
M. Spivak, Calculus, 4th ed., Ch. 1 (standard reference, not scraped)
Elias Zakon, Mathematical Analysis: Natural Numbers and Induction (standard reference, not scraped)