rename

Arithmetization/Basic/IOpen.lean

@@ -182,7 +182,7 @@ lemma div_mul (a b c : M) : a / (b * c) = a / b / c := by
   have : 1 * (a / b) ≤ b * (a / b) := mul_le_mul_of_nonneg_right (le_iff_lt_succ.mpr (by simp[pos])) (by simp)
   simpa using le_trans this (mul_div_le a b)
 
-instance div_polybounded : PolyBounded₂ ℒₒᵣ ((· / ·) : M → M → M) := ⟨#0, λ _ ↦ by simp⟩
+instance div_polybounded : Bounded₂ ℒₒᵣ ((· / ·) : M → M → M) := ⟨#0, λ _ ↦ by simp⟩
 
 instance div_definable : DefinableFunction₂ ℒₒᵣ Σ 0 ((· / ·) : M → M → M) := defined_to_with_param _ div_defined
 
@@ -348,7 +348,7 @@ lemma mod_mul_add_of_lt (a b : M) {r} (hr : r < b) : (a * b + r) % b = r := by
 @[simp] lemma mod_le (a b : M) : a % b ≤ a := by
   simp [mod_def]
 
-instance mod_polybounded : PolyBounded₂ ℒₒᵣ ((· % ·) : M → M → M) := ⟨#0, by intro v; simp⟩
+instance mod_polybounded : Bounded₂ ℒₒᵣ ((· % ·) : M → M → M) := ⟨#0, by intro v; simp⟩
 
 lemma mod_eq_zero_iff_dvd {a b : M} : b % a = 0 ↔ a ∣ b := by
   simp [mod_def]
@@ -507,7 +507,7 @@ lemma sqrt_three : √(3 : M) = 1 :=
     _ ≤ a      := sq_sqrt_le a
   simp_all
 
-instance : PolyBounded₁ ℒₒᵣ ((√·) : M → M) := ⟨#0, by intro v; simp⟩
+instance : Bounded₁ ℒₒᵣ ((√·) : M → M) := ⟨#0, by intro v; simp⟩
 
 lemma sqrt_lt_self_of_one_lt {a : M} (h : 1 < a) : √a < a := by
   by_contra A
@@ -552,7 +552,7 @@ lemma pair_defined : Δ₀-Function₂ (λ a b : M ↦ ⟪a, b⟫) via pairDef :
 
 instance pair_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (pair : M → M → M) := defined_to_with_param₀ _ pair_defined
 
