Documentation

Arithmetization.OmegaOne.Basic

def LO.Arith.omegaOneAxiom :

LO.FirstOrder.SyntacticFormula ℒₒᵣ

∀ x, ∃ y, 2^{|x|^2} = y

Equations

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

Instances For

inductive LO.Arith.Theory.omegaOne :

LO.FirstOrder.Theory ℒₒᵣ

omega: 𝛀₁ LO.Arith.omegaOneAxiom

Instances For

def LO.Arith.«term𝛀₁» :

Lean.ParserDescr

Equations

LO.Arith.«term𝛀₁» = Lean.ParserDescr.node `LO.Arith.term𝛀₁ 1024 (Lean.ParserDescr.symbol "𝛀₁")

Instances For

@[simp]

theorem LO.Arith.omegaOne.mem_iff {σ : LO.FirstOrder.SyntacticFormula ℒₒᵣ} :

σ ∈ 𝛀₁ ↔ σ = LO.Arith.omegaOneAxiom

theorem LO.Arith.models_Omega₁_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] :

V ⊧ₘ LO.Arith.omegaOneAxiom ↔ ∀ (x : V), ∃ (y : V), LO.Arith.Exponential (‖x‖ ^ 2) y

theorem LO.Arith.sigma₁_omega₁ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

V ⊧ₘ LO.Arith.omegaOneAxiom

instance LO.Arith.instModelsTheoryHAddTheoryORingISigmaOfNatNatOmegaOne {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁

Equations

⋯ = ⋯

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

V ⊧ₘ* 𝐈𝚺₀

Equations

⋯ = ⋯

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

V ⊧ₘ* 𝛀₁

Equations

⋯ = ⋯

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

∃ (y : V), LO.Arith.Exponential (‖x‖ ^ 2) y

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

∃! y : V, LO.Arith.Exponential (‖x‖ ^ 2) y

theorem LO.Arith.hash_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (x : V) (y : V) :

∃! z : V, LO.Arith.Exponential (‖x‖ * ‖y‖) z

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

Equations

LO.Arith.instHash = { hash := fun (a b : V) => Classical.choose! ⋯ }

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

LO.Arith.Exponential (‖a‖ * ‖b‖) (a # b)

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

LO.Arith.Exponential ‖a‖ (a # 1)

def LO.Arith.hashDef :

𝚺₀.Semisentence 3

Equations

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

Instances For

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

𝚺₀ -Function₂ Hash.hash via LO.Arith.hashDef

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

𝚺₀ -Function₂ Hash.hash

Equations

⋯ = ⋯

@[simp]

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

LO.Arith.Pow2 (a # b)

@[simp]

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

0 < a # b

@[simp]

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

‖a‖ * ‖b‖ < a # b

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

‖a # b‖ = ‖a‖ * ‖b‖ + 1

@[simp]

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

0 # a = 1

@[simp]

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

a # 0 = 1

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

a # b = b # a

@[simp]

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

a < a # 1

@[simp]

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

a # 1 ≤ 2 * a + 1

theorem LO.Arith.lt_hash_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a : V} {b : V} {c : V} :

a < b # c ↔ ‖a‖ ≤ ‖b‖ * ‖c‖

theorem LO.Arith.hash_le_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a : V} {b : V} {c : V} :

b # c ≤ a ↔ ‖b‖ * ‖c‖ < ‖a‖

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

a < b # 1 ↔ ‖a‖ ≤ ‖b‖

theorem LO.Arith.hash_monotone {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] {a₁ : V} {a₂ : V} {b₁ : V} {b₂ : V} (h₁ : a₁ ≤ b₁) (h₂ : a₂ ≤ b₂) :

a₁ # a₂ ≤ b₁ # b₂

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

LO.Arith.bexp (a # b) (‖a‖ * ‖b‖) = a # b

theorem LO.Arith.hash_two_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀ + 𝛀₁] (a : V) {b : V} (pos : 0 < b) :

a # (2 * b) = a # b * a # 1

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

a # (2 * b) ≤ (a # b) ^ 2