Documentation

Arithmetization.ISigmaOne.Bit

def LO.Arith.Bit {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) (a : V) :
Equations
Instances For
    Equations
    • LO.Arith.instMembership_arithmetization = { mem := LO.Arith.Bit }
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      instance LO.Arith.mem_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :
      𝚺₀-Relation fun (x x_1 : V) => x x_1
      Equations
      • =
      instance LO.Arith.mem_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) :
      -Relation fun (x x_1 : V) => x x_1
      Equations
      • =
      theorem LO.Arith.mem_absolute {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (i : ) (a : ) :
      i a i a
      theorem LO.Arith.mem_iff_bit {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} :
      theorem LO.Arith.exp_le_of_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i a) :
      exp i a
      theorem LO.Arith.lt_of_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i a) :
      i < a
      theorem LO.Arith.not_mem_of_lt_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : a < exp i) :
      ia
      theorem LO.Arith.HierarchySymbol.Boldface.ball_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } (Γ : LO.SigmaPiDelta) (m : ) {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
      { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => xf v, P v x
      theorem LO.Arith.HierarchySymbol.Boldface.bex_mem {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } (Γ : LO.SigmaPiDelta) (m : ) {P : (Fin kV)VProp} {f : (Fin kV)V} (hf : { Γ := 𝚺, rank := m + 1 }.BoldfaceFunction f) (h : { Γ := Γ, rank := m + 1 }.Boldface fun (w : Fin k.succV) => P (fun (x : Fin k) => w x.succ) (w 0)) :
      { Γ := Γ, rank := m + 1 }.Boldface fun (v : Fin kV) => xf v, P v x
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem LO.FirstOrder.Arith.eval_memRel {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {r : V} :
                          LO.FirstOrder.Arith.memRelOpr.val ![r, x, y] x, y r
                          @[simp]
                          theorem LO.FirstOrder.Arith.eval_memRel₃ {V : Type u_2} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {x : V} {y : V} {z : V} {r : V} :
                          LO.FirstOrder.Arith.memRel₃Opr.val ![r, x, y, z] x, y, z r
                          theorem LO.Arith.mem_iff_mul_exp_add_exp_add {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} :
                          i a ∃ (k : V), r < exp i, a = k * exp (i + 1) + exp i + r
                          theorem LO.Arith.not_mem_iff_mul_exp_add {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} :
                          ia ∃ (k : V), r < exp i, a = k * exp (i + 1) + r
                          Equations
                          • LO.Arith.instEmptyCollection_arithmetization = { emptyCollection := 0 }
                          Instances For
                            theorem LO.Arith.emptyset_def {V : Type u_1} [Zero V] :
                            = 0
                            @[simp]
                            theorem LO.Arith.not_mem_empty {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) :
                            i
                            @[simp]
                            theorem LO.Arith.not_mem_zero {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) :
                            i0
                            Equations
                            • LO.Arith.instSingleton_arithmetization = { singleton := fun (a : V) => exp a }
                            Instances For
                              theorem LO.Arith.singleton_def {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
                              {a} = exp a
                              noncomputable def LO.Arith.bitInsert {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) (a : V) :
                              V
                              Equations
                              Instances For
                                noncomputable def LO.Arith.bitRemove {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) (a : V) :
                                V
                                Equations
                                Instances For
                                  def LO.Arith.instInsert_arithmetization {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :
                                  Insert V V
                                  Equations
                                  • LO.Arith.instInsert_arithmetization = { insert := LO.Arith.bitInsert }
                                  Instances For
                                    theorem LO.Arith.insert_eq {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} :
                                    theorem LO.Arith.singleton_eq_insert {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) :
                                    {i} = insert i
                                    Equations
                                    • =
                                    @[simp]
                                    theorem LO.Arith.mem_bitInsert_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} {a : V} :
                                    i insert j a i = j i a
                                    @[simp]
                                    theorem LO.Arith.mem_bitRemove_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} {a : V} :
                                    @[simp]
                                    theorem LO.Arith.not_mem_bitRemove_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) (a : V) :
                                    theorem LO.Arith.insert_graph {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (b : V) (i : V) (a : V) :
                                    b = insert i a i a b = a ia eb, e = exp i b = a + e
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      instance LO.Arith.insert_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :
                                      Equations
                                      • =
                                      Equations
                                      • =
                                      theorem LO.Arith.insert_le_of_le_of_le {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} {a : V} {b : V} (hij : i j) (hab : a b) :
                                      insert i a b + exp j
                                      theorem LO.Arith.one_eq_singleton {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :
                                      1 = {}
                                      @[simp]
                                      theorem LO.Arith.mem_singleton_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} :
                                      i {j} i = j
                                      theorem LO.Arith.bitRemove_lt_of_mem {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i a) :
                                      theorem LO.Arith.pos_of_nonempty {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i a) :
                                      0 < a
                                      @[simp]
                                      theorem LO.Arith.mem_insert {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) (a : V) :
                                      i insert i a
                                      theorem LO.Arith.insert_eq_self_of_mem {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i a) :
                                      insert i a = a
                                      theorem LO.Arith.log_mem_of_pos {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} (h : 0 < a) :
                                      theorem LO.Arith.le_log_of_mem {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i a) :
                                      theorem LO.Arith.succ_mem_iff_mem_div_two {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} :
                                      i + 1 a i a / 2
                                      theorem LO.Arith.lt_length_of_mem {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i a) :
                                      theorem LO.Arith.lt_exp_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {i : V} :
                                      a < exp i ja, j < i
                                      Equations
                                      • LO.Arith.instHasSubset_arithmetization = { Subset := fun (a b : V) => ∀ ⦃i : V⦄, i ai b }
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        instance LO.Arith.bitSubset_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :
                                        𝚺₀-Relation fun (x x_1 : V) => x x_1
                                        Equations
                                        • =
                                        @[simp]
                                        instance LO.Arith.bitSubset_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) :
                                        -Relation fun (x x_1 : V) => x x_1
                                        Equations
                                        • =
                                        theorem LO.Arith.subset_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} :
                                        a b xa, x b
                                        @[simp]
                                        theorem LO.Arith.subset_refl {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
                                        a a
                                        theorem LO.Arith.subset_trans {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} {c : V} (hab : a b) (hbc : b c) :
                                        a c
                                        theorem LO.Arith.mem_exp_add_succ_sub_one {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) (j : V) :
                                        i exp (i + j + 1) - 1
                                        def LO.Arith.under {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
                                        V

                                        under a = {0, 1, 2, ..., a - 1}

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem LO.Arith.le_under {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
                                          @[simp]
                                          theorem LO.Arith.mem_under_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} :
                                          @[simp]
                                          theorem LO.Arith.not_mem_under_self {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) :
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            instance LO.Arith.under_definable {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :
                                            𝚺₀-Function₁ LO.Arith.under
                                            Equations
                                            • =
                                            instance LO.Arith.under_definable' {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (Γ : LO.FirstOrder.Arith.HierarchySymbol) :
                                            Γ-Function₁ LO.Arith.under
                                            Equations
                                            • =
                                            theorem LO.Arith.eq_zero_of_subset_zero {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} :
                                            a 0a = 0
                                            theorem LO.Arith.subset_div_two {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} :
                                            a ba / 2 b / 2
                                            theorem LO.Arith.zero_mem_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} :
                                            0a 2 a
                                            @[simp]
                                            theorem LO.Arith.zero_not_mem {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
                                            02 * a
                                            @[simp]
                                            theorem LO.Arith.zero_mem_double_add_one {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
                                            0 2 * a + 1
                                            @[simp]
                                            theorem LO.Arith.succ_mem_two_mul_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} :
                                            i + 1 2 * a i a
                                            @[simp]
                                            theorem LO.Arith.succ_mem_two_mul_succ_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} :
                                            i + 1 2 * a + 1 i a
                                            theorem LO.Arith.le_of_subset {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (h : a b) :
                                            a b
                                            theorem LO.Arith.mem_ext {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (h : ∀ (i : V), i a i b) :
                                            a = b
                                            theorem LO.Arith.pos_iff_nonempty {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} :
                                            0 < s s
                                            theorem LO.Arith.nonempty_of_pos {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} (h : 0 < a) :
                                            ∃ (i : V), i a
                                            theorem LO.Arith.eq_empty_or_nonempty {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) :
                                            a = ∃ (i : V), i a
                                            theorem LO.Arith.nonempty_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} :
                                            s ∃ (x : V), x s
                                            theorem LO.Arith.isempty_iff {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {s : V} :
                                            s = ∀ (x : V), xs
                                            @[simp]
                                            theorem LO.Arith.empty_subset {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) :
                                            theorem LO.Arith.lt_of_lt_log {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (pos : 0 < b) (h : ia, i < LO.Arith.log b) :
                                            a < b
                                            @[simp]
                                            theorem LO.Arith.under_inj {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {j : V} :
                                            @[simp]
                                            theorem LO.Arith.under_zero {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] :
                                            @[simp]
                                            theorem LO.Arith.under_succ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] (i : V) :
                                            theorem LO.Arith.insert_remove {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (h : i a) :
                                            theorem LO.Arith.finset_comprehension {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] {m : } [Fact (1 m)] [V ⊧ₘ* 𝐈𝐍𝐃𝚺 m] {Γ : LO.SigmaPiDelta} {P : VProp} (hP : { Γ := Γ, rank := m }-Predicate P) (a : V) :
                                            s < exp a, i < a, i s P i
                                            theorem LO.Arith.finset_comprehension_exists_unique {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] {m : } [Fact (1 m)] [V ⊧ₘ* 𝐈𝐍𝐃𝚺 m] {Γ : LO.SigmaPiDelta} {P : VProp} (hP : { Γ := Γ, rank := m }-Predicate P) (a : V) :
                                            ∃! s : V, s < exp a i < a, i s P i
                                            theorem LO.Arith.finset_comprehension₁ {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {P : VProp} (hP : { Γ := Γ, rank := 1 }-Predicate P) (a : V) :
                                            s < exp a, i < a, i s P i
                                            theorem LO.Arith.finset_comprehension₁! {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {P : VProp} (hP : { Γ := Γ, rank := 1 }-Predicate P) (a : V) :
                                            ∃! s : V, s < exp a i < a, i s P i
                                            theorem LO.Arith.finite_comprehension₁! {V : Type u_1} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {P : VProp} (hP : { Γ := Γ, rank := 1 }-Predicate P) (fin : ∃ (m : V), ∀ (i : V), P ii < m) :
                                            ∃! s : V, ∀ (i : V), i s P i