A small Lean 4 + Mathlib port of selected results from the
agda/cubical development on
Archimedean ordered commutative rings. It states the witness-extraction
form of the Archimedean property as a typeclass and proves its
equivalence with Mathlib's existing Archimedean typeclass over a
linearly ordered commutative ring.
The portfolio companions the TYPES 2026 abstract A Cubical Path from Algebra to Analysis, where this constructive form supports a development of Cauchy reals over a constructive ordered field.
class IsConstructiveArchimedean
(R : Type u) [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] : Prop where
archimedean_witness :
∀ (x y : R), 0 < x → 0 < y → ∃ k : ℕ, x < ((k : R) + 1) * y
theorem isConstructiveArchimedean_iff_archimedean :
IsConstructiveArchimedean R ↔ Archimedean RInstances are provided for ℚ, ℤ, and ℝ. Two inline example
blocks at the end of Archimedean.lean show witness extraction in
action. A specialised application — extracting a natural k with
1 / (k + 1) < ε from any positive ε : ℚ — illustrates how the class
is consumed in constructive analysis.
Mathlib's Archimedean R says: for every x : R and every 0 < y,
there is some n : ℕ with x ≤ n • y. That is the right form for
the order-theoretic content of the property.
The form preferred in constructive analysis (and in the cubical
development this is ported from) is dual: given two positives x and
y, produce a natural k such that x < (k + 1) * y. This is the
witness one needs to bound denominators of approximations to a Cauchy
real. Classically the two formulations are interchangeable; the value
of stating both is that the witness form is easier to use in proofs
that build sequences, while the upper-bound form participates in
order-theoretic algebra.
The equivalence between the two is the unique mathematical content of
this file — neither half is a verbatim re-statement of an existing
Mathlib result. Two short bridge proofs handle the n • y ↔
(n : R) * y translation and the n → n + 1 strictness bump.
The Lean port draws on these agda/cubical contributions:
- PR #1246 —
OrderedCommRing(axioms + connection lemmas). - PR #1271 — Pseudolattice instances for the standard ordered rings.
- PR #1272 — Pseudolattice properties.
The full Agda development additionally covers ordered fields, premetric spaces (after Gilbert, CPP 2017), and a higher inductive-inductive construction of the Cauchy reals. Those are out of scope for a Lean + Mathlib port: they depend essentially on cubical-specific features (path types, propositional truncation in record fields, higher inductive-inductive types) that have no direct counterpart in Mathlib's classical setting.
This project pins Mathlib v4.29.1 with the corresponding Lean
toolchain leanprover/lean4:v4.29.1.
lake exe cache get # pulls precompiled Mathlib oleans (saves ~30 min)
lake buildlake build is wired up as a CI check via
.github/workflows/lean_action_ci.yml.