Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-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.

Every complete ordered field is Archimedean

Statement

Every complete ordered field FF (Complete ordered field (least-upper-bound property)) is Archimedean: for every xFx \in F there is a natural number n1n \ge 1 with x<n1Fx < n \cdot 1_F, where n1Fn \cdot 1_F is the canonical natural of the ordered field FF (Ordered field). Equivalently, the canonical naturals are cofinal in FF.

Facts & Assumptions

Given: A complete ordered field FF; write A={n1F:n1}A = \{\, n \cdot 1_F : n \ge 1 \,\} for the set of its canonical naturals.

[L1]

Least-upper-bound property: every nonempty SFS \subseteq F that is bounded above has a least upper bound supSF\sup S \in F (Complete ordered field (least-upper-bound property)).

[L2]

Each canonical natural satisfies n1F>0n \cdot 1_F > 0, one has (n+1)1F=n1F+1F(n+1) \cdot 1_F = n \cdot 1_F + 1_F, and (n+1)1F>n1F(n+1) \cdot 1_F > n \cdot 1_F (Canonical naturals are positive and strictly increasing).

[L3]

Proof

technique · contradiction
1.1

Suppose, for contradiction, that FF is not Archimedean: there is some xFx \in F with n1Fxn \cdot 1_F \le x for all n1n \ge 1, that is, xx is an upper bound of AA.

assume-contra
2.1

The set AA is nonempty, since 11F=1FA1 \cdot 1_F = 1_F \in A, and it is bounded above by xx.

step 1.1L2
3.1

By the least-upper-bound property, AA has a least upper bound s=supAFs = \sup A \in F.

step 2.1L1
4.1

Since 1F>01_F > 0, we have s1F<ss - 1_F < s; as ss is the least upper bound, s1Fs - 1_F is not an upper bound of AA.

step 3.1L3
5.1

Hence there is some m1m \ge 1 with m1F>s1Fm \cdot 1_F > s - 1_F.

step 4.1
6.1

Adding 1F1_F to both sides, (m+1)1F=m1F+1F>s(m+1) \cdot 1_F = m \cdot 1_F + 1_F > s.

step 5.1L2
7.1

But (m+1)1FA(m+1) \cdot 1_F \in A, so (m+1)1Fs(m+1) \cdot 1_F \le s because ss is an upper bound of AA, contradicting 6.1.

step 6.1step 3.1L2
8.1

The assumption is therefore untenable, so FF is Archimedean.

step 7.1discharge-contradiction

Depends on

Used by

…and 112 more results.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 8 results over 5 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