Documentation

LeanPool.Incompleteness.Arithmetization.ISigmaZero.Exponential.Pow2

Pow2 #

source
def LO.Arith.Pow2 {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] (a : V) :
Prop

Imported declaration from the Incompleteness formalization.

Equations
Instances For
    source
    def LO.FirstOrder.Arith.pow2Def :
    Sg0.Semisentence 1

    Imported declaration from the Incompleteness formalization.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LO.Arith.pow2_defined {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] :
      FirstOrder.Arith.Sg0-Predicate Pow2 via FirstOrder.Arith.pow2Def
      source
      instance LO.Arith.pow2_definable {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] :
      FirstOrder.Arith.Sg0-Predicate Pow2
      source
      theorem LO.Arith.Pow2.pos {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} (h : Pow2 a) :
      0 < a
      source
      theorem LO.Arith.Pow2.dvd {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} (h : Pow2 a) {r : V} (hr : r ≀ a) :
      1 < r β†’ r ∣ a β†’ 2 ∣ r
      source
      @[simp]
      theorem LO.Arith.pow2_one {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] :
      Pow2 1
      source
      @[simp]
      theorem LO.Arith.not_pow2_zero {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] :
      Β¬Pow2 0
      source
      theorem LO.Arith.Pow2.two_dvd {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} (h : Pow2 a) (lt : 1 < a) :
      2 ∣ a
      source
      theorem LO.Arith.Pow2.two_dvd' {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} (h : Pow2 a) (lt : a β‰  1) :
      2 ∣ a
      source
      theorem LO.Arith.Pow2.of_dvd {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a b : V} (h : b ∣ a) :
      Pow2 a β†’ Pow2 b
      source
      theorem LO.Arith.pow2_mul_two {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} :
      Pow2 (2 * a) ↔ Pow2 a
      source
      theorem LO.Arith.pow2_mul_four {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} :
      Pow2 (4 * a) ↔ Pow2 a
      source
      theorem LO.Arith.Pow2.elim {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {p : V} :
      Pow2 p ↔ p = 1 ∨ βˆƒ (q : V), p = 2 * q ∧ Pow2 q
      source
      @[simp]
      theorem LO.Arith.pow2_two {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] :
      Pow2 2
      source
      theorem LO.Arith.Pow2.div_two {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {p : V} (h : Pow2 p) (ne : p β‰  1) :
      Pow2 (p / 2)
      source
      theorem LO.Arith.Pow2.two_mul_div_two {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {p : V} (h : Pow2 p) (ne : p β‰  1) :
      2 * (p / 2) = p
      source
      theorem LO.Arith.Pow2.div_two_mul_two {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {p : V} (h : Pow2 p) (ne : p β‰  1) :
      p / 2 * 2 = p
      source
      theorem LO.Arith.Pow2.elim' {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {p : V} :
      Pow2 p ↔ p = 1 ∨ 1 < p ∧ βˆƒ (q : V), p = 2 * q ∧ Pow2 q
      source
      def LO.Arith.LenBit {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] (i a : V) :
      Prop

      $\mathrm{LenBit} (2^i, a) \iff \text{$i$th-bit of $a$ is $1$}$.

      Equations
      Instances For
        source
        def LO.FirstOrder.Arith.lenbitDef :
        Sg0.Semisentence 2

        Imported declaration from the Incompleteness formalization.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem LO.Arith.lenbit_defined {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] :
          FirstOrder.Arith.Sg0-Relation LenBit via FirstOrder.Arith.lenbitDef
          source
          @[simp]
          theorem LO.Arith.lenbit_defined_iff {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] (v : Fin 2 β†’ V) :
          V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.lenbitDef) ↔ LenBit (v 0) (v 1)
          source
          instance LO.Arith.lenbit_definable {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] :
          FirstOrder.Arith.Sg0-Relation LenBit
          source
          theorem LO.Arith.LenBit.le {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i a : V} (h : LenBit i a) :
          i ≀ a
          source
          theorem LO.Arith.not_lenbit_of_lt {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i a : V} (h : a < i) :
          Β¬LenBit i a
          source
          @[simp]
          theorem LO.Arith.LenBit.zero {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] (a : V) :
          Β¬LenBit 0 a
          source
          @[simp]
          theorem LO.Arith.LenBit.on_zero {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] (a : V) :
          Β¬LenBit a 0
          source
          theorem LO.Arith.LenBit.one {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] (a : V) :
          LenBit 1 a ↔ Β¬2 ∣ a
          source
          theorem LO.Arith.LenBit.iff_rem {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i a : V} :
          LenBit i a ↔ a / i % 2 = 1
          source
          theorem LO.Arith.not_lenbit_iff_rem {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i a : V} :
          Β¬LenBit i a ↔ a / i % 2 = 0
          source
          @[simp]
          theorem LO.Arith.LenBit.self {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a : V} (pos : 0 < a) :
          LenBit a a
          source
          theorem LO.Arith.LenBit.mod {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i a k : V} (h : 2 * i ∣ k) :
          LenBit i (a % k) ↔ LenBit i a
          source
          @[simp]
          theorem LO.Arith.LenBit.mod_two_mul_self {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a i : V} :
          LenBit i (a % (2 * i)) ↔ LenBit i a
          source
          theorem LO.Arith.LenBit.add {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i a b : V} (h : 2 * i ∣ b) :
          LenBit i (a + b) ↔ LenBit i a
          source
          theorem LO.Arith.LenBit.add_self {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {i a : V} (h : a < i) :
          LenBit i (a + i)
          source
          theorem LO.Arith.LenBit.add_self_of_not_lenbit {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a i : V} (pos : 0 < i) (h : Β¬LenBit i a) :
          LenBit i (a + i)
          source
          theorem LO.Arith.LenBit.add_self_of_lenbit {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a i : V} (pos : 0 < i) (h : LenBit i a) :
          Β¬LenBit i (a + i)
          source
          theorem LO.Arith.LenBit.sub_self_of_lenbit {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈open] {a i : V} (pos : 0 < i) (h : LenBit i a) :
          Β¬LenBit i (a - i)
          source
          theorem LO.Arith.Pow2.mul {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a b : V} (ha : Pow2 a) (hb : Pow2 b) :
          Pow2 (a * b)
          source
          @[simp]
          theorem LO.Arith.Pow2.mul_iff {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a b : V} :
          Pow2 (a * b) ↔ Pow2 a ∧ Pow2 b
          source
          @[simp]
          theorem LO.Arith.Pow2.sq_iff {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a : V} :
          Pow2 (a ^ 2) ↔ Pow2 a
          source
          theorem LO.Arith.Pow2.sq {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a : V} :
          Pow2 a β†’ Pow2 (a ^ 2)
          source
          theorem LO.Arith.Pow2.dvd_of_le {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a b : V} (ha : Pow2 a) (hb : Pow2 b) :
          a ≀ b β†’ a ∣ b
          source
          theorem LO.Arith.Pow2.le_iff_dvd {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a b : V} (ha : Pow2 a) (hb : Pow2 b) :
          a ≀ b ↔ a ∣ b
          source
          theorem LO.Arith.Pow2.two_le {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a : V} (pa : Pow2 a) (ne1 : a β‰  1) :
          2 ≀ a
          source
          theorem LO.Arith.Pow2.le_iff_lt_two {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a b : V} (ha : Pow2 a) (hb : Pow2 b) :
          a ≀ b ↔ a < 2 * b
          source
          theorem LO.Arith.Pow2.lt_iff_two_mul_le {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a b : V} (ha : Pow2 a) (hb : Pow2 b) :
          a < b ↔ 2 * a ≀ b
          source
          theorem LO.Arith.Pow2.sq_or_dsq {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a : V} (pa : Pow2 a) :
          βˆƒ (b : V), a = b ^ 2 ∨ a = 2 * b ^ 2
          source
          theorem LO.Arith.Pow2.sqrt {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a : V} (h : Pow2 a) (hsq : (√a) ^ 2 = a) :
          Pow2 (√a)
          source
          @[simp]
          theorem LO.Arith.Pow2.not_three {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] :
          Β¬Pow2 3
          source
          theorem LO.Arith.Pow2.four_le {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {i : V} (hi : Pow2 i) (lt : 2 < i) :
          4 ≀ i
          source
          theorem LO.Arith.Pow2.mul_add_lt_of_mul_lt_of_pos {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a b p q : V} (hp : Pow2 p) (hq : Pow2 q) (h : a * p < q) (hb : b < p) (hbq : b < q) :
          a * p + b < q
          source
          theorem LO.Arith.LenBit.mod_pow2 {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a i j : V} (pi : Pow2 i) (pj : Pow2 j) (h : i < j) :
          LenBit i (a % j) ↔ LenBit i a
          source
          theorem LO.Arith.LenBit.add_pow2 {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a i j : V} (pi : Pow2 i) (pj : Pow2 j) (h : i < j) :
          LenBit i (a + j) ↔ LenBit i a
          source
          theorem LO.Arith.LenBit.add_pow2_iff_of_lt {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a i j : V} (pi : Pow2 i) (pj : Pow2 j) (h : a < j) :
          LenBit i (a + j) ↔ i = j ∨ LenBit i a
          source
          theorem LO.Arith.lenbit_iff_add_mul {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {i a : V} (hi : Pow2 i) :
          LenBit i a ↔ βˆƒ (k : V), βˆƒ r < i, a = k * (2 * i) + i + r
          source
          theorem LO.Arith.not_lenbit_iff_add_mul {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {i a : V} (hi : Pow2 i) :
          Β¬LenBit i a ↔ βˆƒ (k : V), βˆƒ r < i, a = k * (2 * i) + r
          source
          theorem LO.Arith.lenbit_mul_add {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {i j a r : V} (pi : Pow2 i) (pj : Pow2 j) (hr : r < j) :
          LenBit (i * j) (a * j + r) ↔ LenBit i a
          source
          theorem LO.Arith.lenbit_add_pow2_iff_of_not_lenbit {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a i j : V} (pi : Pow2 i) (pj : Pow2 j) (h : Β¬LenBit j a) :
          LenBit i (a + j) ↔ i = j ∨ LenBit i a
          source
          theorem LO.Arith.lenbit_sub_pow2_iff_of_lenbit {V : Type u_1} [ORingStruc V] [V βŠ§β‚˜* 𝐈Sg0] {a i j : V} (pi : Pow2 i) (pj : Pow2 j) (h : LenBit j a) :
          LenBit i (a - j) ↔ i β‰  j ∧ LenBit i a