Tower

Difficulty: optional — 8 definitions, 0 abbreviations, 20 lemmas, 11 theorems, 0 examples.

definition lemma theorem
legend

The infinite model need not be assumed. It can be built from the finite ones.

A tower is a sequence of finite models, each sitting inside the next as an initial segment: the embedding preserves and reflects the order, sends the bottom to the bottom, has nothing new appearing below an old element, and leaves at least one element uncovered, so the levels keep growing. The canonical tower is the sequence of universes of \(2, 3, 4, \dots\) elements, each an initial segment of the one after it.

Gluing the levels together gives the colimit: an element of a level and its image in the next level count as one and the same. The colimit is a model again, because everything up to one of its elements already lies inside a single level, and a level is finite. It is infinite, because it contains a copy of every level and the levels grow without bound. So by ultrafinitism the colimit satisfies Peano’s postulate. The standard model arrives as the limit of the finite ones.

A tower: finite models, each sitting inside the next as an initial segment.

tower-of-finite-models
structure Structure.Arithmetic.Tower : Type 1

  • The universe at each level.

    Level : ℕ → Type

  • Each level is a model.

    arith : (n : ℕ) → Structure.Arithmetic.Arith (self.Level n)

  • Each level is finite.

    finite : ∀ (n : ℕ), Finite (self.Level n)

  • The embedding of a level into the next.

    step : (n : ℕ) → self.Level n → self.Level (n + 1)

  • Distinct elements stay distinct.

    step_injective : ∀ (n : ℕ), Function.Injective (self.step n)

  • The order is preserved.

    step_mono : ∀ (n : ℕ) (a b : self.Level n), a ≤ b → self.step n a ≤ self.step n b

  • The bottom goes to the bottom.

    step_bot : ∀ (n : ℕ), self.step n ⊥ = ⊥

  • Below an old element everything is old: each level is an initial segment of the next.

    step_initial : ∀ (n : ℕ) (a : self.Level n), ∀ y ≤ self.step n a, ∃ b, y = self.step n b

  • Each level leaves at least one element of the next uncovered, so the levels keep growing.

    step_not_surjective : ∀ (n : ℕ), ¬Function.Surjective (self.step n)
Show details

Outer dependencies: (none)

Inner dependencies: Structure.Arithmetic.Arith

Mathlib dependencies: Finite

Lean core dependencies: Eq, Exists, Function.Injective, Function.Surjective, HEq, Nat, Not

Used by: Structure.Arithmetic.Tower.Colimit, Structure.Arithmetic.Tower.Same, Structure.Arithmetic.Tower.SigmaLe, Structure.Arithmetic.Tower.exists_of_le_ι, Structure.Arithmetic.Tower.instArithColimit, Structure.Arithmetic.Tower.instInfiniteColimit, Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.Tower.instNontrivialColimit, Structure.Arithmetic.Tower.instOrderBotColimit, Structure.Arithmetic.Tower.instPeanoColimit, Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.levelFinite, Structure.Arithmetic.Tower.lt_card_level, Structure.Arithmetic.Tower.same_refl, Structure.Arithmetic.Tower.same_symm, Structure.Arithmetic.Tower.same_trans, Structure.Arithmetic.Tower.setoid, Structure.Arithmetic.Tower.sigmaLe_antisymm, Structure.Arithmetic.Tower.sigmaLe_congr, Structure.Arithmetic.Tower.sigmaLe_refl, Structure.Arithmetic.Tower.sigmaLe_total, Structure.Arithmetic.Tower.sigmaLe_trans, Structure.Arithmetic.Tower.sigmaLe_up, Structure.Arithmetic.Tower.stepTo, Structure.Arithmetic.Tower.stepTo_bot, Structure.Arithmetic.Tower.stepTo_initial, Structure.Arithmetic.Tower.stepTo_le_iff, Structure.Arithmetic.Tower.stepTo_self, Structure.Arithmetic.Tower.stepTo_succ, Structure.Arithmetic.Tower.stepTo_trans, Structure.Arithmetic.Tower.step_le_iff, Structure.Arithmetic.Tower.ι, Structure.Arithmetic.Tower.ι_injective, Structure.Arithmetic.Tower.ι_le_iff, Structure.Arithmetic.Tower.ι_stepTo, Structure.Arithmetic.finTower

instance Structure.Arithmetic.Tower.levelFinite (T : Structure.Arithmetic.Tower) (n : ℕ) : Finite (T.Level n)
Show details 
fun T n => T.finite n

Complexity: 9 (size of the value term)

Outer dependencies: Structure.Arithmetic.Tower

Mathlib dependencies: Finite

Lean core dependencies: Nat

Used by: Structure.Arithmetic.Tower.instArithColimit, Structure.Arithmetic.Tower.lt_card_level

theorem Structure.Arithmetic.Tower.stepTo_self (T : Structure.Arithmetic.Tower) {m : ℕ} (x : T.Level m) :
  T.stepTo ⋯ x = x
Show details 
fun T {m} x => Nat.leRecOn_self x

Complexity: 23 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.stepTo

Mathlib dependencies: Nat.leRecOn_self, le_refl

Lean core dependencies: Eq, Nat

Used by: Structure.Arithmetic.Tower.stepTo_bot, Structure.Arithmetic.Tower.stepTo_initial, Structure.Arithmetic.Tower.stepTo_le_iff, Structure.Arithmetic.Tower.ι_le_iff, Structure.Arithmetic.Tower.ι_stepTo

theorem Structure.Arithmetic.Tower.stepTo_succ (T : Structure.Arithmetic.Tower) {m n : ℕ} (h : m ≤ n)
  (x : T.Level m) : T.stepTo ⋯ x = T.step n (T.stepTo h x)
Show details 
fun T {m n} h x => Nat.leRecOn_succ h x

Complexity: 63 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.stepTo

Mathlib dependencies: Nat.leRecOn_succ

Lean core dependencies: Eq, Nat, Nat.le_succ

Used by: Structure.Arithmetic.Tower.stepTo_bot, Structure.Arithmetic.Tower.stepTo_initial, Structure.Arithmetic.Tower.stepTo_le_iff

theorem Structure.Arithmetic.Tower.stepTo_trans (T : Structure.Arithmetic.Tower) {m n k : ℕ} (h₁ : m ≤ n)
  (h₂ : n ≤ k) (x : T.Level m) : T.stepTo ⋯ x = T.stepTo h₂ (T.stepTo h₁ x)