-instance : PolyBounded₂ ℒₒᵣ (pair : M → M → M) :=
+instance : Bounded₂ ℒₒᵣ (pair : M → M → M) :=
   ⟨ᵀ“(#1 * #1 + #0) + (#0 * #0 + #0 + #1)”, by intro v; simp [pair]; split_ifs <;> try simp [pair, *]⟩
 
 def unpair (a : M) : M × M := if a - √a * √a < √a then (a - √a * √a, √a) else (√a, a - √a * √a - √a)
@@ -596,9 +596,9 @@ def pairEquiv : M × M ≃ M := ⟨Function.uncurry pair, unpair, fun ⟨a, b⟩
 
 @[simp] lemma pi₂_le_self (a : M) : π₂ a ≤ a := by simp [pi₂, unpair]; split_ifs <;> simp [add_assoc]
 
-instance : PolyBounded₁ ℒₒᵣ (pi₁ : M → M) := ⟨ᵀ“#0”, by intro v; simp⟩
+instance : Bounded₁ ℒₒᵣ (pi₁ : M → M) := ⟨ᵀ“#0”, by intro v; simp⟩
 
-instance : PolyBounded₁ ℒₒᵣ (pi₂ : M → M) := ⟨ᵀ“#0”, by intro v; simp⟩
+instance : Bounded₁ ℒₒᵣ (pi₂ : M → M) := ⟨ᵀ“#0”, by intro v; simp⟩
 
 def pi₁Def : Δ₀-Sentence 2 := ⟨“∃[#0 < #2 + 1] !pairDef [#2, #1, #0]”, by simp⟩
 

Arithmetization/Basic/PeanoMinus.lean

@@ -47,7 +47,7 @@ lemma sub_defined : Δ₀-Function₂ ((· - ·) : M → M → M) via subDef :=
 
 instance sub_definable (Γ s) : DefinableFunction₂ ℒₒᵣ Γ s ((· - ·) : M → M → M) := defined_to_with_param₀ subDef sub_defined
 
-instance sub_polybounded : PolyBounded₂ ℒₒᵣ ((· - ·) : M → M → M) := ⟨#0, λ _ ↦ by simp⟩
+instance sub_polybounded : Bounded₂ ℒₒᵣ ((· - ·) : M → M → M) := ⟨#0, λ _ ↦ by simp⟩
 
 @[simp] lemma sub_self (a : M) : a - a = 0 :=
   add_right_eq_self.mp (sub_spec_of_ge (a := a) (b := a) (by rfl)).symm

Arithmetization/IDeltaZero/Bit.lean

@@ -0,0 +1,73 @@
+import Arithmetization.IDeltaZero.Exponential.Exp
+import Arithmetization.IDeltaZero.Exponential.Log
+
+namespace LO.FirstOrder
+
+namespace Arith
+
+noncomputable section
+
+variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M]
+
+namespace Model
+
+variable [M ⊧ₘ* 𝐈𝚺₀]
+
+def Bit (i a : M) : Prop := ∃ p ≤ a, Exponential i p ∧ LenBit p a
+
+instance : Membership M M := ⟨Bit⟩
+
+def bitDef : Δ₀-Sentence 2 := ⟨“∃[#0 < #2 + 1] (!Exponential.def [#1, #0] ∧ !lenbitDef [#0, #2])”, by simp⟩
+
+lemma bit_defined : Δ₀-Relation ((· ∈ ·) : M → M → Prop) via bitDef := by
+  intro v; simp [bitDef, lenbit_defined.pval, Exponential.defined.pval, ←le_iff_lt_succ]; rfl
+
+instance mem_definable : DefinableRel ℒₒᵣ Σ 0 ((· ∈ ·) : M → M → Prop) := defined_to_with_param _ bit_defined
+
+lemma lt_of_mem {i a : M} (h : i ∈ a) : i < a := by
+  rcases h with ⟨p, _, hep, hp⟩
+  exact lt_of_lt_of_le hep.lt hp.le
+
+lemma mem_def (i a : M) : i ∈ a ↔ Bit i a := by rfl
+
+section
+
+variable {L : Language} [L.ORing] [Structure L M] [Structure.ORing L M] [Structure.Monotone L M]
+
+variable (Γ : Polarity) (n : ℕ)
+
+@[definability] lemma Definable.ball_mem {P : (Fin k → M) → M → Prop} {f : (Fin k → M) → M}
+    (hf : Semipolynomial L Γ n f) (h : Definable L Γ n (fun w ↦ P (w ·.succ) (w 0))) :
+    Definable L Γ n (fun v ↦ ∀ x ∈ f v, P v x) := by
+  rcases hf.bounded with ⟨bf, hbf⟩
+  rcases hf.definable with ⟨f_graph, hf_graph⟩
+  rcases h with ⟨p, hp⟩
+  exact ⟨⟨“∃[#0 < !!(Rew.bShift bf) + 1] (!f_graph ∧ ∀[#0 < #1] (!bitDef .[#0, #1] → !((Rew.substs (#0 :> (#·.succ.succ))).hom p)))”,
+    by simp; apply Hierarchy.oringEmb; simp⟩,
+    by  intro v; simp [hf_graph.eval, hp.eval, bit_defined.pval, ←le_iff_lt_succ]
+        constructor
+        · rintro h; exact ⟨f v, hbf v, rfl, fun x _ hx ↦ h x hx⟩
+        · rintro ⟨_, _, rfl, h⟩ x hx; exact h x (lt_of_mem hx) hx⟩
+
+@[definability] lemma Definable.bex_mem {P : (Fin k → M) → M → Prop} {f : (Fin k → M) → M}
+    (hf : Semipolynomial L Γ n f) (h : Definable L Γ n (fun w ↦ P (w ·.succ) (w 0))) :
+    Definable L Γ n (fun v ↦ ∃ x ∈ f v, P v x) := by
+  rcases hf.bounded with ⟨bf, hbf⟩
+  rcases hf.definable with ⟨f_graph, hf_graph⟩
+  rcases h with ⟨p, hp⟩
+  exact ⟨⟨“∃[#0 < !!(Rew.bShift bf) + 1] (!f_graph ∧ ∃[#0 < #1] (!bitDef .[#0, #1] ∧ !((Rew.substs (#0 :> (#·.succ.succ))).hom p)))”,
+    by simp; apply Hierarchy.oringEmb; simp⟩,
+    by  intro v; simp [hf_graph.eval, hp.eval, bit_defined.pval, ←le_iff_lt_succ]
+        constructor
+        · rintro ⟨x, hx, h⟩; exact ⟨f v, hbf v, rfl, x, lt_of_mem hx, hx, h⟩
+        · rintro ⟨_, _, rfl, x, _, hx, h⟩; exact ⟨x, hx, h⟩⟩
+
+end
+
+end Model
+
+end
+
+end Arith
+
+end LO.FirstOrder

Arithmetization/IDeltaZero/Exponential/Exp.lean

@@ -33,7 +33,7 @@ instance ext_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (ext : M → M →
 @[simp] lemma ext_le_add (u z : M) : ext u z ≤ z :=
   le_trans (mod_le (z / u) u) (by simp [add_comm])
 
-instance : PolyBounded₂ ℒₒᵣ (ext : M → M → M) := ⟨#1, by intro v; simp⟩
+instance : Bounded₂ ℒₒᵣ (ext : M → M → M) := ⟨#1, by intro v; simp⟩
 
 @[simp] lemma ext_lt {u} (z : M) (pos : 0 < u) : ext u z < u := by simp [ext, pos]
 
@@ -472,13 +472,13 @@ lemma range_pos {x y : M} (h : Exponential x y) : 0 < y := by
   · have : 2 ≤ ext u Y := two_le_ext_of_seq₀_of_seqₛ H₀ Hₛ ne2 hu ppu
     exact lt_of_lt_of_le (by simp) this
 
-lemma dom_lt_range {x y : M} (h : Exponential x y) : x < y := by
+lemma lt {x y : M} (h : Exponential x y) : x < y := by
   rcases h with (⟨rfl, rfl⟩ | ⟨X, bX, Y, bY, H₀, Hₛ, ⟨u, hu, ne2, ppu, rfl, rfl⟩⟩)
   · simp
   · exact ext_le_ext_of_seq₀_of_seqₛ H₀ Hₛ ne2 hu ppu
 
 lemma not_exponential_of_le {x y : M} (h : x ≤ y) : ¬Exponential y x := by
-  intro hxy; exact not_le.mpr (dom_lt_range hxy) h
+  intro hxy; exact not_le.mpr (lt hxy) h
 
 @[simp] lemma one_not_even (a : M) : 1 ≠ 2 * a := by
   intro h
@@ -518,20 +518,20 @@ lemma exponential_succ {x y : M} : Exponential (x + 1) y ↔ ∃ z, y = 2 * z 
           have : 1 < y := by
             simpa using (show 1 < y^2 from lt_of_le_of_lt (by simp) hxy)
           have : Exponential (x + 1) y ↔ ∃ z ≤ y, y = 2 * z ∧ Exponential x z :=
-            IH y (lt_square_of_lt $ this) (lt_trans _ _ _ (by simp) H'.dom_lt_range)
+            IH y (lt_square_of_lt $ this) (lt_trans _ _ _ (by simp) H'.lt)
           rcases this.mp H' with ⟨y, _, rfl, H''⟩
           exact ⟨2 * y ^ 2, by simp [sq, mul_assoc, mul_left_comm y 2],
             by simp [sq, mul_assoc, mul_left_comm y 2], H''.bit_one⟩
         · rintro ⟨y, _, rfl, H⟩
           rcases exponential_odd.mp H with ⟨y, rfl, H'⟩
           by_cases ne1 : y = 1
           · rcases ne1 with rfl
-            rcases (show x = 0 from by simpa using H'.dom_lt_range)
+            rcases (show x = 0 from by simpa using H'.lt)
             simp [one_add_one_eq_two, two_mul_two_eq_four]
           have : y < y^2 := lt_square_of_lt $ one_lt_iff_two_le.mpr $ H'.range_pow2.two_le ne1
           have : Exponential (x + 1) (2 * y) ↔ ∃ z ≤ 2 * y, 2 * y = 2 * z ∧ Exponential x z :=
             IH (2 * y) (by simp; exact lt_of_lt_of_le this le_two_mul_left)
-              (lt_of_lt_of_le H'.dom_lt_range $ by simp)
+              (lt_of_lt_of_le H'.lt $ by simp)
           have : Exponential (x + 1) (2 * y) := this.mpr ⟨y, by simp, rfl, H'⟩
           simpa [sq, mul_add, add_assoc, mul_assoc, one_add_one_eq_two, mul_left_comm y 2] using this.bit_zero
 
@@ -577,7 +577,7 @@ protected lemma uniq {x y₁ y₂ : M} : Exponential x y₁ → Exponential x y
   · exact Eq.symm <| this h₂ h₁ (show y₂ ≤ y₁ from le_of_not_ge h)
   revert x h y₁
   suffices ∀ x < y₂, ∀ y₁ ≤ y₂, Exponential x y₁ → Exponential x y₂ → y₁ = y₂ by
-    intro x y₁ h₁ h₂ hy; exact this x h₂.dom_lt_range y₁ hy h₁ h₂
+    intro x y₁ h₁ h₂ hy; exact this x h₂.lt y₁ hy h₁ h₂
   induction y₂ using order_induction_iSigmaZero
   · definability
   case ind y₂ IH =>
@@ -587,14 +587,14 @@ protected lemma uniq {x y₁ y₂ : M} : Exponential x y₁ → Exponential x y
     · rcases exponential_succ.mp h₁ with ⟨y₁, rfl, h₁'⟩
       rcases exponential_succ.mp h₂ with ⟨y₂, rfl, h₂'⟩
       have : y₁ = y₂ := IH y₂ (lt_mul_of_pos_of_one_lt_left h₂'.range_pos one_lt_two)
-        x h₂'.dom_lt_range y₁ (by simpa using h) h₁' h₂'
+        x h₂'.lt y₁ (by simpa using h) h₁' h₂'
       simp [this]
 
 protected lemma inj {x₁ x₂ y : M} : Exponential x₁ y → Exponential x₂ y → x₁ = x₂ := by
   intro h₁ h₂
   revert x₁ x₂ h₁ h₂
   suffices ∀ x₁ < y, ∀ x₂ < y, Exponential x₁ y → Exponential x₂ y → x₁ = x₂ by
-    intro x₁ x₂ h₁ h₂; exact this x₁ h₁.dom_lt_range x₂ h₂.dom_lt_range h₁ h₂
+    intro x₁ x₂ h₁ h₂; exact this x₁ h₁.lt x₂ h₂.lt h₁ h₂
   induction y using order_induction_iSigmaZero
   · definability
   case ind y IH =>
@@ -611,7 +611,7 @@ protected lemma inj {x₁ x₂ y : M} : Exponential x₁ y → Exponential x₂
       have hy₂ : Exponential x₂ y := h₂.of_succ_two_mul
       have : x₁ = x₂ :=
         IH y (lt_mul_of_pos_of_one_lt_left hy₁.range_pos one_lt_two)
-          x₁ hy₁.dom_lt_range x₂ hy₂.dom_lt_range hy₁ hy₂
+          x₁ hy₁.lt x₂ hy₂.lt hy₁ hy₂
       simp [this]
 
 lemma exponential_elim {x y : M} : Exponential x y ↔ (x = 0 ∧ y = 1) ∨ ∃ x', ∃ y', x = x' + 1 ∧ y = 2 * y' ∧ Exponential x' y' :=
@@ -628,7 +628,7 @@ lemma monotone {x₁ x₂ y₁ y₂ : M} : Exponential x₁ y₁ → Exponential
   suffices ∀ x₁ < y₁, ∀ y₂ ≤ y₁, ∀ x₂ < y₂, Exponential x₁ y₁ → Exponential x₂ y₂ → x₂ ≤ x₁ by
     intro h₁ h₂; contrapose; simp
     intro hy
-    exact this x₁ h₁.dom_lt_range y₂ hy x₂ h₂.dom_lt_range h₁ h₂
+    exact this x₁ h₁.lt y₂ hy x₂ h₂.lt h₁ h₂
   induction y₁ using order_induction_iSigmaZero
   · definability
   case ind y₁ IH =>
@@ -643,7 +643,7 @@ lemma monotone {x₁ x₂ y₁ y₂ : M} : Exponential x₁ y₁ → Exponential
     · rcases exponential_succ.mp h₁ with ⟨y₁, rfl, h₁'⟩
       rcases exponential_succ.mp h₂ with ⟨y₂, rfl, h₂'⟩
       have : x₂ ≤ x₁ := IH y₁ (lt_mul_of_pos_of_one_lt_left h₁'.range_pos one_lt_two)
-        x₁ h₁'.dom_lt_range y₂ (le_of_mul_le_mul_left hy (by simp)) x₂ h₂'.dom_lt_range h₁' h₂'
+        x₁ h₁'.lt y₂ (le_of_mul_le_mul_left hy (by simp)) x₂ h₂'.lt h₁' h₂'
       simpa using this
 
 lemma monotone_le {x₁ x₂ y₁ y₂ : M} (h₁ : Exponential x₁ y₁) (h₂ : Exponential x₂ y₂) : x₁ ≤ x₂ → y₁ ≤ y₂ := by
@@ -732,19 +732,13 @@ lemma exp_inj : Function.Injective (Exp.exp : M → M) := λ a _ H ↦
 lemma exp_succ (a : M) : exp (a + 1) = 2 * exp a :=
   exp_of_exponential <| Exponential.exponential_succ_mul_two.mpr <| exp_exponential a
 
-@[simp] lemma numeral_two_eq_two : (ORingSymbol.numeral 2 : M) = 2 := by simp [numeral_eq_natCast]
-
-@[simp] lemma numeral_three_eq_three : (ORingSymbol.numeral 3 : M) = 3 := by simp [numeral_eq_natCast]
-
-@[simp] lemma numeral_four_eq_four : (ORingSymbol.numeral 4 : M) = 4 := by simp [numeral_eq_natCast]
-
 instance models_exponential_of_models_iSigmaOne : M ⊧ₘ* 𝐄𝐗𝐏 :=
   ⟨by intro f hf; rcases hf <;> simp [models_iff, exp_succ]⟩
 
 lemma exp_even (a : M) : exp (2 * a) = (exp a)^2 :=
   exp_of_exponential <| Exponential.exponential_even_sq.mpr <| exp_exponential a
 
-@[simp] lemma lt_exp (a : M) : a < exp a := (exp_exponential a).dom_lt_range
+@[simp] lemma lt_exp (a : M) : a < exp a := (exp_exponential a).lt
 
 @[simp] lemma exp_pos (a : M) : 0 < exp a := (exp_exponential a).range_pos
 

Arithmetization/IDeltaZero/Exponential/Log.lean

@@ -74,10 +74,10 @@ lemma log_defined : Δ₀-Function₁ (log : M → M) via logDef := by
 
 instance log_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (log : M → M) := defined_to_with_param _ log_defined
 
-instance : PolyBounded₁ ℒₒᵣ (log : M → M) := ⟨#0, λ _ ↦ by simp⟩
+instance : Bounded₁ ℒₒᵣ (log : M → M) := ⟨#0, λ _ ↦ by simp⟩
 
 lemma log_eq_of_pos {x y : M} (pos : 0 < y) {y'} (H : Exponential x y') (hy' : y' ≤ y) (hy : y < 2 * y') : log y = x :=
-  (log_exists_unique_pos pos).unique ⟨log_lt_self_of_pos pos, log_pos pos⟩ ⟨lt_of_lt_of_le H.dom_lt_range hy', y', hy', H, hy⟩
+  (log_exists_unique_pos pos).unique ⟨log_lt_self_of_pos pos, log_pos pos⟩ ⟨lt_of_lt_of_le H.lt hy', y', hy', H, hy⟩
 
 @[simp] lemma log_one : log (1 : M) = 0 := log_eq_of_pos (by simp) (y' := 1) (by simp) (by rfl) (by simp [one_lt_two])
 
@@ -165,7 +165,7 @@ lemma length_defined : Δ₀-Function₁ (‖·‖ : M → M) via lengthDef := b
 
 instance length_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (‖·‖ : M → M) := defined_to_with_param _ length_defined
 
-instance : PolyBounded₁ ℒₒᵣ (‖·‖ : M → M) := ⟨#0, λ _ ↦ by simp⟩
+instance : Bounded₁ ℒₒᵣ (‖·‖ : M → M) := ⟨#0, λ _ ↦ by simp⟩
 
 @[simp] lemma length_one : ‖(1 : M)‖ = 1 := by simp [length_eq_binaryLength]
 
@@ -336,7 +336,7 @@ lemma bexp_defined : Δ₀-Function₂ (bexp : M → M → M) via bexpDef := by
 
 instance bexp_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (bexp : M → M → M) := defined_to_with_param _ bexp_defined
 
-instance : PolyBounded₂ ℒₒᵣ (bexp : M → M → M) := ⟨#0, λ _ ↦ by simp⟩
+instance : Bounded₂ ℒₒᵣ (bexp : M → M → M) := ⟨#0, λ _ ↦ by simp⟩
 
 lemma bexp_monotone_iff {a i j : M} (hi : i < ‖a‖) (hj : j < ‖a‖) : bexp a i < bexp a j ↔ i < j :=
   Iff.symm <| Exponential.monotone_iff (by simp [hi]) (by simp [hj])
@@ -351,7 +351,7 @@ lemma bexp_eq_of_lt_length {i a a' : M} (ha : i < ‖a‖) (ha' : i < ‖a'‖)
 
 @[simp] lemma bexp_pow2 {a x : M} (h : x < ‖a‖) : Pow2 (bexp a x) := (exp_bexp_of_lt h).range_pow2
 
-@[simp] lemma lt_bexp {a x : M} (h : x < ‖a‖) : x < bexp a x := (exp_bexp_of_lt h).dom_lt_range
+@[simp] lemma lt_bexp {a x : M} (h : x < ‖a‖) : x < bexp a x := (exp_bexp_of_lt h).lt
 
 @[simp] lemma bexp_pos {a x : M} (h : x < ‖a‖) : 0 < bexp a x := (exp_bexp_of_lt h).range_pos
 
@@ -415,7 +415,7 @@ lemma fbit_defined : Δ₀-Function₂ (fbit : M → M → M) via fbitDef := by
 
 instance fbit_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (fbit : M → M → M) := defined_to_with_param _ fbit_defined
 
-instance : PolyBounded₂ ℒₒᵣ (fbit : M → M → M) := ⟨ᵀ“1”, λ _ ↦ by simp⟩
+instance : Bounded₂ ℒₒᵣ (fbit : M → M → M) := ⟨ᵀ“1”, λ _ ↦ by simp⟩
 
 @[simp] lemma fbit_zero (i : M) : fbit 0 i = 0 := by simp [fbit]
 

Arithmetization/ISigmaOne/Bit.lean

@@ -266,30 +266,6 @@ lemma domain_exists_unique (s : M) :
     ∃! d : M, ∀ x, x ∈ d ↔ ∃ y, ⟪x, y⟫ ∈ s := by { }
 -/
 
-namespace ArithmetizedTerm
-
-variable (L : Language) [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)]
-
-variable (M)
-
-class ArithmetizedLanguage where
-  isFunc : Δ₀-Sentence 2
-  isFunc_spec : Δ₀-Relation (fun (k' f' : M) ↦ ∃ (k : ℕ) (f : L.Func k), k' = k ∧ f' = Encodable.encode f) via isFunc
-  isRel : Δ₀-Sentence 2
-  isRel_spec : Δ₀-Relation (fun (k' r' : M) ↦ ∃ (k : ℕ) (r : L.Rel k), k' = k ∧ r' = Encodable.encode r) via isRel
-
-variable {M L}
-
-def bvar (x : M) : M := ⟪0, ⟪0, x⟫⟫
-
-def fvar (x : M) : M := ⟪0, ⟪1, x⟫⟫
-
-def func : {k : ℕ} → (f : L.Func k) → M
-  | 0,     c => ⟪0, ⟪2, Encodable.encode c⟫⟫
-  | k + 1, f => ⟪k + 1, Encodable.encode f⟫
-
-end ArithmetizedTerm
-
 end ISigma₁
 
 end Model

Arithmetization/OmegaOne/Basic.lean

@@ -78,7 +78,7 @@ instance hash_definable : DefinableFunction₂ ℒₒᵣ Σ 0 (Hash.hash : M →
 
 @[simp] lemma hash_pos (a b : M) : 0 < a # b := (exponential_hash a b).range_pos
 
-@[simp] lemma hash_lt (a b : M) : ‖a‖ * ‖b‖ < a # b := (exponential_hash a b).dom_lt_range
+@[simp] lemma hash_lt (a b : M) : ‖a‖ * ‖b‖ < a # b := (exponential_hash a b).lt
 
 lemma length_hash (a b : M) : ‖a # b‖ = ‖a‖ * ‖b‖ + 1 := (exponential_hash a b).length_eq
 

Arithmetization/OmegaOne/Nuon.lean

@@ -84,7 +84,7 @@ lemma ext_defined : Δ₀-Function₃ (ext : M → M → M → M) via extDef :=
 
 instance ext_Definable : DefinableFunction₃ ℒₒᵣ Σ 0 (ext : M → M → M → M) := defined_to_with_param₀ _ ext_defined
 
-instance : PolyBounded₃ ℒₒᵣ (ext : M → M → M → M) := ⟨#1, λ _ ↦ by simp⟩
+instance : Bounded₃ ℒₒᵣ (ext : M → M → M → M) := ⟨#1, λ _ ↦ by simp⟩
 
 @[simp] lemma ext_zero (L i : M) : 0{L}[i] = 0 := by simp [ext]
 
@@ -567,7 +567,7 @@ lemma nuonAux_defined : Δ₀-Relation₃ (NuonAux : M → M → M → Prop) via
 
 instance nuonAux_definable : DefinableRel₃ ℒₒᵣ Σ 0 (NuonAux : M → M → M → Prop) := defined_to_with_param _ nuonAux_defined
 
-instance : PolyBounded₃ ℒₒᵣ (ext : M → M → M → M) := ⟨#1, λ _ ↦ by simp⟩
+instance : Bounded₃ ℒₒᵣ (ext : M → M → M → M) := ⟨#1, λ _ ↦ by simp⟩
 
 @[simp] lemma NuonAux.initial (A : M) : NuonAux A 0 0 := SeriesSegment.initial (by simp [polyU])
 

Arithmetization/Vorspiel/Lemmata.lean

@@ -84,6 +84,12 @@ variable {a b c : M}
 
 instance : Nonempty M := ⟨0⟩
 
+@[simp] lemma numeral_two_eq_two : (ORingSymbol.numeral 2 : M) = 2 := by simp [numeral_eq_natCast]
+
+@[simp] lemma numeral_three_eq_three : (ORingSymbol.numeral 3 : M) = 3 := by simp [numeral_eq_natCast]
+
+@[simp] lemma numeral_four_eq_four : (ORingSymbol.numeral 4 : M) = 4 := by simp [numeral_eq_natCast]
+
 lemma lt_succ_iff_le {x y : M} : x < y + 1 ↔ x ≤ y := Iff.symm le_iff_lt_succ
 
 lemma lt_iff_succ_le : a < b ↔ a + 1 ≤ b := by simp [le_iff_lt_succ]