Move towards base-n expansions (#112)

2025-10-08 13:28:39 +00:00 · 2020-04-11 19:46:26 +01:00
parent e9aa1bcc05
commit 380548134d
22 changed files with 312 additions and 102 deletions
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -93,6 +93,8 @@ open import Rings.InitialRing
 open import Rings.Homomorphisms.Lemmas
 open import Rings.UniqueFactorisationDomains.Definition
 open import Rings.Examples.Examples
+open import Rings.Orders.Total.Bounded
+open import Rings.Orders.Partial.Bounded

 open import Setoids.Setoids
 open import Setoids.DirectSum
--- a/Fields/CauchyCompletion/Addition.agda
+++ b/Fields/CauchyCompletion/Addition.agda
@@ -16,7 +16,7 @@ open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 open import Numbers.Naturals.Order.Lemmas

-module Fields.CauchyCompletion.Addition {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) (charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) where
+module Fields.CauchyCompletion.Addition {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

 open Setoid S
 open SetoidTotalOrder (TotallyOrderedRing.total order)
@@ -30,7 +30,9 @@ open Field F
 open import Fields.Lemmas F
 open import Fields.CauchyCompletion.Definition order F
 open import Rings.Orders.Partial.Lemmas pRing
+open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })
 open import Rings.Orders.Total.Lemmas order
+open import Rings.InitialRing R

 private
  lemm : (m : ℕ) (a b : Sequence A) → index (apply _+_ a b) m ≡ (index a m) + (index b m)
--- a/Fields/CauchyCompletion/Approximation.agda
+++ b/Fields/CauchyCompletion/Approximation.agda
@@ -18,7 +18,7 @@ open import Numbers.Naturals.Order
 open import Numbers.Naturals.Order.Lemmas
 open import Semirings.Definition

-module Fields.CauchyCompletion.Approximation {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) (charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) where
+module Fields.CauchyCompletion.Approximation {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

 open Setoid S
 open SetoidTotalOrder (TotallyOrderedRing.total order)
@@ -34,8 +34,10 @@ open import Fields.Orders.Lemmas {F = F} record { oRing = order }
 open import Rings.Orders.Total.Lemmas order
 open import Rings.Orders.Partial.Lemmas pRing
 open import Fields.CauchyCompletion.Definition order F
-open import Fields.CauchyCompletion.Addition order F charNot2
-open import Fields.CauchyCompletion.Comparison order F charNot2
+open import Fields.CauchyCompletion.Addition order F
+open import Fields.CauchyCompletion.Comparison order F
+open import Rings.InitialRing R
+open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })

 abstract