Show details 
fun T {m n k} h₁ h₂ x => Nat.leRecOn_trans h₁ h₂ x

Complexity: 59 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.stepTo

Mathlib dependencies: Nat.leRecOn_trans

Lean core dependencies: Eq, Nat

Used by: Structure.Arithmetic.Tower.same_trans, Structure.Arithmetic.Tower.sigmaLe_congr, Structure.Arithmetic.Tower.sigmaLe_up

The embeddings reflect the order as well as preserve it.

theorem Structure.Arithmetic.Tower.step_le_iff (T : Structure.Arithmetic.Tower) {n : ℕ} (a b : T.Level n) :
  T.step n a ≤ T.step n b ↔ a ≤ b
Show details 
fun T {n} a b =>
  {
    mp := fun h =>
      Decidable.byContradiction fun hab =>
        have hba := LT.lt.le (not_le.mp hab);
        have this := le_antisymm h (T.step_mono n b a hba);
        hab (le_of_eq (T.step_injective n this)),
    mpr := T.step_mono n a b }

Complexity: 1583 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.levelArith

Mathlib dependencies: le_antisymm, le_of_eq, not_le

Lean core dependencies: Decidable.byContradiction, Eq, Iff, Nat, Not

Used by: Structure.Arithmetic.Tower.stepTo_initial, Structure.Arithmetic.Tower.stepTo_le_iff

theorem Structure.Arithmetic.Tower.stepTo_le_iff (T : Structure.Arithmetic.Tower) {m n : ℕ} (h : m ≤ n)
  (a b : T.Level m) : T.stepTo h a ≤ T.stepTo h b ↔ a ≤ b
Show details 
fun T {m n} h a b =>
  Nat.le_induction
    (of_eq_true
      (Eq.trans
        (congrFun'
          (congrArg Iff
            (congr (congrArg LE.le (Structure.Arithmetic.Tower.stepTo_self T a))
              (Structure.Arithmetic.Tower.stepTo_self T b)))
          (a ≤ b))
        (iff_self (a ≤ b))))
    (fun n hn ih =>
      Eq.mpr
        (id
          (congrArg (fun _a => _a ≤ T.stepTo (Nat.le_succ_of_le hn) b ↔ a ≤ b)
            (Structure.Arithmetic.Tower.stepTo_succ T hn a)))
        (Eq.mpr
          (id
            (congrArg (fun _a => T.step n (T.stepTo hn a) ≤ _a ↔ a ≤ b)
              (Structure.Arithmetic.Tower.stepTo_succ T hn b)))
          (Eq.mpr
            (id
              (congrArg (fun _a => _a ↔ a ≤ b)
                (propext
                  (Structure.Arithmetic.Tower.step_le_iff T (T.stepTo hn a) (T.stepTo hn b)))))
            (Eq.mpr (id (congrArg (fun _a => _a ↔ a ≤ b) (propext ih))) Iff.rfl))))
    n h

Complexity: 9307 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.stepTo

Proof dependencies: Structure.Arithmetic.Tower.stepTo_self, Structure.Arithmetic.Tower.stepTo_succ, Structure.Arithmetic.Tower.step_le_iff

Mathlib dependencies: Nat.le_induction

Lean core dependencies: Eq, Eq.mpr, Eq.trans, Iff, Iff.rfl, Nat, Nat.le_refl, Nat.le_succ, Nat.le_succ_of_le, True, congr, congrArg, congrFun', id, iff_self, of_eq_true

Used by: Structure.Arithmetic.Tower.sigmaLe_up

Two elements of the tower name the same one when they agree at some higher level.

def Structure.Arithmetic.Tower.Same (T : Structure.Arithmetic.Tower) (x y : (n : ℕ) × T.Level n) : Prop
Show details 
| T.Same x y = ∃ k, ∃ (hx : x.fst ≤ k) (hy : y.fst ≤ k), T.stepTo hx x.snd = T.stepTo hy y.snd

Complexity: 203 (size of the value term)

Outer dependencies: Structure.Arithmetic.Tower

Inner dependencies: Structure.Arithmetic.Tower.stepTo

Lean core dependencies: Eq, Exists, Nat, Sigma

Used by: Structure.Arithmetic.Tower.same_refl, Structure.Arithmetic.Tower.same_symm, Structure.Arithmetic.Tower.same_trans, Structure.Arithmetic.Tower.setoid, Structure.Arithmetic.Tower.sigmaLe_antisymm, Structure.Arithmetic.Tower.sigmaLe_congr

theorem Structure.Arithmetic.Tower.same_refl (T : Structure.Arithmetic.Tower) (x : (n : ℕ) × T.Level n) :
  T.Same x x
Show details 
fun T x => Exists.intro x.fst (Exists.intro le_rfl (Exists.intro le_rfl rfl))

Complexity: 791 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Same

Proof dependencies: Structure.Arithmetic.Tower.stepTo

Mathlib dependencies: le_rfl

Lean core dependencies: Eq, Exists, Nat, Sigma, rfl

Used by: Structure.Arithmetic.Tower.setoid

theorem Structure.Arithmetic.Tower.same_symm (T : Structure.Arithmetic.Tower) {x y : (n : ℕ) × T.Level n}
  (h : T.Same x y) : T.Same y x
Show details 
fun T {x y} h =>
  Exists.casesOn h fun k h =>
    Exists.casesOn h fun hx h =>
      Exists.casesOn h fun hy h => Exists.intro k (Exists.intro hy (Exists.intro hx (Eq.symm h)))

Complexity: 1833 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Same

Proof dependencies: Structure.Arithmetic.Tower.stepTo

Lean core dependencies: Eq, Eq.symm, Exists, Nat, Sigma

Used by: Structure.Arithmetic.Tower.setoid, Structure.Arithmetic.Tower.sigmaLe_congr

theorem Structure.Arithmetic.Tower.same_trans (T : Structure.Arithmetic.Tower) {x y z : (n : ℕ) × T.Level n}
  (hxy : T.Same x y) (hyz : T.Same y z) : T.Same x z
