1-- Ordered-field definitions2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.OrderedField.Defs8import Field.Core9import Order1011-- Translation preserves strict order. Commutativity later gives either side.12predicate AddStrictMono (A add lt : Set) :=13∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A,14 relates(lt, x, y) → relates(lt, call2(add, x, z), call2(add, y, z))1516-- The product of two positive elements is positive.17predicate MulPositive (A mul zero lt : Set) :=18∀ x ∈ A, ∀ y ∈ A,19 relates(lt, zero, x) → relates(lt, zero, y) →20 relates(lt, zero, call2(mul, x, y))2122-- A strict-order presentation of an ordered field. This is equivalent to the23-- usual non-strict interface, while matching the natural order on Dedekind24-- cuts: proper inclusion.25predicate IsOrderedField (A add zero neg mul one inv lt : Set) :=26 IsFieldWithInverse(A, add, zero, neg, mul, one, inv) ∧27 (StrictLinearOrder(A, lt) ∧28 (AddStrictMono(A, add, lt) ∧ MulPositive(A, mul, zero, lt)))2930-- An absolute-value operation is characterized by its zero, positive, and31-- negative branches. Ordered-field theory supplies the laws derived from32-- these equations; concrete models need only prove the branch interface.33predicate AbsoluteValue (A zero neg lt abs : Set) :=34 FunctionBetween(abs, A, A) ∧35 (abs(zero) = zero ∧36 (∀ x ∈ A,37 (relates(lt, zero, x) → abs(x) = x) ∧38 (relates(lt, x, zero) → abs(x) = neg(x))))3940-- The non-strict order canonically induced by a strict linear order.41predicate LessEqualBy (A lt x y : Set) :=42 x ∈ A ∧ y ∈ A ∧ (x = y ∨ relates(lt, x, y))4344-- Division by two in any field, expressed through its graph operations.45def fieldHalf (add mul one inv x : Set) : Set:=46 call2(mul, inv(call2(add, one, one)), x)47