--- a/Fields/CauchyCompletion/BaseExpansion.agda
+++ b/Fields/CauchyCompletion/BaseExpansion.agda
@@ -0,0 +1,126 @@
+{-# OPTIONS --safe --warning=error --without-K --guardedness #-}
+
+open import Setoids.Setoids
+open import Rings.Definition
+open import Rings.Lemmas
+open import Rings.Orders.Partial.Definition
+open import Rings.Orders.Total.Definition
+open import Groups.Definition
+open import Groups.Lemmas
+open import Fields.Fields
+open import Sets.EquivalenceRelations
+open import Sequences
+open import Setoids.Orders
+open import Functions
+open import LogicalFormulae
+open import Numbers.Naturals.Semiring
+open import Numbers.Naturals.Order
+open import Numbers.Naturals.Order.Lemmas
+open import Semirings.Definition
+open import Numbers.Modulo.Definition
+open import Orders.Total.Definition
+
+module Fields.CauchyCompletion.BaseExpansion {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where
+
+open Setoid S
+open SetoidTotalOrder (TotallyOrderedRing.total order)
+open SetoidPartialOrder pOrder
+open Equivalence eq
+open PartiallyOrderedRing pRing
+open Ring R
+open Group additiveGroup
+open Field F
+open import Fields.Orders.Limits.Definition {F = F} (record { oRing = order })
+open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })
+open import Fields.Orders.Limits.Lemmas {F = F} (record { oRing = order })
+
+open import Fields.Lemmas F
+open import Fields.Orders.Lemmas {F = F} record { oRing = order }
+open import Rings.Orders.Total.Lemmas order
+open import Rings.Orders.Partial.Lemmas pRing
+open import Fields.CauchyCompletion.Definition order F
+open import Fields.CauchyCompletion.Setoid order F
+open import Fields.CauchyCompletion.Addition order F
+open import Fields.CauchyCompletion.Comparison order F
+open import Fields.CauchyCompletion.Approximation order F
+open import Rings.InitialRing R
+open import Rings.Orders.Partial.Bounded pRing
+open import Rings.Orders.Total.Bounded order
+
+cauchyTimesBoundedIsCauchy : {s : Sequence A} → cauchy s → {t : Sequence A} → Bounded t → cauchy (apply _*_ s t)
+cauchyTimesBoundedIsCauchy {s} cau {t} (K , bounded) e 0<e with allInvertible K (boundNonzero (K , bounded))
+... | 1/K , prK with cau (1/K * e) (orderRespectsMultiplication (reciprocalPositive K 1/K (boundGreaterThanZero (K , bounded)) (transitive *Commutative prK)) 0<e)
+... | N , cauPr = N , ans
+  where
+    ans : {m n : ℕ} (N<m : N <N m) (N<n : N <N n) → (abs (index (apply _*_ s t) m + inverse (index (apply _*_ s t) n))) < e
+    ans N<m N<n with cauPr N<m N<n
+    ... | r = {!!}
+
+boundedTimesCauchyIsCauchy : {s : Sequence A} → cauchy s → {t : Sequence A} → Bounded t → cauchy (apply _*_ t s)
+boundedTimesCauchyIsCauchy {s} cau {t} bou = cauchyWellDefined (ans s t) (cauchyTimesBoundedIsCauchy cau bou)
+  where
+    ans : (s t : Sequence A) (m : ℕ) → index (apply _*_ s t) m ∼ index (apply _*_ t s) m
+    ans s t m rewrite indexAndApply t s _*_ {m} | indexAndApply s t _*_ {m} = *Commutative
+
+private
+  digitExpansionSeq : {n : ℕ} → .(0<n : 0 <N n) → Sequence (ℤn n 0<n) → Sequence A
+  Sequence.head (digitExpansionSeq {n} 0<n seq) = fromN (ℤn.x (Sequence.head seq))
+  Sequence.tail (digitExpansionSeq {n} 0<n seq) = digitExpansionSeq 0<n (Sequence.tail seq)
+
+  powerSeq : (i : A) → (start : A) → Sequence A
+  Sequence.head (powerSeq i start) = start
+  Sequence.tail (powerSeq i start) = powerSeq i (start * i)
+
+  powerSeqInduction : (i : A) (start : A) → (m : ℕ) → (index (powerSeq i start) (succ m)) ∼ i * (index (powerSeq i start) m)
+  powerSeqInduction i start zero = *Commutative
+  powerSeqInduction i start (succ m) = powerSeqInduction i (start * i) m
+
+  ofBaseExpansionSeq : {n : ℕ} → .(0<n : 0 <N n) → Sequence (ℤn n 0<n) → Sequence A
+  ofBaseExpansionSeq {succ n} 0<n seq = apply _*_ (digitExpansionSeq 0<n seq) (powerSeq pow pow)
+    where
+      pow : A
+      pow = underlying (allInvertible (fromN (succ n)) (charNotN n))
+
+  powerSeqPositive : {i : A} → (0R < i) → {s : A} → (0R < s) → (m : ℕ) → 0R < index (powerSeq i s) m
+  powerSeqPositive {i} 0<i {s} 0<s zero = 0<s
+  powerSeqPositive {i} 0<i {s} 0<s (succ m) = <WellDefined reflexive (symmetric (powerSeqInduction i s m)) (orderRespectsMultiplication 0<i (powerSeqPositive 0<i 0<s m))
+
+  powerSeqConvergesTo0 : (i : A) → (0R < i) → (i < 1R) → {s : A} → (0R < s) → (powerSeq i s) ~> 0G
+  powerSeqConvergesTo0 i 0<i i<1 {s} 0<s e 0<e = {!!}
+
+  powerSeqConverges : (i : A) → (0R < i) → (i < 1R) → {s : A} → (0R < s) → cauchy (powerSeq i s)
+  powerSeqConverges i 0<i i<1 {s} 0<s = convergentSequenceCauchy nontrivial {r = 0R} (powerSeqConvergesTo0 i 0<i i<1 0<s)
+
+  0<n : {n : ℕ} → 1 <N n → 0 <N n
+  0<n 1<n = TotalOrder.<Transitive ℕTotalOrder (le 0 refl) 1<n
+
+  digitExpansionBoundedLemma : {n : ℕ} → .(0<n : 0 <N n) → (seq : Sequence (ℤn n 0<n)) → (m : ℕ) → index (digitExpansionSeq _ seq) m < fromN n
+  digitExpansionBoundedLemma {n} 0<n seq zero with Sequence.head seq
+  ... | record { x = x ; xLess = xLess } = fromNPreservesOrder nontrivial {x} {n} ((squash<N xLess))
+  digitExpansionBoundedLemma 0<n seq (succ m) = digitExpansionBoundedLemma 0<n (Sequence.tail seq) m
+
+  digitExpansionBoundedLemma2 : {n : ℕ} → .(0<n : 0 <N n) → (seq : Sequence (ℤn n 0<n)) → (m : ℕ) → inverse (fromN n) < index (digitExpansionSeq 0<n seq) m
+  digitExpansionBoundedLemma2 {n} 0<n seq zero = <WellDefined identLeft (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) (orderRespectsAddition {_} {fromN (ℤn.x (Sequence.head seq)) + fromN n} (<WellDefined reflexive (fromNPreserves+ (ℤn.x (Sequence.head seq)) n) (fromNPreservesOrder nontrivial {0} {ℤn.x (Sequence.head seq) +N n} (canAddToOneSideOfInequality' _ (squash<N 0<n)))) (inverse (fromN n)))
+  digitExpansionBoundedLemma2 0<n seq (succ m) = digitExpansionBoundedLemma2 0<n (Sequence.tail seq) m
+
+  digitExpansionBounded : {n : ℕ} → .(0<n : 0 <N n) → (seq : Sequence (ℤn n 0<n)) → Bounded (digitExpansionSeq 0<n seq)
+  digitExpansionBounded {n} 0<n seq = fromN n , λ m → ((digitExpansionBoundedLemma2 0<n seq m) ,, digitExpansionBoundedLemma 0<n seq m)
+
+private
+  1/nPositive : (n : ℕ) → 0R < underlying (allInvertible (fromN (succ n)) (charNotN n))
+  1/nPositive n with allInvertible (fromN (succ n)) (charNotN n)
+  ... | a , b = reciprocalPositive (fromN (succ n)) a (fromNPreservesOrder nontrivial (succIsPositive n)) (transitive *Commutative b)
+
+  1/n<1 : (n : ℕ) → (0 <N n) → underlying (allInvertible (fromN (succ n)) (charNotN n)) < 1R
+  1/n<1 n 1<n with allInvertible (fromN (succ n)) (charNotN n)
+  ... | a , b = reciprocal<1 (fromN (succ n)) a (<WellDefined identRight reflexive (fromNPreservesOrder nontrivial {1} {succ n} (succPreservesInequality 1<n))) (transitive *Commutative b)
+
+-- Construct the real that is the given base-n expansion between 0 and 1.
+ofBaseExpansion : {n : ℕ} → .(1<n : 1 <N n) → (fromN n ∼ 0R → False) → Sequence (ℤn n (0<n 1<n)) → CauchyCompletion
+ofBaseExpansion {succ n} 1<n charNotN seq = record { elts = ofBaseExpansionSeq (0<n 1<n) seq ; converges = boundedTimesCauchyIsCauchy (powerSeqConverges _ (1/nPositive n) (1/n<1 n (canRemoveSuccFrom<N (squash<N 1<n))) (1/nPositive n)) (digitExpansionBounded (0<n 1<n) seq)}
+
+toBaseExpansion : {n : ℕ} → .(1<n : 1 <N n) → (fromN n ∼ 0R → False) → CauchyCompletion → Sequence (ℤn n (0<n 1<n))
+toBaseExpansion {n} 1<n charNotN c = {!!}
+
+baseExpansionProof : {n : ℕ} → .{1<n : 1 <N n} → {charNotN : fromN n ∼ 0R → False} → (as : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid (ofBaseExpansion 1<n charNotN (toBaseExpansion 1<n charNotN as)) as
+baseExpansionProof = {!!}
--- a/Fields/CauchyCompletion/Comparison.agda
+++ b/Fields/CauchyCompletion/Comparison.agda
@@ -18,7 +18,7 @@ open import Numbers.Naturals.Order
 open import Numbers.Naturals.Order.Lemmas
 open import Semirings.Definition

-module Fields.CauchyCompletion.Comparison {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) (charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) where
+module Fields.CauchyCompletion.Comparison {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

 open Setoid S
 open SetoidTotalOrder (TotallyOrderedRing.total order)
@@ -34,7 +34,8 @@ open import Rings.Orders.Partial.Lemmas pRing
 open import Rings.Orders.Total.Lemmas order
 open import Fields.Lemmas F
 open import Fields.CauchyCompletion.Definition order F
-open import Fields.CauchyCompletion.Setoid order F charNot2
+open import Fields.CauchyCompletion.Setoid order F
+open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })

 -- "<C rational", where the r indicates where the rational number goes
 record _<Cr_ (a : CauchyCompletion) (b : A) : Set (m ⊔ o) where
--- a/Fields/CauchyCompletion/Definition.agda
+++ b/Fields/CauchyCompletion/Definition.agda
@@ -27,9 +27,12 @@ open Group additiveGroup
 open Field F

 open import Rings.Orders.Total.Lemmas order
+open import Rings.Orders.Total.Cauchy order
+open import Groups.Lemmas additiveGroup

-cauchy : Sequence A → Set (m ⊔ o)
-cauchy s = ∀ (ε : A) → (0R < ε) → Sg ℕ (λ N → ∀ {m n : ℕ} → (N <N m) → (N <N n) → abs ((index s m) -R (index s n)) < ε)
+cauchyWellDefined : {s1 s2 : Sequence A} → ((m : ℕ) → index s1 m ∼ index s2 m) → cauchy s1 → cauchy s2
+cauchyWellDefined {s1} {s2} prop c e 0<e with c e 0<e
+... | N , pr = N , λ {m} {n} N<m N<n → <WellDefined (absWellDefined _ _ (+WellDefined (prop m) (inverseWellDefined (prop n)))) reflexive (pr N<m N<n)

 record CauchyCompletion : Set (m ⊔ o) where
  field
--- a/Fields/CauchyCompletion/Group.agda
+++ b/Fields/CauchyCompletion/Group.agda
@@ -16,7 +16,7 @@ open import LogicalFormulae
 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order

-module Fields.CauchyCompletion.Group {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) (charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) where
+module Fields.CauchyCompletion.Group {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

 open Setoid S
 open SetoidTotalOrder (TotallyOrderedRing.total order)
@@ -29,8 +29,8 @@ open Ring R

 open import Rings.Orders.Total.Lemmas order
 open import Fields.CauchyCompletion.Definition order F
-open import Fields.CauchyCompletion.Addition order F charNot2
-open import Fields.CauchyCompletion.Setoid order F charNot2
+open import Fields.CauchyCompletion.Addition order F
+open import Fields.CauchyCompletion.Setoid order F

 abstract
  +CCommutative : {a b : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid (a +C b) (b +C a)
--- a/Fields/CauchyCompletion/Multiplication.agda
+++ b/Fields/CauchyCompletion/Multiplication.agda
@@ -17,7 +17,7 @@ open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 open import Numbers.Naturals.Order.Lemmas

-module Fields.CauchyCompletion.Multiplication {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) (charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) where
+module Fields.CauchyCompletion.Multiplication {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

 open Setoid S
 open SetoidTotalOrder (TotallyOrderedRing.total order)
@@ -28,13 +28,14 @@ open Ring R
 open Group additiveGroup
 open Field F
 open import Fields.Orders.Lemmas {F = F} record { oRing = order }
+open import Fields.Orders.Total.Lemmas {F = F} record { oRing = order }

 open import Fields.Lemmas F
 open import Rings.Orders.Partial.Lemmas pRing
 open import Rings.Orders.Total.Lemmas order
 open import Fields.CauchyCompletion.Definition order F
-open import Fields.CauchyCompletion.Setoid order F charNot2
-open import Fields.CauchyCompletion.Approximation order F charNot2
+open import Fields.CauchyCompletion.Setoid order F
+open import Fields.CauchyCompletion.Approximation order F

 0!=1 : {e : A} → (0G < e) → 0R ∼ 1R → False
 0!=1 {e} 0<e 0=1 = irreflexive (<WellDefined (Equivalence.reflexive eq) (oneZeroImpliesAllZero R 0=1) 0<e)
--- a/Fields/CauchyCompletion/PartiallyOrderedRing.agda
+++ b/Fields/CauchyCompletion/PartiallyOrderedRing.agda
@@ -22,7 +22,7 @@ open import Semirings.Definition
 open import Groups.Homomorphisms.Definition
 open import Rings.Homomorphisms.Definition

-module Fields.CauchyCompletion.PartiallyOrderedRing {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) (charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) where
+module Fields.CauchyCompletion.PartiallyOrderedRing {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

 open Setoid S
 open SetoidTotalOrder (TotallyOrderedRing.total order)
@@ -36,13 +36,14 @@ open import Fields.Lemmas F
 open import Rings.Orders.Partial.Lemmas pRing
 open import Rings.Orders.Total.Lemmas order
 open import Fields.Orders.Lemmas {F = F} {pRing} (record { oRing = order })
+open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })
 open import Fields.CauchyCompletion.Definition order F
-open import Fields.CauchyCompletion.Addition order F charNot2
-open import Fields.CauchyCompletion.Multiplication order F charNot2
-open import Fields.CauchyCompletion.Approximation order F charNot2
-open import Fields.CauchyCompletion.Ring order F charNot2
-open import Fields.CauchyCompletion.Comparison order F charNot2
-open import Fields.CauchyCompletion.Setoid order F charNot2
+open import Fields.CauchyCompletion.Addition order F
+open import Fields.CauchyCompletion.Multiplication order F
+open import Fields.CauchyCompletion.Approximation order F
+open import Fields.CauchyCompletion.Ring order F
+open import Fields.CauchyCompletion.Comparison order F
+open import Fields.CauchyCompletion.Setoid order F

 productPositives : (a b : A) → (injection 0R) <Cr a → (injection 0R) <Cr b → (injection 0R) <Cr (a * b)
 productPositives a b record { e = eA ; 0<e = 0<eA ; N = Na ; property = prA } record { e = eB ; 0<e = 0<eB ; N = Nb ; property = prB } = record { e = eA * eB ; 0<e = orderRespectsMultiplication 0<eA 0<eB ; N = Na +N Nb ; property = ans }
--- a/Fields/CauchyCompletion/Ring.agda
+++ b/Fields/CauchyCompletion/Ring.agda
@@ -16,7 +16,7 @@ open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 open import Rings.Homomorphisms.Definition

-module Fields.CauchyCompletion.Ring {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) (charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) where
+module Fields.CauchyCompletion.Ring {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

 open Setoid S
 open SetoidTotalOrder (TotallyOrderedRing.total order)
@@ -28,10 +28,10 @@ open Group (Ring.additiveGroup R)

 open import Rings.Orders.Total.Lemmas order
 open import Fields.CauchyCompletion.Definition order F
-open import Fields.CauchyCompletion.Multiplication order F charNot2
-open import Fields.CauchyCompletion.Addition order F charNot2
-open import Fields.CauchyCompletion.Setoid order F charNot2
-open import Fields.CauchyCompletion.Group order F charNot2
+open import Fields.CauchyCompletion.Multiplication order F
+open import Fields.CauchyCompletion.Addition order F
+open import Fields.CauchyCompletion.Setoid order F
+open import Fields.CauchyCompletion.Group order F

 private
  abstract
--- a/Fields/CauchyCompletion/Setoid.agda
+++ b/Fields/CauchyCompletion/Setoid.agda
@@ -18,7 +18,7 @@ open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 open import Semirings.Definition

-module Fields.CauchyCompletion.Setoid {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) (charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) where
+module Fields.CauchyCompletion.Setoid {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where

 open Setoid S
 open SetoidTotalOrder (TotallyOrderedRing.total order)
@@ -31,9 +31,11 @@ open Field F

 open import Fields.Lemmas F
 open import Fields.CauchyCompletion.Definition order F
-open import Fields.CauchyCompletion.Addition order F charNot2
+open import Fields.CauchyCompletion.Addition order F
 open import Rings.Orders.Partial.Lemmas pRing
 open import Rings.Orders.Total.Lemmas order
+open import Rings.InitialRing R
+open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })

 isZero : CauchyCompletion → Set (m ⊔ o)
 isZero record { elts = elts ; converges = converges } = ∀ ε → 0R < ε → Sg ℕ (λ N → ∀ {m : ℕ} → (N <N m) → (abs (index elts m)) < ε)
--- a/Fields/Orders/Limits/Lemmas.agda
+++ b/Fields/Orders/Limits/Lemmas.agda
@@ -41,22 +41,14 @@ open import Fields.Lemmas F
 open import Fields.Orders.Total.Lemmas oF
 open import Rings.Characteristic R
 open import Rings.InitialRing R
+open import Rings.Orders.Total.Cauchy oRing

 private
  2!=3 : 2 ≡ 3 → False
  2!=3 ()

-convergentSequenceCauchy : (nontrivial : 0R ∼ 1R → False) → {a : Sequence A} → {r : A} → a ~> r → (decidedCharacteristic : ((1R + 1R) ∼ 0R) || (((1R + 1R) ∼ 0R) → False)) → cauchy a
-convergentSequenceCauchy nontrivial {a} {r} a->r (inl 2=0) ε x with 1/nPositive 2 λ t → 2!=3 (characteristicWellDefined nontrivial {2} {3} twoIsPrime threeIsPrime (transitive (transitive +Associative identRight) 2=0) t)
-... | 0<1/3 with allInvertible (fromN 3) λ t → 2!=3 (characteristicWellDefined nontrivial {2} {3} twoIsPrime threeIsPrime (transitive (transitive +Associative identRight) 2=0) t)
-... | 1/3 , pr1/3 with a->r (1/3 * ε) (orderRespectsMultiplication 0<1/3 x)
-... | N , pr = N , λ {m} {n} → ans m n
-  where
-    2/3 : (1/3 + 1/3) < 1R
-    2/3 = <WellDefined reflexive (transitive (transitive (+WellDefined (transitive (symmetric identIsIdent) *Commutative) (transitive (+WellDefined (transitive (symmetric identIsIdent) *Commutative) (transitive (+WellDefined (symmetric (transitive *Commutative identIsIdent)) (symmetric timesZero)) (symmetric *DistributesOver+))) (symmetric *DistributesOver+))) (symmetric *DistributesOver+)) pr1/3) (<WellDefined reflexive (transitive (+WellDefined reflexive (symmetric identRight)) (symmetric +Associative)) (orderRespectsAddition (<WellDefined identLeft reflexive (orderRespectsAddition 0<1/3 1/3)) 1/3))
-    ans : (m n : ℕ) → N <N m → N <N n → abs (index a m + inverse (index a n)) < ε
-    ans m n N<m N<n = <Transitive (bothNearImpliesNear {r} (1/3 * ε) (orderRespectsMultiplication 0<1/3 x) (pr m N<m) (pr n N<n)) (<WellDefined *DistributesOver+' identIsIdent (ringCanMultiplyByPositive x 2/3))
-convergentSequenceCauchy _ {a} {r} a->r (inr 2!=0) e 0<e with halve 2!=0 e
+convergentSequenceCauchy : (nontrivial : 0R ∼ 1R → False) → {a : Sequence A} → {r : A} → a ~> r → cauchy a
+convergentSequenceCauchy _ {a} {r} a->r e 0<e with halve (λ i → charNotN 1 (transitive (transitive +Associative identRight) i)) e
 ... | e/2 , prE/2 with a->r e/2 (halvePositive' prE/2 0<e)
 ... | N , pr = N , λ {m} {n} → ans m n
  where
--- a/Fields/Orders/Partial/Lemmas.agda
+++ b/Fields/Orders/Partial/Lemmas.agda
@@ -1,28 +0,0 @@
-{-# OPTIONS --safe --warning=error --without-K #-}
-
-open import Rings.Definition
-open import Rings.Orders.Partial.Definition
-open import Setoids.Setoids
-open import Setoids.Orders
-open import Functions
-open import Fields.Fields
-open import Fields.Orders.Partial.Definition
-open import Numbers.Naturals.Semiring
-open import Sets.EquivalenceRelations
-open import LogicalFormulae
-open import Groups.Definition
-
-open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-
-module Fields.Orders.Partial.Lemmas {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {F : Field R} {p : _} {_<_ : Rel {_} {p} A} {pOrder : SetoidPartialOrder S _<_} (oF : PartiallyOrderedField F pOrder) where
-
-open Ring R
-open Group additiveGroup
-open Setoid S
-open Equivalence eq
-open Field F
-open PartiallyOrderedField oF
-open SetoidPartialOrder pOrder
-open import Rings.Orders.Partial.Lemmas oRing
-open import Rings.InitialRing R
-
--- a/Fields/Orders/Total/Lemmas.agda
+++ b/Fields/Orders/Total/Lemmas.agda
@@ -34,11 +34,11 @@ open import Rings.Orders.Partial.Lemmas oR
 open import Rings.Lemmas R
 open import Groups.Lemmas additiveGroup

-1/nPositive : (n : ℕ) → (charNotN : (fromN (succ n) ∼ 0R) → False) → 0R < underlying (allInvertible _ charNotN)
-1/nPositive 0 nNot0 with allInvertible (fromN 1) nNot0
-... | 1/1 , pr1 = <WellDefined reflexive (transitive (symmetric pr1) (transitive (transitive (*WellDefined reflexive identRight) *Commutative) identIsIdent)) (0<1 λ i → nNot0 (transitive identRight (symmetric i)))
-1/nPositive (succ n) nNot0 with allInvertible (fromN (succ (succ n))) nNot0
-... | 1/n , pr1/n with totality 0R 1/n
-... | inr x = exFalso (nNot0 (oneZeroImpliesAllZero (transitive (symmetric (transitive (*WellDefined (symmetric x) reflexive) timesZero')) pr1/n)))
-... | inl (inl x) = x
-... | inl (inr x) = exFalso (1<0False (<WellDefined pr1/n timesZero' (ringCanMultiplyByPositive (fromNPreservesOrder (anyComparisonImpliesNontrivial x) (succIsPositive (succ n))) x)))
+charNotN : (n : ℕ) → fromN (succ n) ∼ 0R → False
+charNotN n pr = irreflexive (<WellDefined reflexive pr t)
+  where
+    t : 0R < fromN (succ n)
+    t = fromNPreservesOrder (Field.nontrivial F) (succIsPositive n)
+
+charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False
+charNot2 pr = charNotN 1 (transitive (transitive +Associative identRight) pr)
--- a/Numbers/Naturals/Order.agda
+++ b/Numbers/Naturals/Order.agda
@@ -92,9 +92,23 @@ canRemoveSuccFrom<N {a} {b} (le x proof) rewrite commutative x (succ a) | commut
 a<SuccA : (a : ℕ) → a <N succ a
 a<SuccA a = le zero refl

+<NWellDefined : {a b : ℕ} → (p1 : a <N b) → (p2 : a <N b) → _<N_.x p1 ≡ _<N_.x p2
+<NWellDefined {a} {b} (le x proof) (le y proof1) = equalityCommutative r
+  where
+    q : y +N a ≡ x +N a
+    q = succInjective {y +N a} {x +N a} (transitivity proof1 (equalityCommutative proof))
+    r : y ≡ x
+    r = canSubtractFromEqualityRight q
+
 canAddToOneSideOfInequality : {a b : ℕ} (c : ℕ) → a <N b → a <N (b +N c)
 canAddToOneSideOfInequality {a} {b} c (le x proof) = le (x +N c) (transitivity (applyEquality succ (equalityCommutative (+Associative x c a))) (transitivity (applyEquality (λ i → (succ x) +N i) (commutative c a)) (transitivity (applyEquality succ (+Associative x a c)) (applyEquality (_+N c) proof))))

+canAddToOneSideOfInequality' : {a b : ℕ} (c : ℕ) → a <N b → a <N (c +N b)
+canAddToOneSideOfInequality' {a} {b} c (le x proof) = le (x +N c) ans
+  where
+    ans : succ ((x +N c) +N a) ≡ c +N b
+    ans rewrite (equalityCommutative (+Associative x c a)) | commutative c a | (+Associative x a c) = transitivity (applyEquality (_+N c) proof) (commutative b c)
+
 addingIncreases : (a b : ℕ) → a <N a +N succ b
 addingIncreases zero b = succIsPositive b
 addingIncreases (succ a) b = succPreservesInequality (addingIncreases a b)
@@ -107,14 +121,6 @@ noIntegersBetweenXAndSuccX {zero} x x<a a<sx = zeroNeverGreater x<a
 noIntegersBetweenXAndSuccX {succ a} x (le y proof) (le z proof1) with succInjective proof1
 ... | ah rewrite (equalityCommutative proof) | (succExtracts z (y +N x)) | +Associative (succ z) y x | commutative (succ (z +N y)) x = lessIrreflexive {x} (le (z +N y) (transitivity (commutative _ x) ah))

-<NWellDefined : {a b : ℕ} → (p1 : a <N b) → (p2 : a <N b) → _<N_.x p1 ≡ _<N_.x p2
-<NWellDefined {a} {b} (le x proof) (le y proof1) = equalityCommutative r
-  where
-    q : y +N a ≡ x +N a
-    q = succInjective {y +N a} {x +N a} (transitivity proof1 (equalityCommutative proof))
-    r : y ≡ x
-    r = canSubtractFromEqualityRight q
-
 private
  orderIsTotal : (a b : ℕ) → ((a <N b) || (b <N a)) || (a ≡ b)
  orderIsTotal zero zero = inr refl
@@ -192,6 +198,12 @@ canFlipMultiplicationsInIneq {a} {b} {c} {d} pr = identityOfIndiscernablesRight
 lessRespectsMultiplication : (a b c : ℕ) → (a <N b) → (zero <N c) → (a *N c <N b *N c)
 lessRespectsMultiplication a b c prAB cPos = canFlipMultiplicationsInIneq {c} {a} {c} {b} (lessRespectsMultiplicationLeft a b c prAB cPos)

+squash<N : {a b : ℕ} → .(a <N b) → a <N b
+squash<N {a} {b} a<b with orderIsTotal a b
+... | inl (inl x) = x
+... | inl (inr x) = exFalso (lessIrreflexive (orderIsTransitive x a<b))
+squash<N {a} {b} a<b | inr refl = exFalso (lessIrreflexive a<b)
+
 <NTo<N' : {a b : ℕ} → a <N b → a <N' b
 <NTo<N' (le x proof) = le' x proof

--- a/Numbers/Rationals/Definition.agda
+++ b/Numbers/Rationals/Definition.agda
@@ -90,6 +90,3 @@ negateQWellDefined a b a=b = inverseWellDefined (Ring.additiveGroup ℚRing) {a}

 ℚOrdered : TotallyOrderedRing ℚPOrdered
 ℚOrdered = fieldOfFractionsOrderedRing
-
-ℚcharNot2 : ((Ring.1R ℚRing) +Q (Ring.1R ℚRing)) =Q (Ring.0R ℚRing) → False
-ℚcharNot2 ()
--- a/Numbers/Reals/Definition.agda
+++ b/Numbers/Reals/Definition.agda
@@ -10,11 +10,11 @@ open import Functions
 module Numbers.Reals.Definition where

 open import Fields.CauchyCompletion.Definition ℚOrdered ℚField
-open import Fields.CauchyCompletion.Setoid ℚOrdered ℚField ℚcharNot2
-open import Fields.CauchyCompletion.Addition ℚOrdered ℚField ℚcharNot2
-open import Fields.CauchyCompletion.Multiplication ℚOrdered ℚField ℚcharNot2
-open import Fields.CauchyCompletion.Ring ℚOrdered ℚField ℚcharNot2
-open import Fields.CauchyCompletion.Comparison ℚOrdered ℚField ℚcharNot2
+open import Fields.CauchyCompletion.Setoid ℚOrdered ℚField
+open import Fields.CauchyCompletion.Addition ℚOrdered ℚField
+open import Fields.CauchyCompletion.Multiplication ℚOrdered ℚField
+open import Fields.CauchyCompletion.Ring ℚOrdered ℚField
+open import Fields.CauchyCompletion.Comparison ℚOrdered ℚField

 ℝ : Set
 ℝ = CauchyCompletion
--- a/Rings/Orders/Partial/Bounded.agda
+++ b/Rings/Orders/Partial/Bounded.agda
@@ -0,0 +1,35 @@
+{-# OPTIONS --safe --warning=error --without-K --guardedness #-}
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+open import Setoids.Setoids
+open import Rings.Definition
+open import Rings.Orders.Partial.Definition
+open import Sets.EquivalenceRelations
+open import Sequences
+open import Setoids.Orders
+open import Functions
+open import LogicalFormulae
+open import Numbers.Naturals.Semiring
+open import Groups.Definition
+
+module Rings.Orders.Partial.Bounded {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} (pRing : PartiallyOrderedRing R pOrder) where
+
+open Group (Ring.additiveGroup R)
+open import Groups.Lemmas (Ring.additiveGroup R)
+open Setoid S
+open Equivalence eq
+open SetoidPartialOrder pOrder
+
+BoundedAbove : Sequence A → Set (m ⊔ o)
+BoundedAbove x = Sg A (λ K → (n : ℕ) → index x n < K)
+
+BoundedBelow : Sequence A → Set (m ⊔ o)
+BoundedBelow x = Sg A (λ K → (n : ℕ) → K < index x n)
+
+Bounded : Sequence A → Set (m ⊔ o)
+Bounded x = Sg A (λ K → (n : ℕ) → ((Group.inverse (Ring.additiveGroup R) K) < index x n) && (index x n < K))
+
+boundNonzero : {s : Sequence A} → (b : Bounded s) → underlying b ∼ 0G → False
+boundNonzero {s} (a , b) isEq with b 0
+... | bad1 ,, bad2 = irreflexive (<Transitive bad1 (<WellDefined reflexive (transitive isEq (symmetric (transitive (inverseWellDefined isEq) invIdent))) bad2))
--- a/Rings/Orders/Total/Bounded.agda
+++ b/Rings/Orders/Total/Bounded.agda
@@ -0,0 +1,31 @@
+{-# OPTIONS --safe --warning=error --without-K --guardedness #-}
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+open import Setoids.Setoids
+open import Rings.Definition
+open import Rings.Orders.Partial.Definition
+open import Rings.Orders.Total.Definition
+open import Sets.EquivalenceRelations
+open import Sequences
+open import Setoids.Orders
+open import Functions
+open import LogicalFormulae
+open import Numbers.Naturals.Semiring
+open import Groups.Definition
+
+module Rings.Orders.Total.Bounded {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (tRing : TotallyOrderedRing pRing) where
+
+open import Rings.Orders.Partial.Bounded pRing
+open Ring R
+open Group additiveGroup
+open import Groups.Lemmas (Ring.additiveGroup R)
+open Setoid S
+open Equivalence eq
+open SetoidPartialOrder pOrder
+open import Rings.Orders.Total.Lemmas tRing
+open PartiallyOrderedRing pRing
+
+boundGreaterThanZero : {s : Sequence A} → (b : Bounded s) → 0G < underlying b
+boundGreaterThanZero {s} (a , b) with b 0
+... | (l ,, r) = halvePositive a (<WellDefined invLeft reflexive (orderRespectsAddition (<Transitive l r) a))
--- a/Rings/Orders/Total/Cauchy.agda
+++ b/Rings/Orders/Total/Cauchy.agda
@@ -0,0 +1,30 @@
+{-# OPTIONS --safe --warning=error --without-K --guardedness #-}
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Setoids.Setoids
+open import Rings.Definition
+open import Rings.Orders.Partial.Definition
+open import Rings.Orders.Total.Definition
+open import Groups.Definition
+open import Sets.EquivalenceRelations
+open import Sequences
+open import Setoids.Orders
+open import Functions
+open import LogicalFormulae
+open import Numbers.Naturals.Semiring
+open import Numbers.Naturals.Order
+
+module Rings.Orders.Total.Cauchy {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) where
+
+open Setoid S
+open SetoidTotalOrder (TotallyOrderedRing.total order)
+open SetoidPartialOrder pOrder
+open Equivalence eq
+open TotallyOrderedRing order
+open Ring R
+open Group additiveGroup
+
+open import Rings.Orders.Total.Lemmas order
+
+cauchy : Sequence A → Set (m ⊔ o)
+cauchy s = ∀ (ε : A) → (0R < ε) → Sg ℕ (λ N → ∀ {m n : ℕ} → (N <N m) → (N <N n) → abs ((index s m) -R (index s n)) < ε)
--- a/Rings/Orders/Total/Lemmas.agda
+++ b/Rings/Orders/Total/Lemmas.agda
@@ -363,3 +363,15 @@ fromNPreservesOrder : (0R ∼ 1R → False) → {a b : ℕ} → (a <N b) → (fr
 fromNPreservesOrder 0!=1 {zero} {succ zero} a<b = fromNIncreasing 0!=1 0
 fromNPreservesOrder 0!=1 {zero} {succ (succ b)} a<b = <Transitive (fromNPreservesOrder 0!=1 (succIsPositive b)) (fromNIncreasing 0!=1 (succ b))
 fromNPreservesOrder 0!=1 {succ a} {succ b} a<b = <WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (fromNPreservesOrder 0!=1 (canRemoveSuccFrom<N a<b)) 1R)
+
+reciprocalPositive : (a b : A) → .(0<a : 0R < a) → (a * b ∼ 1R) → 0R < b
+reciprocalPositive a 1/a 0<a ab=1 with totality 0G 1/a
+... | inl (inl x) = x
+... | inl (inr x) = exFalso (1<0False (<WellDefined (transitive *Commutative ab=1) timesZero' (ringCanMultiplyByPositive 0<a x)))
+... | inr x = exFalso (anyComparisonImpliesNontrivial 0<a (transitive (transitive (symmetric timesZero) (*WellDefined reflexive x)) ab=1))
+
+reciprocal<1 : (a b : A) → .(1<a : 1R < a) → (a * b ∼ 1R) → b < 1R
+reciprocal<1 a b 0<a ab=1 with totality b 1R
+... | inl (inl x) = x
+... | inr b=1 = exFalso (irreflexive (<WellDefined (symmetric ab=1) (transitive (symmetric identIsIdent) (transitive *Commutative ((*WellDefined reflexive (symmetric b=1))))) 0<a))
+... | inl (inr x) = exFalso (irreflexive (<WellDefined identIsIdent ab=1 (ringMultiplyPositives (0<1 (anyComparisonImpliesNontrivial 0<a)) (0<1 (anyComparisonImpliesNontrivial 0<a)) 0<a x)))
--- a/WithK.agda
+++ b/WithK.agda
@@ -1,11 +0,0 @@
-{-# OPTIONS --safe --warning=error #-}
-
-open import LogicalFormulae
-
-module WithK where
-
-typeCastEqual : {a : _} {A : Set a} {B : Set a} {el : A} (pr1 pr2 : A ≡ B) → (typeCast el pr1) ≡ (typeCast el pr2)
-typeCastEqual {a} {A} {.A} {el} refl refl = refl
-
-reflRefl : {a : _} {A : Set a} → {r s : A} → (pr1 pr2 : r ≡ s) → pr1 ≡ pr2
-reflRefl refl refl = refl