Show details 
fun T {x y z} hxy hyz =>
  Exists.casesOn hxy fun k h =>
    Exists.casesOn h fun hx h =>
      Exists.casesOn h fun hy h =>
        Exists.casesOn hyz fun l h_1 =>
          Exists.casesOn h_1 fun hy' h_2 =>
            Exists.casesOn h_2 fun hz h' =>
              Exists.intro (max k l)
                (Exists.intro (LE.le.trans hx (le_max_left k l))
                  (Exists.intro (LE.le.trans hz (le_max_right k l))
                    (Eq.mpr
                      (id
                        (congrArg
                          (fun _a => _a = T.stepTo (LE.le.trans hz (le_max_right k l)) z.snd)
                          (Structure.Arithmetic.Tower.stepTo_trans T hx (le_max_left k l) x.snd)))
                      (Eq.mpr
                        (id
                          (congrArg
                            (fun _a =>
                              T.stepTo (le_max_left k l) _a =
                                T.stepTo (LE.le.trans hz (le_max_right k l)) z.snd)
                            h))
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a => _a = T.stepTo (LE.le.trans hz (le_max_right k l)) z.snd)
                              (Eq.symm
                                (Structure.Arithmetic.Tower.stepTo_trans T hy (le_max_left k l)
                                  y.snd))))
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a => _a = T.stepTo (LE.le.trans hz (le_max_right k l)) z.snd)
                                (Structure.Arithmetic.Tower.stepTo_trans T hy' (le_max_right k l)
                                  y.snd)))
                            (Eq.mpr
                              (id
                                (congrArg
                                  (fun _a =>
                                    T.stepTo (le_max_right k l) _a =
                                      T.stepTo (LE.le.trans hz (le_max_right k l)) z.snd)
                                  h'))
                              (Eq.mpr
                                (id
                                  (congrArg
                                    (fun _a =>
                                      _a = T.stepTo (LE.le.trans hz (le_max_right k l)) z.snd)
                                    (Eq.symm
                                      (Structure.Arithmetic.Tower.stepTo_trans T hz
                                        (le_max_right k l) z.snd))))
                                (Eq.refl
                                  (T.stepTo (LE.le.trans hz (le_max_right k l)) z.snd))))))))))

Complexity: 9899 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Same

Proof dependencies: Structure.Arithmetic.Tower.stepTo, Structure.Arithmetic.Tower.stepTo_trans

Mathlib dependencies: le_max_left, le_max_right

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Exists, Nat, Sigma, congrArg, id

Used by: Structure.Arithmetic.Tower.setoid

The colimit of the tower: the elements of all levels together, an element of a level and its image in the next counting as one and the same.

colimit
def Structure.Arithmetic.Tower.Colimit (T : Structure.Arithmetic.Tower) : Type
Show details 
| T.Colimit = Quotient T.setoid

Complexity: 19 (size of the value term)

Outer dependencies: Structure.Arithmetic.Tower

Inner dependencies: Structure.Arithmetic.Tower.setoid

Lean core dependencies: Nat, Quotient, Sigma

Used by: Structure.Arithmetic.Standard, Structure.Arithmetic.Tower.exists_of_le_ι, Structure.Arithmetic.Tower.instArithColimit, Structure.Arithmetic.Tower.instInfiniteColimit, Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.Tower.instNontrivialColimit, Structure.Arithmetic.Tower.instOrderBotColimit, Structure.Arithmetic.Tower.instPeanoColimit, Structure.Arithmetic.Tower.ι, Structure.Arithmetic.Tower.ι_injective, Structure.Arithmetic.Tower.ι_le_iff, Structure.Arithmetic.Tower.ι_stepTo, Structure.Arithmetic.instPeanoStandard

Comparison at a common level.

def Structure.Arithmetic.Tower.SigmaLe (T : Structure.Arithmetic.Tower) (x y : (n : ℕ) × T.Level n) :
  Prop
Show details 
| T.SigmaLe x y = ∃ k, ∃ (hx : x.fst ≤ k) (hy : y.fst ≤ k), T.stepTo hx x.snd ≤ T.stepTo hy y.snd

Complexity: 265 (size of the value term)

Outer dependencies: Structure.Arithmetic.Tower

Inner dependencies: Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.stepTo

Lean core dependencies: Exists, Nat, Sigma

Used by: Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.Tower.sigmaLe_antisymm, Structure.Arithmetic.Tower.sigmaLe_congr, Structure.Arithmetic.Tower.sigmaLe_refl, Structure.Arithmetic.Tower.sigmaLe_total, Structure.Arithmetic.Tower.sigmaLe_trans, Structure.Arithmetic.Tower.sigmaLe_up, Structure.Arithmetic.instPeanoStandard

Comparison is the same at whatever level it is read.

theorem Structure.Arithmetic.Tower.sigmaLe_up (T : Structure.Arithmetic.Tower) {x y : (n : ℕ) × T.Level n}
  {k : ℕ} (hx : x.fst ≤ k) (hy : y.fst ≤ k) (h : T.SigmaLe x y) :
  T.stepTo hx x.snd ≤ T.stepTo hy y.snd
