@[simp]

theorem LO.Arith.Nuon.llen_lt_len_hash_len {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (K : V) : ‖‖K‖‖ < ‖K # ‖K‖‖

theorem LO.Arith.Nuon.mul_len_lt_len_hash {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {i : V} {I : V} {L : V} (hi : i ≤ ‖I‖) : i * ‖L‖ < ‖I # L‖

theorem LO.Arith.Nuon.mul_len_lt_len_hash' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {i : V} {K : V} {z : V} (hi : i ≤ ‖z‖) : i * ‖‖K‖‖ < ‖z # ‖K‖‖

def LO.Arith.Nuon.ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (L : V) (S : V) (i : V) : V

Equations

• LO.Arith.Nuon.ext L S i = S / LO.Arith.bexp S (i * ‖L‖) % L # 1

theorem LO.Arith.Nuon.ext_eq_zero_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L : V} {S : V} {i : V} (h : ‖S‖ ≤ i * ‖L‖) : LO.Arith.Nuon.ext L S i = 0

@[simp]

theorem LO.Arith.Nuon.ext_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (L : V) (S : V) (i : V) : LO.Arith.Nuon.ext L S i ≤ S

theorem LO.Arith.Nuon.ext_graph_aux {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (z : V) (S : V) (L : V) (i : V) : z = LO.Arith.Nuon.ext L S i ↔ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, LO.Arith.Exponential (i * ‖L‖) b ∧ z = S / b % L # 1)

theorem LO.Arith.Nuon.ext_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (z : V) (S : V) (L : V) (i : V) : z = LO.Arith.Nuon.ext L S i ↔ ∃ lS ≤ S, lS = ‖S‖ ∧ ∃ lL ≤ L, lL = ‖L‖ ∧ (lS ≤ i * lL → z = 0) ∧ (i * lL < lS → ∃ b ≤ S, LO.Arith.Exponential (i * lL) b ∧ ∃ hL ≤ 2 * L + 1, LO.Arith.Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)

def LO.Arith.Nuon.extDef : 𝚺₀.Semisentence 4

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LO.Arith.Nuon.cons_app_seven {α : Type u_2} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 7 = s 6

@[simp]

theorem LO.Arith.Nuon.cons_app_eight {α : Type u_2} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 8 = s 7

@[simp]

theorem LO.Arith.Nuon.cons_app_nine {α : Type u_2} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 9 = s 8

theorem LO.Arith.Nuon.ext_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Function₃ LO.Arith.Nuon.ext via LO.Arith.Nuon.extDef

instance LO.Arith.Nuon.ext_Definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Function₃ LO.Arith.Nuon.ext

Equations

• ⋯ = ⋯

instance LO.Arith.Nuon.instBounded₃Ext {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : LO.FirstOrder.Arith.Bounded₃ LO.Arith.Nuon.ext

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.Nuon.ext_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (L : V) (i : V) : LO.Arith.Nuon.ext L 0 i = 0

theorem LO.Arith.Nuon.ext_zero_eq_self_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L : V} {S : V} (h : ‖S‖ ≤ ‖L‖) : LO.Arith.Nuon.ext L S 0 = S

theorem LO.Arith.Nuon.ext_eq_of_ge {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L : V} {S : V} {S' : V} {i : V} (h : S ≤ S') : S / LO.Arith.bexp S' (i * ‖L‖) % L # 1 = LO.Arith.Nuon.ext L S i

theorem LO.Arith.Nuon.ext_eq_of_gt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L : V} {S : V} {S' : V} {i : V} (h : i * ‖L‖ < ‖S'‖) : S / LO.Arith.bexp S' (i * ‖L‖) % L # 1 = LO.Arith.Nuon.ext L S i

theorem LO.Arith.Nuon.ext_eq_hash_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {I : V} {L : V} {S : V} {i : V} (h : i ≤ ‖I‖) : S / LO.Arith.bexp (I # L) (i * ‖L‖) % L # 1 = LO.Arith.Nuon.ext L S i

theorem LO.Arith.Nuon.ext_add₁_pow2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L : V} {i : V} {S₁ : V} {S₂ : V} {p : V} (pp : LO.Arith.Pow2 p) (h : (i + 1) * ‖L‖ < ‖p‖) : LO.Arith.Nuon.ext L (S₁ + S₂ * p) i = LO.Arith.Nuon.ext L S₁ i

theorem LO.Arith.Nuon.ext_add₁_bexp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {I : V} {L : V} {i : V} {j : V} {S₁ : V} {S₂ : V} (hi : i ≤ ‖I‖) (hij : j < i) : LO.Arith.Nuon.ext L (S₁ + S₂ * LO.Arith.bexp (I # L) (i * ‖L‖)) j = LO.Arith.Nuon.ext L S₁ j

theorem LO.Arith.Nuon.ext_add₂_bexp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L : V} {I : V} {i : V} {j : V} {S₁ : V} {S₂ : V} (hij : i + j ≤ ‖I‖) (hS₁ : ‖S₁‖ ≤ i * ‖L‖) : LO.Arith.Nuon.ext L (S₁ + S₂ * LO.Arith.bexp (I # L) (i * ‖L‖)) (i + j) = LO.Arith.Nuon.ext L S₂ j

def LO.Arith.Nuon.append {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I : V) (L : V) (S : V) (i : V) (X : V) : V

Equations

• LO.Arith.Nuon.append I L S i X = S % LO.Arith.bexp (I # L) (i * ‖L‖) + X * LO.Arith.bexp (I # L) (i * ‖L‖)

theorem LO.Arith.Nuon.append_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I : V) (L : V) (S : V) (i : V) : LO.Arith.Nuon.append I L S i 0 = S % LO.Arith.bexp (I # L) (i * ‖L‖)

theorem LO.Arith.Nuon.len_append {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I : V) (L : V) (S : V) {i : V} {X : V} (hi : i ≤ ‖I‖) (hX : 0 < X) : ‖LO.Arith.Nuon.append I L S i X‖ = ‖X‖ + i * ‖L‖

theorem LO.Arith.Nuon.append_lt_hash {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I : V) (L : V) (S : V) {i : V} {X : V} (hi : i < ‖I‖) (hX : ‖X‖ ≤ ‖L‖) : LO.Arith.Nuon.append I L S i X < I # L

theorem LO.Arith.Nuon.append_lt_sq_hash {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I : V) (L : V) (S : V) {i : V} {X : V} (hi : i ≤ ‖I‖) (hX : ‖X‖ ≤ ‖L‖) (Ipos : 0 < I) : LO.Arith.Nuon.append I L S i X < (I # L) ^ 2

theorem LO.Arith.Nuon.ext_append_last {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I : V) (L : V) (S : V) {i : V} {X : V} (hi : i ≤ ‖I‖) (hX : ‖X‖ ≤ ‖L‖) : LO.Arith.Nuon.ext L (LO.Arith.Nuon.append I L S i X) i = X

theorem LO.Arith.Nuon.ext_append_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (I : V) (L : V) (S : V) {i : V} {j : V} {X : V} (hi : i ≤ ‖I‖) (hij : j < i) : LO.Arith.Nuon.ext L (LO.Arith.Nuon.append I L S i X) j = LO.Arith.Nuon.ext L S j

def LO.Arith.Nuon.IsSegment {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (L : V) (A : V) (start : V) (intv : V) (S : V) : Prop

Equations

• LO.Arith.Nuon.IsSegment L A start intv S = ∀ i < intv, LO.Arith.Nuon.ext L S (i + 1) = LO.Arith.Nuon.ext L S i + LO.Arith.fbit A (start + i)

def LO.Arith.Nuon.Segment {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (U : V) (L : V) (A : V) (start : V) (intv : V) (nₛ : V) (nₑ : V) : Prop

Equations

• LO.Arith.Nuon.Segment U L A start intv nₛ nₑ = ∃ S < U, LO.Arith.Nuon.IsSegment L A start intv S ∧ LO.Arith.Nuon.ext L S 0 = nₛ ∧ LO.Arith.Nuon.ext L S intv = nₑ

def LO.Arith.Nuon.IsSeries {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (U : V) (I : V) (L : V) (A : V) (iter : V) (T : V) : Prop

Equations

• LO.Arith.Nuon.IsSeries U I L A iter T = ∀ l < iter, LO.Arith.Nuon.Segment U L A (‖I‖ * l) ‖I‖ (LO.Arith.Nuon.ext L T l) (LO.Arith.Nuon.ext L T (l + 1))

def LO.Arith.Nuon.Series {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (U : V) (I : V) (L : V) (A : V) (iter : V) (n : V) : Prop

Equations

• LO.Arith.Nuon.Series U I L A iter n = ∃ T < U, LO.Arith.Nuon.IsSeries U I L A iter T ∧ LO.Arith.Nuon.ext L T 0 = 0 ∧ LO.Arith.Nuon.ext L T iter = n

def LO.Arith.Nuon.SeriesSegment {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (U : V) (I : V) (L : V) (A : V) (k : V) (n : V) : Prop

Equations

• LO.Arith.Nuon.SeriesSegment U I L A k n = ∃ nₖ ≤ n, LO.Arith.Nuon.Series U I L A (k / ‖I‖) nₖ ∧ LO.Arith.Nuon.Segment U L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) nₖ n

theorem LO.Arith.Nuon.SeriesSegment.series {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {I : V} {L : V} {A : V} {k : V} {n : V} (H : LO.Arith.Nuon.SeriesSegment U I L A k n) : ∃ (T : V) (S : V), LO.Arith.Nuon.IsSeries U I L A (k / ‖I‖) T ∧ LO.Arith.Nuon.IsSegment L A (‖I‖ * (k / ‖I‖)) (k % ‖I‖) S ∧ LO.Arith.Nuon.ext L T 0 = 0 ∧ LO.Arith.Nuon.ext L T (k / ‖I‖) = LO.Arith.Nuon.ext L S 0 ∧ LO.Arith.Nuon.ext L S (k % ‖I‖) = n

theorem LO.Arith.Nuon.IsSegment.le_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {L : V} {A : V} {start : V} {intv : V} {S : V} (H : LO.Arith.Nuon.IsSegment L A start intv S) (i : V) : i ≤ intv → LO.Arith.Nuon.ext L S i ≤ LO.Arith.Nuon.ext L S 0 + i

theorem LO.Arith.Nuon.Segment.refl {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (U : V) (L : V) (A : V) (start : V) (n : V) (hL : L # 1 ≤ U) (hn : ‖n‖ ≤ ‖L‖) : LO.Arith.Nuon.Segment U L A start 0 n n

theorem LO.Arith.Nuon.Segment.le_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {L : V} {A : V} {start : V} {intv : V} {nₛ : V} {nₑ : V} (H : LO.Arith.Nuon.Segment U L A start intv nₛ nₑ) : nₑ ≤ nₛ + intv

theorem LO.Arith.Nuon.Segment.uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {L : V} {A : V} {start : V} {intv : V} {nₛ : V} {nₑ₁ : V} {nₑ₂ : V} (H₁ : LO.Arith.Nuon.Segment U L A start intv nₛ nₑ₁) (H₂ : LO.Arith.Nuon.Segment U L A start intv nₛ nₑ₂) : nₑ₁ = nₑ₂

theorem LO.Arith.Nuon.IsSeries.le_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {I : V} {L : V} {A : V} {iter : V} {T : V} (H : LO.Arith.Nuon.IsSeries U I L A iter T) (l : V) : l ≤ iter → LO.Arith.Nuon.ext L T l ≤ LO.Arith.Nuon.ext L T 0 + ‖I‖ * l

theorem LO.Arith.Nuon.Series.le_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {I : V} {L : V} {A : V} {iter : V} {n : V} (H : LO.Arith.Nuon.Series U I L A iter n) : n ≤ ‖I‖ * iter

theorem LO.Arith.Nuon.Series.uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {I : V} {L : V} {A : V} {iter : V} {n₁ : V} {n₂ : V} (H₁ : LO.Arith.Nuon.Series U I L A iter n₁) (H₂ : LO.Arith.Nuon.Series U I L A iter n₂) : n₁ = n₂

theorem LO.Arith.Nuon.SeriesSegment.le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {I : V} {L : V} {A : V} {k : V} {n : V} (H : LO.Arith.Nuon.SeriesSegment U I L A k n) : n ≤ k

theorem LO.Arith.Nuon.SeriesSegment.initial {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {I : V} {L : V} {A : V} (Upos : 0 < U) : LO.Arith.Nuon.SeriesSegment U I L A 0 0

theorem LO.Arith.Nuon.SeriesSegment.zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {I : V} {L : V} {k : V} (Upos : 0 < U) : LO.Arith.Nuon.SeriesSegment U I L 0 k 0

theorem LO.Arith.Nuon.SeriesSegment.uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {I : V} {L : V} {A : V} {k : V} {n₁ : V} {n₂ : V} (H₁ : LO.Arith.Nuon.SeriesSegment U I L A k n₁) (H₂ : LO.Arith.Nuon.SeriesSegment U I L A k n₂) : n₁ = n₂

theorem LO.Arith.Nuon.Segment.succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {I : V} {L : V} {A : V} (hU : (I # L) ^ 2 ≤ U) {start : V} {intv : V} {nₛ : V} {nₑ : V} (H : LO.Arith.Nuon.Segment U L A start intv nₛ nₑ) (hintv : intv < ‖I‖) (hnₛ : ‖nₛ + ‖I‖‖ ≤ ‖L‖) : LO.Arith.Nuon.Segment U L A start (intv + 1) nₛ (nₑ + LO.Arith.fbit A (start + intv))

theorem LO.Arith.Nuon.Series.succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {I : V} {L : V} {A : V} (hU : (I # L) ^ 2 ≤ U) (hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖) {iter : V} {n : V} {n' : V} (HT : LO.Arith.Nuon.Series U I L A iter n) (HS : LO.Arith.Nuon.Segment U L A (‖I‖ * iter) ‖I‖ n n') (hiter : iter < ‖I‖) : LO.Arith.Nuon.Series U I L A (iter + 1) n'

theorem LO.Arith.Nuon.div_mod_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) (b : V) : (a + 1) / b = a / b + 1 ∧ (a + 1) % b = 0 ∧ a % b + 1 = b ∨ (a + 1) / b = a / b ∧ (a + 1) % b = a % b + 1

theorem LO.Arith.Nuon.SeriesSegment.succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {U : V} {I : V} {L : V} {A : V} (hU : (I # L) ^ 2 ≤ U) (hIL : ‖‖I‖ ^ 2‖ ≤ ‖L‖) {k : V} {n : V} (hk : k < ‖I‖ ^ 2) (H : LO.Arith.Nuon.SeriesSegment U I L A k n) : LO.Arith.Nuon.SeriesSegment U I L A (k + 1) (n + LO.Arith.fbit A k)

def LO.Arith.Nuon.polyI {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) : V

Define $I$, $L$, $U$ to satisfy the following:

1. $I$, $L$, $U$ are polynomial of $A$.
2. $(I \# L)^2 \le U$
3. $\| \| I \|^2 \| \le \|L\|$
4. $\| A \| < \|I\|^2$

Equations

• LO.Arith.Nuon.polyI A = LO.Arith.bexp (2 * A) (√‖A‖)

def LO.Arith.Nuon.polyL {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) : V

Equations

• LO.Arith.Nuon.polyL A = ‖LO.Arith.Nuon.polyI A‖ ^ 2

def LO.Arith.Nuon.polyU {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) : V

Equations

• LO.Arith.Nuon.polyU A = (2 * A + 1) ^ 128

theorem LO.Arith.Nuon.len_polyI {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} (pos : 0 < A) : ‖LO.Arith.Nuon.polyI A‖ = √‖A‖ + 1

theorem LO.Arith.Nuon.polyI_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} (pos : 0 < A) : ‖A‖ < ‖LO.Arith.Nuon.polyI A‖ ^ 2

theorem LO.Arith.Nuon.two_add_two_eq_four {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 2 + 2 = 4

theorem LO.Arith.Nuon.four_mul_eq_two_mul_two_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : 4 * a = 2 * (2 * a)

@[simp]

theorem LO.Arith.Nuon.two_mul_sqrt_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : 2 * √a ≤ a + 1

theorem LO.Arith.Nuon.four_mul_hash_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : (4 * a) # (4 * a) ≤ (a # a) ^ 16

@[simp]

theorem LO.Arith.Nuon.pos_sq_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a : V} : 0 < √a ↔ 0 < a

@[simp]

theorem LO.Arith.Nuon.pow_four_le_pow_four {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a : V} {b : V} : a ^ 4 ≤ b ^ 4 ↔ a ≤ b

theorem LO.Arith.Nuon.bexp_four_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a : V} {a' : V} {x : V} (hx : 4 * x < ‖a‖) (hx' : x < ‖a'‖) : LO.Arith.bexp a (4 * x) = LO.Arith.bexp a' x ^ 4

theorem LO.Arith.Nuon.polyI_hash_self_polybounded {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} (pos : 0 < A) : LO.Arith.Nuon.polyI A # LO.Arith.Nuon.polyI A ≤ (2 * A + 1) ^ 4

theorem LO.Arith.Nuon.polyI_hash_polyL_polybounded {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} (pos : 0 < A) : LO.Arith.Nuon.polyI A # LO.Arith.Nuon.polyL A ≤ (2 * A + 1) ^ 64

theorem LO.Arith.Nuon.sq_polyI_hash_polyL_polybounded {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} (pos : 0 < A) : (LO.Arith.Nuon.polyI A # LO.Arith.Nuon.polyL A) ^ 2 ≤ LO.Arith.Nuon.polyU A

def LO.Arith.Nuon.NuonAux {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) (k : V) (n : V) : Prop

Equations

• LO.Arith.Nuon.NuonAux A k n = LO.Arith.Nuon.SeriesSegment (LO.Arith.Nuon.polyU A) (LO.Arith.Nuon.polyI A) (LO.Arith.Nuon.polyL A) A k n

def LO.Arith.Nuon.isSegmentDef : 𝚺₀.Semisentence 5

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Arith.Nuon.isSegmentDef_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 5 → V) => LO.Arith.Nuon.IsSegment (v 0) (v 1) (v 2) (v 3) (v 4)) LO.Arith.Nuon.isSegmentDef

def LO.Arith.Nuon.segmentDef : 𝚺₀.Semisentence 7

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Arith.Nuon.segmentDef_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 7 → V) => LO.Arith.Nuon.Segment (v 0) (v 1) (v 2) (v 3) (v 4) (v 5) (v 6)) LO.Arith.Nuon.segmentDef

def LO.Arith.Nuon.isSeriesDef : 𝚺₀.Semisentence 6

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Arith.Nuon.bex_eq_le_iff {V : Type u_1} [LO.ORingStruc V] {z : V} {p : V → Prop} {b : V} : (∃ a ≤ z, a = b ∧ p a) ↔ b ≤ z ∧ p b

theorem LO.Arith.Nuon.bex_eq_lt_iff {V : Type u_1} [LO.ORingStruc V] {z : V} {p : V → Prop} {b : V} : (∃ a < z, a = b ∧ p a) ↔ b < z ∧ p b

theorem LO.Arith.Nuon.isSerieDef_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 6 → V) => LO.Arith.Nuon.IsSeries (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)) LO.Arith.Nuon.isSeriesDef

def LO.Arith.Nuon.seriesDef : 𝚺₀.Semisentence 6

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Arith.Nuon.seriesDef_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 6 → V) => LO.Arith.Nuon.Series (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)) LO.Arith.Nuon.seriesDef

def LO.Arith.Nuon.seriesSegmentDef : 𝚺₀.Semisentence 6

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Arith.Nuon.seriesSegmentDef_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin 6 → V) => LO.Arith.Nuon.SeriesSegment (v 0) (v 1) (v 2) (v 3) (v 4) (v 5)) LO.Arith.Nuon.seriesSegmentDef

def LO.Arith.Nuon.nuonAuxDef : 𝚺₀.Semisentence 3

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Arith.Nuon.nuonAux_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Relation₃ LO.Arith.Nuon.NuonAux via LO.Arith.Nuon.nuonAuxDef

instance LO.Arith.Nuon.nuonAux_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Relation₃ LO.Arith.Nuon.NuonAux

Equations

• ⋯ = ⋯

instance LO.Arith.Nuon.instBounded₃Ext_1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : LO.FirstOrder.Arith.Bounded₃ LO.Arith.Nuon.ext

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.Nuon.NuonAux.initial {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) : LO.Arith.Nuon.NuonAux A 0 0

@[simp]

theorem LO.Arith.Nuon.NuonAux.initial_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) (n : V) : LO.Arith.Nuon.NuonAux A 0 n ↔ n = 0

@[simp]

theorem LO.Arith.Nuon.NuonAux.zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (k : V) : LO.Arith.Nuon.NuonAux 0 k 0

theorem LO.Arith.Nuon.NuonAux.le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} {k : V} {n : V} (H : LO.Arith.Nuon.NuonAux A k n) : n ≤ k

theorem LO.Arith.Nuon.NuonAux.uniq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} {k : V} {n₁ : V} {n₂ : V} (H₁ : LO.Arith.Nuon.NuonAux A k n₁) (H₂ : LO.Arith.Nuon.NuonAux A k n₂) : n₁ = n₂

theorem LO.Arith.Nuon.NuonAux.succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {n : V} {A : V} {k : V} (H : LO.Arith.Nuon.NuonAux A k n) (hk : k ≤ ‖A‖) : LO.Arith.Nuon.NuonAux A (k + 1) (n + LO.Arith.fbit A k)

theorem LO.Arith.Nuon.NuonAux.exists {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} {k : V} (hk : k ≤ ‖A‖) : ∃ (n : V), LO.Arith.Nuon.NuonAux A k n

theorem LO.Arith.Nuon.NuonAux.succ_elim {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {n : V} {A : V} {k : V} (hk : k ≤ ‖A‖) (H : LO.Arith.Nuon.NuonAux A (k + 1) n) : ∃ (n' : V), n = n' + LO.Arith.fbit A k ∧ LO.Arith.Nuon.NuonAux A k n'

theorem LO.Arith.Nuon.NuonAux.succ_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {n : V} {A : V} {k : V} (hk : k ≤ ‖A‖) : LO.Arith.Nuon.NuonAux A (k + 1) (n + LO.Arith.fbit A k) ↔ LO.Arith.Nuon.NuonAux A k n

theorem LO.Arith.Nuon.NuonAux.two_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} {k : V} {n : V} (hk : k ≤ ‖A‖) : LO.Arith.Nuon.NuonAux A k n → LO.Arith.Nuon.NuonAux (2 * A) (k + 1) n

theorem LO.Arith.Nuon.NuonAux.two_mul_add_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {A : V} {k : V} {n : V} (hk : k ≤ ‖A‖) : LO.Arith.Nuon.NuonAux A k n → LO.Arith.Nuon.NuonAux (2 * A + 1) (k + 1) (n + 1)

def LO.Arith.Nuon {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) (n : V) : Prop

Equations

• LO.Arith.Nuon A n = LO.Arith.Nuon.NuonAux A ‖A‖ n

theorem LO.Arith.Nuon.exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (A : V) : ∃! n : V, LO.Arith.Nuon A n

def LO.Arith.nuon {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : V

Equations

• LO.Arith.nuon a = Classical.choose! ⋯

@[simp]

theorem LO.Arith.nuon_nuon {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : LO.Arith.Nuon a (LO.Arith.nuon a)

theorem LO.Arith.Nuon.nuon_eq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a : V} {b : V} (h : LO.Arith.Nuon a b) : LO.Arith.nuon a = b

theorem LO.Arith.Nuon.nuon_eq_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a : V} {b : V} : b = LO.Arith.nuon a ↔ LO.Arith.Nuon a b

theorem LO.Arith.nuon_bit0 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : LO.Arith.nuon (2 * a) = LO.Arith.nuon a

theorem LO.Arith.nuon_bit1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) : LO.Arith.nuon (2 * a + 1) = LO.Arith.nuon a + 1

@[simp]

theorem LO.Arith.nuon_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : LO.Arith.nuon 0 = 0

def LO.FirstOrder.Arith.nuonDef : 𝚺₀.Semisentence 2

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Arith.nuon_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Function₁ LO.Arith.nuon via LO.FirstOrder.Arith.nuonDef

@[simp]

theorem LO.Arith.eval_nuon_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.nuonDef) ↔ v 0 = LO.Arith.nuon (v 1)

instance LO.Arith.nuon_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] : 𝚺₀-Function₁ LO.Arith.nuon

Equations

• ⋯ = ⋯