Show details 
fun T {x y} {k} hx hy h =>
  Exists.casesOn h fun l h =>
    Exists.casesOn h fun hx' h =>
      Exists.casesOn h fun hy' hle =>
        have hkl := le_max_left k l;
        have hlk := le_max_right k l;
        have h1 :=
          (Structure.Arithmetic.Tower.stepTo_le_iff T hlk (T.stepTo hx' x.snd)
                (T.stepTo hy' y.snd)).mpr
            hle;
        (Structure.Arithmetic.Tower.stepTo_le_iff T hkl (T.stepTo hx x.snd) (T.stepTo hy y.snd)).mp
          (Eq.mp
            (congrArg (fun _a => T.stepTo hkl (T.stepTo hx x.snd) ≤ _a)
              (Structure.Arithmetic.Tower.stepTo_trans T hy hkl y.snd))
            (Eq.mp
              (congrArg (fun _a => _a ≤ T.stepTo (LE.le.trans hy' hlk) y.snd)
                (Structure.Arithmetic.Tower.stepTo_trans T hx hkl x.snd))
              (Eq.mp
                (congrArg (fun _a => T.stepTo (LE.le.trans hx' hlk) x.snd ≤ _a)
                  (Eq.symm (Structure.Arithmetic.Tower.stepTo_trans T hy' hlk y.snd)))
                (Eq.mp
                  (congrArg (fun _a => _a ≤ T.stepTo hlk (T.stepTo hy' y.snd))
                    (Eq.symm (Structure.Arithmetic.Tower.stepTo_trans T hx' hlk x.snd)))
                  h1))))

Complexity: 7672 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.SigmaLe, Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.stepTo

Proof dependencies: Structure.Arithmetic.Tower.stepTo_le_iff, Structure.Arithmetic.Tower.stepTo_trans

Mathlib dependencies: le_max_left, le_max_right

Lean core dependencies: Eq.mp, Eq.symm, Exists, Nat, Sigma, congrArg

Used by: Structure.Arithmetic.Tower.exists_of_le_ι, Structure.Arithmetic.Tower.sigmaLe_antisymm, Structure.Arithmetic.Tower.sigmaLe_congr, Structure.Arithmetic.Tower.sigmaLe_trans, Structure.Arithmetic.Tower.ι_le_iff

theorem Structure.Arithmetic.Tower.sigmaLe_congr (T : Structure.Arithmetic.Tower)
  {x x' y y' : (n : ℕ) × T.Level n} (hx : T.Same x x') (hy : T.Same y y') :
  T.SigmaLe x y = T.SigmaLe x' y'
Show details 
fun T {x x' y y'} hx hy =>
  have key := fun {a a' b b'} a_1 =>
    Exists.casesOn (motive := fun x => T.Same b b' → T.SigmaLe a b → T.SigmaLe a' b') a_1 fun k h =>
      Exists.casesOn (motive := fun x => T.Same b b' → T.SigmaLe a b → T.SigmaLe a' b') h
        fun hak h =>
        Exists.casesOn (motive := fun x => T.Same b b' → T.SigmaLe a b → T.SigmaLe a' b') h
          fun hak' hae a_2 =>
          Exists.casesOn (motive := fun x => T.SigmaLe a b → T.SigmaLe a' b') a_2 fun l h =>
            Exists.casesOn (motive := fun x => T.SigmaLe a b → T.SigmaLe a' b') h fun hbl h =>
              Exists.casesOn (motive := fun x => T.SigmaLe a b → T.SigmaLe a' b') h
                fun hbl' hbe hab =>
                Exists.intro (max k l)
                  (Exists.intro (LE.le.trans hak' (le_max_left k l))
                    (Exists.intro (LE.le.trans hbl' (le_max_right k l))
                      (Eq.mpr
                        (id
                          (congrArg
                            (fun _a => _a ≤ T.stepTo (LE.le.trans hbl' (le_max_right k l)) b'.snd)
                            (Structure.Arithmetic.Tower.stepTo_trans T hak' (le_max_left k l)
                              a'.snd)))
                        (Eq.mpr
                          (id
                            (congrArg
                              (fun _a =>
                                T.stepTo (le_max_left k l) _a ≤
                                  T.stepTo (LE.le.trans hbl' (le_max_right k l)) b'.snd)
                              (Eq.symm hae)))
                          (Eq.mpr
                            (id
                              (congrArg
                                (fun _a =>
                                  _a ≤ T.stepTo (LE.le.trans hbl' (le_max_right k l)) b'.snd)
                                (Eq.symm
                                  (Structure.Arithmetic.Tower.stepTo_trans T hak (le_max_left k l)
                                    a.snd))))
                            (Eq.mpr
                              (id
                                (congrArg
                                  (fun _a =>
                                    T.stepTo (LE.le.trans hak (le_max_left k l)) a.snd ≤ _a)
                                  (Structure.Arithmetic.Tower.stepTo_trans T hbl' (le_max_right k l)
                                    b'.snd)))
                              (Eq.mpr
                                (id
                                  (congrArg
                                    (fun _a =>
                                      T.stepTo (LE.le.trans hak (le_max_left k l)) a.snd ≤
                                        T.stepTo (le_max_right k l) _a)
                                    (Eq.symm hbe)))
                                (Eq.mpr
                                  (id
                                    (congrArg
                                      (fun _a =>
                                        T.stepTo (LE.le.trans hak (le_max_left k l)) a.snd ≤ _a)
                                      (Eq.symm
                                        (Structure.Arithmetic.Tower.stepTo_trans T hbl
                                          (le_max_right k l) b.snd))))
                                  (Structure.Arithmetic.Tower.sigmaLe_up T
                                    (LE.le.trans hak (le_max_left k l))
                                    (LE.le.trans hbl (le_max_right k l)) hab)))))))));
  propext
    { mp := key hx hy,
      mpr :=
        key (Structure.Arithmetic.Tower.same_symm T hx)
          (Structure.Arithmetic.Tower.same_symm T hy) }

Complexity: 14582 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Same, Structure.Arithmetic.Tower.SigmaLe

Proof dependencies: Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.same_symm, Structure.Arithmetic.Tower.sigmaLe_up, Structure.Arithmetic.Tower.stepTo, Structure.Arithmetic.Tower.stepTo_trans

Mathlib dependencies: le_max_left, le_max_right

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Exists, Nat, Sigma, congrArg, id

Used by: Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.instPeanoStandard

theorem Structure.Arithmetic.Tower.sigmaLe_refl (T : Structure.Arithmetic.Tower) (x : (n : ℕ) × T.Level n) :
  T.SigmaLe x x
Show details 
fun T x => Exists.intro x.fst (Exists.intro le_rfl (Exists.intro le_rfl le_rfl))

Complexity: 1307 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.SigmaLe

Proof dependencies: Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.stepTo

Mathlib dependencies: le_rfl

Lean core dependencies: Exists, Nat, Sigma

Used by: Structure.Arithmetic.Tower.instLinearOrderColimit

theorem Structure.Arithmetic.Tower.sigmaLe_trans (T : Structure.Arithmetic.Tower)
  {x y z : (n : ℕ) × T.Level n} (hxy : T.SigmaLe x y) (hyz : T.SigmaLe y z) : T.SigmaLe x z
Show details 
fun T {x y z} hxy hyz =>
  have hx := LE.le.trans (le_max_left x.fst y.fst) (le_max_left (max x.fst y.fst) z.fst);
  have hy := LE.le.trans (le_max_right x.fst y.fst) (le_max_left (max x.fst y.fst) z.fst);
  have hz := le_max_right (max x.fst y.fst) z.fst;
  Exists.intro (max (max x.fst y.fst) z.fst)
    (Exists.intro hx
      (Exists.intro hz
        (LE.le.trans (Structure.Arithmetic.Tower.sigmaLe_up T hx hy hxy)
          (Structure.Arithmetic.Tower.sigmaLe_up T hy hz hyz))))

Complexity: 3788 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.SigmaLe

Proof dependencies: Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.sigmaLe_up, Structure.Arithmetic.Tower.stepTo

Mathlib dependencies: le_max_left, le_max_right

Lean core dependencies: Exists, Nat, Sigma

Used by: Structure.Arithmetic.Tower.instLinearOrderColimit

theorem Structure.Arithmetic.Tower.sigmaLe_antisymm (T : Structure.Arithmetic.Tower)
  {x y : (n : ℕ) × T.Level n} (hxy : T.SigmaLe x y) (hyx : T.SigmaLe y x) : T.Same x y
Show details 
fun T {x y} hxy hyx =>
  Exists.intro (max x.fst y.fst)
    (Exists.intro (le_max_left x.fst y.fst)
      (Exists.intro (le_max_right x.fst y.fst)
        (le_antisymm
          (Structure.Arithmetic.Tower.sigmaLe_up T (le_max_left x.fst y.fst)
            (le_max_right x.fst y.fst) hxy)
          (Structure.Arithmetic.Tower.sigmaLe_up T (le_max_right x.fst y.fst)
            (le_max_left x.fst y.fst) hyx))))

Complexity: 1745 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Same, Structure.Arithmetic.Tower.SigmaLe

Proof dependencies: Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.sigmaLe_up, Structure.Arithmetic.Tower.stepTo

Mathlib dependencies: le_antisymm, le_max_left, le_max_right

Lean core dependencies: Eq, Exists, Nat, Sigma

Used by: Structure.Arithmetic.Tower.instLinearOrderColimit

theorem Structure.Arithmetic.Tower.sigmaLe_total (T : Structure.Arithmetic.Tower)
  (x y : (n : ℕ) × T.Level n) : T.SigmaLe x y ∨ T.SigmaLe y x
Show details 
fun T x y =>
  have hx := le_max_left x.fst y.fst;
  have hy := le_max_right x.fst y.fst;
  Or.casesOn (le_total (T.stepTo hx x.snd) (T.stepTo hy y.snd))
    (fun h => Or.inl (Exists.intro (max x.fst y.fst) (Exists.intro hx (Exists.intro hy h))))
    fun h => Or.inr (Exists.intro (max x.fst y.fst) (Exists.intro hy (Exists.intro hx h)))

Complexity: 5951 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.SigmaLe

Proof dependencies: Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.stepTo

Mathlib dependencies: le_max_left, le_max_right, le_total

Lean core dependencies: Exists, Nat, Or, Sigma

Used by: Structure.Arithmetic.Tower.instLinearOrderColimit

instance Structure.Arithmetic.Tower.instLinearOrderColimit (T : Structure.Arithmetic.Tower) :
  LinearOrder T.Colimit
Show details 
| T.instLinearOrderColimit =
  { le := Quotient.lift₂ T.SigmaLe ⋯, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯, min := fun a b => if Quotient.lift₂ T.SigmaLe ⋯ a b then a else b,
    max := fun a b => if Quotient.lift₂ T.SigmaLe ⋯ a b then b else a,
    compare := fun a b => compareOfLessAndEq a b, le_total := ⋯,
    toDecidableLE := fun x x_1 => Classical.dec (x ≤ x_1), min_def := ⋯, max_def := ⋯,
    compare_eq_compareOfLessAndEq := ⋯ }

Complexity: 5203 (size of the value term)

Outer dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Colimit

Inner dependencies: Structure.Arithmetic.Tower.SigmaLe, Structure.Arithmetic.Tower.setoid, Structure.Arithmetic.Tower.sigmaLe_antisymm, Structure.Arithmetic.Tower.sigmaLe_congr, Structure.Arithmetic.Tower.sigmaLe_refl, Structure.Arithmetic.Tower.sigmaLe_total, Structure.Arithmetic.Tower.sigmaLe_trans

Mathlib dependencies: Classical.dec, LinearOrder, decidableEqOfDecidableLE, decidableLTOfDecidableLE

Lean core dependencies: And, Eq, Iff.rfl, Nat, Not, Or, Ordering, Quotient.lift₂, Quotient.sound, Sigma, compareOfLessAndEq, ite

Used by: Structure.Arithmetic.Tower.exists_of_le_ι, Structure.Arithmetic.Tower.instArithColimit, Structure.Arithmetic.Tower.instNontrivialColimit, Structure.Arithmetic.Tower.instOrderBotColimit, Structure.Arithmetic.Tower.ι_injective, Structure.Arithmetic.Tower.ι_le_iff

theorem Structure.Arithmetic.Tower.ι_le_iff (T : Structure.Arithmetic.Tower) {n : ℕ} (a b : T.Level n) :
  T.ι n a ≤ T.ι n b ↔ a ≤ b
Show details 
fun T {n} a b =>
  {
    mp := fun h =>
      have this := Structure.Arithmetic.Tower.sigmaLe_up T le_rfl le_rfl h;
      Eq.mpr (id ge_iff_le._simp_1)
        (Eq.mp
          (congr (congrArg LE.le (Structure.Arithmetic.Tower.stepTo_self T a))
            (Structure.Arithmetic.Tower.stepTo_self T b))
          this),
    mpr := fun h =>
      Exists.intro n
        (Exists.intro le_rfl
          (Exists.intro le_rfl
            (Eq.mpr
              (id
                (congr (congrArg LE.le (Structure.Arithmetic.Tower.stepTo_self T a))
                  (Structure.Arithmetic.Tower.stepTo_self T b)))
              h))) }

Complexity: 5834 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Colimit, Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.ι

Proof dependencies: Structure.Arithmetic.Tower.sigmaLe_up, Structure.Arithmetic.Tower.stepTo, Structure.Arithmetic.Tower.stepTo_self

Mathlib dependencies: le_rfl

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Exists, Iff, Nat, congr, congrArg, id

Used by: Structure.Arithmetic.Tower.instNontrivialColimit, Structure.Arithmetic.Tower.ι_injective

theorem Structure.Arithmetic.Tower.ι_stepTo (T : Structure.Arithmetic.Tower) {m n : ℕ} (h : m ≤ n)
  (x : T.Level m) : T.ι n (T.stepTo h x) = T.ι m x
Show details 
fun T {m n} h x =>
  Quotient.sound
    (Exists.intro n
      (Exists.intro le_rfl
        (Exists.intro h
          (of_eq_true
            (Eq.trans
              (congrFun' (congrArg Eq (Structure.Arithmetic.Tower.stepTo_self T (T.stepTo h x)))
                (T.stepTo h x))
              (eq_self (T.stepTo h x)))))))

Complexity: 1763 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Colimit, Structure.Arithmetic.Tower.stepTo, Structure.Arithmetic.Tower.ι

Proof dependencies: Structure.Arithmetic.Tower.setoid, Structure.Arithmetic.Tower.stepTo_self

Mathlib dependencies: le_rfl

Lean core dependencies: Eq, Eq.trans, Exists, Nat, Quotient.sound, Sigma, True, congrArg, congrFun', eq_self, of_eq_true

Used by: Structure.Arithmetic.Tower.exists_of_le_ι

Nothing new appears below an old element, however many levels are stepped through.

theorem Structure.Arithmetic.Tower.stepTo_initial (T : Structure.Arithmetic.Tower) {m n : ℕ} (h : m ≤ n)
  (a : T.Level m) (y : T.Level n) (hy : y ≤ T.stepTo h a) : ∃ b, y = T.stepTo h b
Show details 
fun T {m n} h a y hy =>
  Nat.le_induction
    (fun y hy =>
      Exists.intro y
        (of_eq_true
          (Eq.trans (congrArg (Eq y) (Structure.Arithmetic.Tower.stepTo_self T y)) (eq_self y))))
    (fun n hn ih y hy =>
      Exists.casesOn
        (T.step_initial n (T.stepTo hn a) y
          (Eq.mp (congrArg (fun _a => y ≤ _a) (Structure.Arithmetic.Tower.stepTo_succ T hn a)) hy))
        fun c h =>
        Eq.ndrec (motive := fun y =>
          y ≤ T.step n (T.stepTo hn a) → ∃ b, y = T.stepTo (Nat.le_succ_of_le hn) b)
          (fun hy =>
            Exists.casesOn
              (ih c ((Structure.Arithmetic.Tower.step_le_iff T c (T.stepTo hn a)).mp hy)) fun b h =>
              Eq.ndrec (motive := fun c =>
                T.step n c ≤ T.step n (T.stepTo hn a) →
                  ∃ b, T.step n c = T.stepTo (Nat.le_succ_of_le hn) b)
                (fun hy => Exists.intro b (Eq.symm (Structure.Arithmetic.Tower.stepTo_succ T hn b)))
                (Eq.symm h) hy)
          (Eq.symm h)
          (Eq.mp (congrArg (fun _a => y ≤ _a) (Structure.Arithmetic.Tower.stepTo_succ T hn a)) hy))
    n h y hy

Complexity: 5695 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.stepTo

Proof dependencies: Structure.Arithmetic.Tower.stepTo_self, Structure.Arithmetic.Tower.stepTo_succ, Structure.Arithmetic.Tower.step_le_iff

Mathlib dependencies: Nat.le_induction

Lean core dependencies: Eq, Eq.mp, Eq.symm, Eq.trans, Exists, Nat, Nat.le_refl, Nat.le_succ, Nat.le_succ_of_le, True, congrArg, eq_self, of_eq_true

Used by: Structure.Arithmetic.Tower.exists_of_le_ι

Everything below an element of a level already lies in that level.

theorem Structure.Arithmetic.Tower.exists_of_le_ι (T : Structure.Arithmetic.Tower) {n : ℕ} {a : T.Level n}
  {z : T.Colimit} (hz : z ≤ T.ι n a) : ∃ b, z = T.ι n b
Show details 
fun T {n} {a} {z} hz =>
  Quotient.ind (motive := fun {z} => z ≤ T.ι n a → ∃ b, z = T.ι n b)
    (fun x hz =>
      Sigma.casesOn (motive := fun x => ⟦x⟧ ≤ T.ι n a → ∃ b, ⟦x⟧ = T.ι n b) x
        (fun m y hz =>
          have hm := le_max_left m n;
          have ha := le_max_right m n;
          have hle := Structure.Arithmetic.Tower.sigmaLe_up T hm ha hz;
          Exists.casesOn (Structure.Arithmetic.Tower.stepTo_initial T ha a (T.stepTo hm y) hle)
            fun b hb =>
            Exists.intro b
              (Eq.mpr
                (id
                  (congrArg (fun _a => ⟦⟨m, y⟩⟧ = _a)
                    (Eq.symm (Structure.Arithmetic.Tower.ι_stepTo T ha b))))
                (Eq.mpr (id (congrArg (fun _a => ⟦⟨m, y⟩⟧ = T.ι (max m n) _a) (Eq.symm hb)))
                  (Eq.mpr
                    (id
                      (congrArg (fun _a => ⟦⟨m, y⟩⟧ = _a)
                        (Structure.Arithmetic.Tower.ι_stepTo T hm y)))
                    (Eq.refl ⟦⟨m, y⟩⟧)))))
        hz)
    z hz

Complexity: 2484 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Colimit, Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.Tower.ι

Proof dependencies: Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.setoid, Structure.Arithmetic.Tower.sigmaLe_up, Structure.Arithmetic.Tower.stepTo, Structure.Arithmetic.Tower.stepTo_initial, Structure.Arithmetic.Tower.ι_stepTo

Mathlib dependencies: le_max_left, le_max_right

Lean core dependencies: Eq, Eq.mpr, Eq.symm, Exists, Nat, Quotient.ind, Quotient.mk, Sigma, congrArg, id

Used by: Structure.Arithmetic.Tower.instArithColimit

theorem Structure.Arithmetic.Tower.stepTo_bot (T : Structure.Arithmetic.Tower) {n : ℕ} : T.stepTo ⋯ ⊥ = ⊥
Show details 
fun T {n} =>
  Nat.recAux
    (of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (Structure.Arithmetic.Tower.stepTo_self T ⊥)) ⊥)
        (eq_self ⊥)))
    (fun n ih =>
      Eq.mpr
        (id
          (congrArg (fun _a => _a = ⊥)
            (Structure.Arithmetic.Tower.stepTo_succ T (Nat.zero_le n) ⊥)))
        (Eq.mpr (id (congrArg (fun _a => T.step n _a = ⊥) ih))
          (Eq.mpr (id (congrArg (fun _a => _a = ⊥) (T.step_bot n))) (Eq.refl ⊥))))
    n

Complexity: 10875 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.stepTo

Proof dependencies: Structure.Arithmetic.Tower.stepTo_self, Structure.Arithmetic.Tower.stepTo_succ

Lean core dependencies: Eq, Eq.mpr, Eq.trans, Nat, Nat.le_succ, Nat.recAux, Nat.zero_le, True, congrArg, congrFun', eq_self, id, of_eq_true

Used by: Structure.Arithmetic.Tower.instOrderBotColimit

instance Structure.Arithmetic.Tower.instOrderBotColimit (T : Structure.Arithmetic.Tower) : OrderBot T.Colimit
Show details 
| T.instOrderBotColimit = { bot := T.ι 0 ⊥, bot_le := ⋯ }

Complexity: 211 (size of the value term)

Outer dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Colimit, Structure.Arithmetic.Tower.instLinearOrderColimit

Inner dependencies: Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.setoid, Structure.Arithmetic.Tower.stepTo, Structure.Arithmetic.Tower.stepTo_bot, Structure.Arithmetic.Tower.ι

Mathlib dependencies: OrderBot, bot_le, le_rfl

Lean core dependencies: Eq, Eq.mpr, Exists, Nat, Nat.zero_le, Sigma, congrArg, id

Used by: Structure.Arithmetic.Tower.instArithColimit

instance Structure.Arithmetic.Tower.instNontrivialColimit (T : Structure.Arithmetic.Tower) :
  Nontrivial T.Colimit
Show details 
fun T =>
  Exists.casesOn Nontrivial.exists_pair_ne fun a h =>
    Exists.casesOn h fun b hab =>
      {
        exists_pair_ne :=
          Exists.intro (T.ι 0 a)
            (Exists.intro (T.ι 0 b) fun h =>
              hab
                (le_antisymm ((Structure.Arithmetic.Tower.ι_le_iff T a b).mp (Eq.le h))
                  ((Structure.Arithmetic.Tower.ι_le_iff T b a).mp (Eq.ge h)))) }

Complexity: 1311 (size of the value term)

Outer dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Colimit

Inner dependencies: Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.ι, Structure.Arithmetic.Tower.ι_le_iff

Mathlib dependencies: Eq.ge, Eq.le, Nontrivial, le_antisymm

Lean core dependencies: Eq, Exists, Nat, Ne

Used by: Structure.Arithmetic.Tower.instArithColimit, Structure.Arithmetic.instPeanoStandard

The colimit is a model: everything up to one of its elements lies inside a single level, and a level is finite.

instance Structure.Arithmetic.Tower.instArithColimit (T : Structure.Arithmetic.Tower) :
  Structure.Arithmetic.Arith T.Colimit
Show details 
| T.instArithColimit =
  { toLinearOrder := T.instLinearOrderColimit, toOrderBot := T.instOrderBotColimit,
    toNontrivial := ⋯, reach := ⋯ }

Complexity: 23 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Colimit

Inner dependencies: Structure.Arithmetic.Tower.exists_of_le_ι, Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.Tower.instNontrivialColimit, Structure.Arithmetic.Tower.instOrderBotColimit, Structure.Arithmetic.Tower.levelFinite, Structure.Arithmetic.Tower.setoid, Structure.Arithmetic.Tower.ι

Mathlib dependencies: Set, Set.Finite, Set.Finite.subset, Set.Iic, Set.finite_range, Set.range

Lean core dependencies: Eq, Eq.symm, Exists, Nat, Sigma, rfl

Used by: Structure.Arithmetic.Tower.instPeanoColimit

theorem Structure.Arithmetic.Tower.ι_injective (T : Structure.Arithmetic.Tower) (n : ℕ) :
  Function.Injective (T.ι n)
Show details 
fun T n a b h =>
  le_antisymm ((Structure.Arithmetic.Tower.ι_le_iff T a b).mp (Eq.le h))
    ((Structure.Arithmetic.Tower.ι_le_iff T b a).mp (Eq.ge h))

Complexity: 507 (size of the value term)

Dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Colimit, Structure.Arithmetic.Tower.ι

Proof dependencies: Structure.Arithmetic.Tower.instLinearOrderColimit, Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.ι_le_iff

Mathlib dependencies: Eq.ge, Eq.le, le_antisymm

Lean core dependencies: Eq, Function.Injective, Nat

Used by: Structure.Arithmetic.Tower.instInfiniteColimit

Levels grow: each holds more elements than the one below.

theorem Structure.Arithmetic.Tower.lt_card_level (T : Structure.Arithmetic.Tower) (n : ℕ) :
  n < Nat.card (T.Level n)
Show details 
fun T n =>
  Nat.recAux
    (have this := Nontrivial.exists_pair_ne;
    have this := Finite.one_lt_card_iff_nontrivial.mpr { exists_pair_ne := this };
    Decidable.byContradiction fun a => Structure.Arithmetic.Tower.lt_card_level._proof_1_1 T this a)
    (fun n ih =>
      have this :=
        have x := Fintype.ofFinite (T.Level n);
        have x_1 := Fintype.ofFinite (T.Level (n + 1));
        have this :=
          Fintype.card_lt_of_injective_not_surjective (T.step n) (T.step_injective n)
            (T.step_not_surjective n);
        Eq.mpr
          (id
            (Eq.trans (congr (congrArg LT.lt Nat.card_eq_fintype_card) Nat.card_eq_fintype_card)
              gt_iff_lt._simp_1))
          this;
      Decidable.byContradiction fun a =>
        Structure.Arithmetic.Tower.lt_card_level._proof_1_2 T n ih this a)
    n

Complexity: 1453 (size of the value term)

Dependencies: Structure.Arithmetic.Tower

Proof dependencies: Structure.Arithmetic.Tower.levelFinite

Mathlib dependencies: Finite.one_lt_card_iff_nontrivial, Fintype, Fintype.card, Fintype.card_lt_of_injective_not_surjective, Fintype.ofFinite, Nat.card, Nat.card_eq_fintype_card, Nontrivial

Lean core dependencies: Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mpr, Eq.symm, Eq.trans, Exists, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_2, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.le_of_not_lt, Nat.recAux, Ne, Not, congr, congrArg, id, le_of_le_of_eq, of_decide_eq_true

Used by: Structure.Arithmetic.Tower.instInfiniteColimit

The colimit is infinite: it holds a copy of every level, and the levels grow without bound.

instance Structure.Arithmetic.Tower.instInfiniteColimit (T : Structure.Arithmetic.Tower) : Infinite T.Colimit
Show details 
fun T =>
  Eq.mpr (id (congrArg (fun _a => _a) (Eq.symm (propext not_finite_iff_infinite)))) fun hfin =>
    let N := Nat.card T.Colimit;
    have hN := rfl;
    have hle := Nat.card_le_card_of_injective (T.ι N) (Structure.Arithmetic.Tower.ι_injective T N);
    have this := Structure.Arithmetic.Tower.lt_card_level T N;
    Structure.Arithmetic.Tower.instInfiniteColimit._proof_1 T hle this

Complexity: 201 (size of the value term)

Outer dependencies: Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Colimit

Inner dependencies: Structure.Arithmetic.Tower.lt_card_level, Structure.Arithmetic.Tower.ι, Structure.Arithmetic.Tower.ι_injective

Mathlib dependencies: Finite, Infinite, Nat.card, Nat.card_le_card_of_injective, not_finite_iff_infinite

Lean core dependencies: Bool, Decidable.decide, Eq, Eq.mpr, Eq.symm, Eq.trans, Int, Int.add_one_le_of_lt, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.tidy_sat, Nat, Nat.cast, Not, congrArg, id, le_of_le_of_eq, of_decide_eq_true, rfl

Used by: Structure.Arithmetic.Tower.instPeanoColimit

The infinite model is reached rather than assumed: the colimit of a tower of finite models is infinite, so by ultrafinitism it satisfies Peano’s postulate.

instance Structure.Arithmetic.Tower.instPeanoColimit (T : Structure.Arithmetic.Tower) :
  Structure.Arithmetic.Peano T.Colimit
Show details 
| T.instPeanoColimit = { toArith := T.instArithColimit, peano := ⋯ }

Complexity: 15 (size of the value term)

Outer dependencies: Structure.Arithmetic.Peano, Structure.Arithmetic.Tower, Structure.Arithmetic.Tower.Colimit

Inner dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.NonPeano, Structure.Arithmetic.S, Structure.Arithmetic.Tower.instArithColimit, Structure.Arithmetic.Tower.instInfiniteColimit, Structure.Arithmetic.Z, Structure.Arithmetic.ultrafinitism

Mathlib dependencies: Finite, Infinite, not_finite_iff_infinite

Lean core dependencies: And, Exists, Nonempty, Not, inferInstance

Used by: (none)

The canonical tower: the universes of \(n + 2\) elements, each an initial segment of the next.

def Structure.Arithmetic.finTower : Structure.Arithmetic.Tower
Show details 
| Structure.Arithmetic.finTower =
  { Level := fun n => Fin (n + 2), arith := fun n => inferInstance,
    finite := Structure.Arithmetic.finTower._proof_4, step := fun x => Fin.castSucc,
    step_injective := Structure.Arithmetic.finTower._proof_5,
    step_mono := Structure.Arithmetic.finTower._proof_6,
    step_bot := Structure.Arithmetic.finTower._proof_8,
    step_initial := Structure.Arithmetic.finTower._proof_9,
    step_not_surjective := Structure.Arithmetic.finTower._proof_10 }

Complexity: 139 (size of the value term)

Outer dependencies: Structure.Arithmetic.Tower

Inner dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.instArithFin

Mathlib dependencies: Fin.castSucc_injective, Finite

Lean core dependencies: Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mp, Eq.mpr, Eq.symm, Eq.trans, Exists, False, Fin, Fin.castSucc, Fin.ext, Fin.last, Fin.le_def, Fin.val_castSucc, Fin.val_last, Function.Surjective, Int, Int.add_one_le_of_lt, Int.natCast_add, Int.sub_eq_zero_of_eq, Int.sub_nonneg_of_le, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addEquality_sat, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.ofNat_lt_of_lt, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_2, Lean.Omega.LinearCombo.coordinate_eval_3, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, Nat, Nat.cast, Nat.le_of_not_lt, Not, congrArg, eq_self, id, inferInstance, le_of_le_of_eq, of_decide_eq_true, of_eq_true, rfl

Used by: Structure.Arithmetic.Standard, Structure.Arithmetic.instPeanoStandard

The standard model, as the colimit of the finite ones.

def Structure.Arithmetic.Standard : Type
Show details 
| Structure.Arithmetic.Standard = Structure.Arithmetic.finTower.Colimit

Complexity: 3 (size of the value term)

Outer dependencies: (none)

Inner dependencies: Structure.Arithmetic.Tower.Colimit, Structure.Arithmetic.finTower

Used by: Structure.Arithmetic.instPeanoStandard

instance Structure.Arithmetic.instPeanoStandard : Structure.Arithmetic.Peano Structure.Arithmetic.Standard
Show details 
| Structure.Arithmetic.instPeanoStandard =
  { le := Structure.Arithmetic.instPeanoStandard._aux_1,
    lt := Structure.Arithmetic.instPeanoStandard._aux_3,
    le_refl := Structure.Arithmetic.instPeanoStandard._proof_5,
    le_trans := Structure.Arithmetic.instPeanoStandard._proof_6,
    lt_iff_le_not_ge := Structure.Arithmetic.instPeanoStandard._proof_7,
    le_antisymm := Structure.Arithmetic.instPeanoStandard._proof_8,
    min := Structure.Arithmetic.instPeanoStandard._aux_9,
    max := Structure.Arithmetic.instPeanoStandard._aux_11,
    compare := Structure.Arithmetic.instPeanoStandard._aux_13,
    le_total := Structure.Arithmetic.instPeanoStandard._proof_15,
    toDecidableLE := fun a b => Classical.propDecidable (a ≤ b),
    toDecidableEq := Structure.Arithmetic.instPeanoStandard._aux_16,
    toDecidableLT := Structure.Arithmetic.instPeanoStandard._aux_18,
    min_def := Structure.Arithmetic.instPeanoStandard._proof_20,
    max_def := Structure.Arithmetic.instPeanoStandard._proof_21,
    compare_eq_compareOfLessAndEq := Structure.Arithmetic.instPeanoStandard._proof_22,
    bot := Structure.Arithmetic.instPeanoStandard._aux_23,
    bot_le := Structure.Arithmetic.instPeanoStandard._proof_25,
    toNontrivial := Structure.Arithmetic.instPeanoStandard._proof_26,
    reach := Structure.Arithmetic.instPeanoStandard._proof_27,
    peano := Structure.Arithmetic.instPeanoStandard._proof_28 }

Complexity: 261 (size of the value term)

Outer dependencies: Structure.Arithmetic.Peano, Structure.Arithmetic.Standard

Inner dependencies: Structure.Arithmetic.Tower.Colimit, Structure.Arithmetic.Tower.SigmaLe, Structure.Arithmetic.Tower.instNontrivialColimit, Structure.Arithmetic.Tower.levelArith, Structure.Arithmetic.Tower.setoid, Structure.Arithmetic.Tower.sigmaLe_congr, Structure.Arithmetic.Tower.ι, Structure.Arithmetic.finTower

Mathlib dependencies: Classical.dec, decidableEqOfDecidableLE, decidableLTOfDecidableLE

Lean core dependencies: And, Nat, Not, Quotient.lift₂, Sigma, compareOfLessAndEq, ite

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend