Concrete Binary Tower Core

Core definitions for the concrete bitvector model of the binary tower.

def ConcreteBinaryTower.ConcreteBTField : ℕ → Type

theorem ConcreteBinaryTower.cast_ConcreteBTField_eq (k m : ℕ) (h_eq : k = m) : ConcreteBTField k = ConcreteBTField m

@[implicit_reducible]

instance ConcreteBinaryTower.BitVec.instDCast : DCast ℕ BitVec

theorem ConcreteBinaryTower.BitVec.bitvec_cast_eq_dcast {n m : ℕ} (h : n = m) (bv : BitVec n) : BitVec.cast h bv = dcast h bv

theorem ConcreteBinaryTower.BitVec.dcast_id {n : ℕ} (bv : BitVec n) : dcast ⋯ bv = bv

theorem ConcreteBinaryTower.BitVec.dcast_bitvec_eq {l r val : ℕ} (h_width_eq : l = r) : dcast h_width_eq (BitVec.ofNat l val) = BitVec.ofNat r val

@[simp]

theorem ConcreteBinaryTower.BitVec.cast_zero {n m : ℕ} (h : n = m) : BitVec.cast h 0 = 0

@[simp]

theorem ConcreteBinaryTower.BitVec.cast_one {n m : ℕ} (h : n = m) : BitVec.cast h 1 = 1#m

@[simp]

theorem ConcreteBinaryTower.BitVec.dcast_zero {n m : ℕ} (h : n = m) : dcast h 0#n = 0#m

@[simp]

theorem ConcreteBinaryTower.BitVec.dcast_one {n m : ℕ} (h : n = m) : dcast h 1#n = 1#m

theorem ConcreteBinaryTower.BitVec.dcast_bitvec_toNat_eq {w w2 : ℕ} (x : BitVec w) (h_width_eq : w = w2) : x.toNat = (dcast h_width_eq x).toNat

theorem ConcreteBinaryTower.BitVec.dcast_bitvec_eq_zero {l r : ℕ} (h_width_eq : l = r) : dcast h_width_eq 0#l = 0#r

theorem ConcreteBinaryTower.BitVec.dcast_bitvec_extractLsb_eq {w hi1 lo1 hi2 lo2 : ℕ} (x : BitVec w) (h_lo_eq : lo1 = lo2) (h_width_eq : hi1 - lo1 + 1 = hi2 - lo2 + 1) : dcast h_width_eq (BitVec.extractLsb hi1 lo1 x) = BitVec.extractLsb hi2 lo2 x

theorem ConcreteBinaryTower.BitVec.dcast_dcast_bitvec_extractLsb_eq {w hi lo : ℕ} (x : BitVec w) (h_width_eq : w = hi - lo + 1) : dcast h_width_eq (dcast ⋯ (BitVec.extractLsb hi lo x)) = BitVec.extractLsb hi lo x

theorem ConcreteBinaryTower.BitVec.eq_mp_eq_dcast {w w2 : ℕ} (x : BitVec w) (h_width_eq : w = w2) (h_bitvec_eq : BitVec w = BitVec w2 := by rw [h_width_eq]) : h_bitvec_eq.mp x = dcast h_width_eq x

theorem ConcreteBinaryTower.BitVec.extractLsb_concat_hi {hi_size lo_size : ℕ} (hi : BitVec hi_size) (lo : BitVec lo_size) (h_hi : hi_size > 0) : BitVec.extractLsb (hi_size + lo_size - 1) lo_size (hi.append lo) = dcast ⋯ hi

theorem ConcreteBinaryTower.BitVec.extractLsb_concat_lo {hi_size lo_size : ℕ} (hi : BitVec hi_size) (lo : BitVec lo_size) (h_lo : lo_size > 0) : BitVec.extractLsb (lo_size - 1) 0 (hi.append lo) = dcast ⋯ lo

theorem ConcreteBinaryTower.Nat.shiftRight_eq_sub_mod_then_div_two_pow {n lo_len : ℕ} : n >>> lo_len = (n - n % 2 ^ lo_len) / 2 ^ lo_len

theorem ConcreteBinaryTower.Nat.shiftRight_lo_mod_2_pow_hi_shiftLeft_lo (n hi_len lo_len : ℕ) (h_n : n < 2 ^ (hi_len + lo_len)) : (n >>> lo_len % 2 ^ hi_len) <<< lo_len = n - n % 2 ^ lo_len

theorem ConcreteBinaryTower.Nat.reconstruct_from_hi_and_lo_parts (n hi_len lo_len : ℕ) (h_n : n < 2 ^ (hi_len + lo_len)) : n = (n >>> lo_len % 2 ^ hi_len) <<< lo_len + n % 2 ^ lo_len

theorem ConcreteBinaryTower.Nat.reconstruct_from_hi_and_lo_parts_or_ver (n hi_len lo_len : ℕ) (h_n : n < 2 ^ (hi_len + lo_len)) : n = (n >>> lo_len % 2 ^ hi_len) <<< lo_len ||| n % 2 ^ lo_len

theorem ConcreteBinaryTower.BitVec.eq_append_iff_extract {lo_size hi_size : ℕ} (lo : BitVec lo_size) (hi : BitVec hi_size) (h_hi_gt_0 : hi_size > 0) (h_lo_gt_0 : lo_size > 0) (x : BitVec (hi_size + lo_size)) : x = dcast ⋯ (hi.append lo) ↔ hi = dcast ⋯ (BitVec.extractLsb (hi_size + lo_size - 1) lo_size x) ∧ lo = dcast ⋯ (BitVec.extractLsb (lo_size - 1) 0 x)

def ConcreteBinaryTower.bitVecToString (width : ℕ) (bv : BitVec width) : String

def ConcreteBinaryTower.ConcreteBTField.toBitString {k : ℕ} (bv : ConcreteBTField k) : String

def ConcreteBinaryTower.width (k : ℕ) : ℕ

def ConcreteBinaryTower.fromNat {k : ℕ} (n : ℕ) : ConcreteBTField k

@[simp]

theorem ConcreteBinaryTower.fromNat_toNat_eq_self {k : ℕ} (bv : BitVec (2 ^ k)) : fromNat bv.toNat = bv

@[implicit_reducible]

instance ConcreteBinaryTower.ConcreteBTField.instDCast_local : DCast ℕ ConcreteBTField

theorem ConcreteBinaryTower.one_le_sub_middle_of_pow2 {k : ℕ} (h_k : 1 ≤ k) : 1 ≤ 2 ^ k - 2 ^ (k - 1)

theorem ConcreteBinaryTower.sub_middle_of_pow2_with_one_canceled {k : ℕ} (h_k : 1 ≤ k) : 2 ^ k - 1 - 2 ^ (k - 1) + 1 = 2 ^ (k - 1)

theorem ConcreteBinaryTower.h_sub_middle {k : ℕ} (h_pos : k > 0) : 2 ^ k - 1 - 2 ^ (k - 1) + 1 = 2 ^ (k - 1)

theorem ConcreteBinaryTower.h_middle_sub {k : ℕ} : 2 ^ (k - 1) - 1 - 0 + 1 = 2 ^ (k - 1)

theorem ConcreteBinaryTower.h_sum_two_same_pow2 {k : ℕ} (h_pos : k > 0) : 2 ^ (k - 1) + 2 ^ (k - 1) = 2 ^ k

def ConcreteBinaryTower.zero {k : ℕ} : ConcreteBTField k

def ConcreteBinaryTower.one {k : ℕ} : ConcreteBTField k

@[implicit_reducible]

instance ConcreteBinaryTower.instZeroConcreteBTField (k : ℕ) : Zero (ConcreteBTField k)

@[implicit_reducible]

instance ConcreteBinaryTower.instOneConcreteBTField (k : ℕ) : One (ConcreteBTField k)

def ConcreteBinaryTower.add {k : ℕ} (x y : ConcreteBTField k) : ConcreteBTField k

def ConcreteBinaryTower.neg {k : ℕ} (x : ConcreteBTField k) : ConcreteBTField k

@[implicit_reducible]

instance ConcreteBinaryTower.instHAddConcreteBTField (k : ℕ) : HAdd (ConcreteBTField k) (ConcreteBTField k) (ConcreteBTField k)

@[implicit_reducible]

instance ConcreteBinaryTower.instAddConcreteBTField (k : ℕ) : Add (ConcreteBTField k)

theorem ConcreteBinaryTower.sum_fromNat_eq_from_xor_Nat {k : ℕ} (x y : ℕ) : fromNat (x ^^^ y) = fromNat x + fromNat y

theorem ConcreteBinaryTower.add_self_cancel {k : ℕ} (a : ConcreteBTField k) : a + a = 0

theorem ConcreteBinaryTower.add_eq_zero_iff_eq {k : ℕ} (a b : ConcreteBTField k) : a + b = 0 ↔ a = b

theorem ConcreteBinaryTower.add_assoc {k : ℕ} (a b c : ConcreteBTField k) : a + b + c = a + (b + c)

theorem ConcreteBinaryTower.add_comm {k : ℕ} (a b : ConcreteBTField k) : a + b = b + a

theorem ConcreteBinaryTower.zero_add {k : ℕ} (a : ConcreteBTField k) : 0 + a = a

theorem ConcreteBinaryTower.add_zero {k : ℕ} (a : ConcreteBTField k) : a + 0 = a

theorem ConcreteBinaryTower.neg_add_cancel {k : ℕ} (a : ConcreteBTField k) : neg a + a = 0

theorem ConcreteBinaryTower.if_self_rfl {α : Type u_1} [DecidableEq α] (a b : α) : (if a = b then b else a) = a

@[implicit_reducible]

noncomputable instance ConcreteBinaryTower.instDecidableEqGaloisFieldOfNatNat_compPoly : DecidableEq (GF(2))

@[implicit_reducible]

instance ConcreteBinaryTower.instDecidableEqConcreteBTField (k : ℕ) : DecidableEq (ConcreteBTField k)

noncomputable def ConcreteBinaryTower.toConcreteBTF0 : GF(2) → ConcreteBTField 0

noncomputable def ConcreteBinaryTower.fromConcreteBTF0 : ConcreteBTField 0 → (GF(2))

theorem ConcreteBinaryTower.nsmul_succ {k : ℕ} (n : ℕ) (x : ConcreteBTField k) : (if n.succ % 2 = 0 then zero else x) = (if n % 2 = 0 then zero else x) + x

theorem ConcreteBinaryTower.zsmul_succ {k : ℕ} (n : ℕ) (x : ConcreteBTField k) : (if ↑n.succ % 2 = 0 then zero else x) = (if ↑n % 2 = 0 then zero else x) + x

theorem ConcreteBinaryTower.neg_mod_2_eq_0_iff_mod_2_eq_0 {n : ℤ} : -n % 2 = 0 ↔ n % 2 = 0

theorem ConcreteBinaryTower.zsmul_neg' {k : ℕ} (n : ℕ) (a : ConcreteBTField k) : (if Int.negSucc n % 2 = 0 then zero else a) = neg (if ↑n.succ % 2 = 0 then zero else a)

def ConcreteBinaryTower.split {k : ℕ} (h : k > 0) (x : ConcreteBTField k) : ConcreteBTField (k - 1) × ConcreteBTField (k - 1)

def ConcreteBinaryTower.join {k : ℕ} (h_pos : k > 0) (hi lo : ConcreteBTField (k - 1)) : ConcreteBTField k

def ConcreteBinaryTower.«term《_,_》» : Lean.ParserDescr

theorem ConcreteBinaryTower.cast_join {k n : ℕ} (h_pos : k > 0) (hi lo : ConcreteBTField (k - 1)) (heq : k = n) : join h_pos hi lo = cast ⋯ (join ⋯ (cast ⋯ hi) (cast ⋯ lo))

structure ConcreteBinaryTower.ConcreteBTFAddCommGroupProps (k : ℕ) : Prop

• add_assoc (a b c : ConcreteBTField k) : a + b + c = a + (b + c)
• add_comm (a b : ConcreteBTField k) : a + b = b + a
• add_zero (a : ConcreteBTField k) : a + zero = a
• zero_add (a : ConcreteBTField k) : zero + a = a
• add_neg (a : ConcreteBTField k) : a + neg a = zero

theorem ConcreteBinaryTower.zero_is_0 {k : ℕ} : zero = 0

theorem ConcreteBinaryTower.one_is_1 {k : ℕ} : one = 1

theorem ConcreteBinaryTower.concrete_one_ne_zero {k : ℕ} : one ≠ zero

instance ConcreteBinaryTower.instNeZeroConcreteBTFieldOfNat {k : ℕ} : NeZero 1

@[reducible]

def ConcreteBinaryTower.mkAddCommGroupInstance {k : ℕ} : AddCommGroup (ConcreteBTField k)

@[implicit_reducible]

instance ConcreteBinaryTower.instAddCommGroupConcreteBTField (k : ℕ) : AddCommGroup (ConcreteBTField k)

theorem ConcreteBinaryTower.BitVec.extractLsb_eq_shift_ofNat {n : ℕ} (x : BitVec n) (l r : ℕ) : BitVec.extractLsb r l x = BitVec.ofNat (r - l + 1) (x.toNat >>> l)

theorem ConcreteBinaryTower.setWidth_eq_ofNat_mod {n num_bits : ℕ} (x : BitVec n) : BitVec.setWidth num_bits x = BitVec.ofNat num_bits (x.toNat % 2 ^ num_bits)

theorem ConcreteBinaryTower.BitVec.extractLsb_eq_and_pow_2_minus_1_ofNat {n num_bits : ℕ} (h_num_bits : num_bits > 0) (x : BitVec n) : BitVec.extractLsb (num_bits - 1) 0 x = BitVec.ofNat (num_bits - 1 - 0 + 1) (x.toNat &&& 2 ^ num_bits - 1)

theorem ConcreteBinaryTower.split_bitvec_eq_iff_fromNat {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField k) (hi_btf lo_btf : ConcreteBTField (k - 1)) : split h_pos x = (hi_btf, lo_btf) ↔ hi_btf = fromNat (BitVec.toNat x >>> 2 ^ (k - 1)) ∧ lo_btf = fromNat (BitVec.toNat x &&& 2 ^ 2 ^ (k - 1) - 1)

theorem ConcreteBinaryTower.BitVec.extractLsb_dcast_eq {w w2 hi lo : ℕ} (x : BitVec w) (h : w = w2) : BitVec.extractLsb hi lo (dcast h x) = BitVec.extractLsb hi lo x

theorem ConcreteBinaryTower.join_eq_dcast_append {k : ℕ} (h_pos : k > 0) (hi lo : ConcreteBTField (k - 1)) : join h_pos hi lo = dcast ⋯ (BitVec.append hi lo)

theorem ConcreteBinaryTower.eq_join_iff_dcast_eq_append {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField k) (hi lo : ConcreteBTField (k - 1)) : x = join h_pos hi lo ↔ dcast ⋯ x = BitVec.append hi lo

theorem ConcreteBinaryTower.join_eq_iff_dcast_extractLsb {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField k) (hi_btf lo_btf : ConcreteBTField (k - 1)) : x = join h_pos hi_btf lo_btf ↔ hi_btf = dcast ⋯ (BitVec.extractLsb (2 ^ k - 1) (2 ^ (k - 1)) x) ∧ lo_btf = dcast ⋯ (BitVec.extractLsb (2 ^ (k - 1) - 1) 0 x)

theorem ConcreteBinaryTower.join_eq_join_iff {k : ℕ} (h_pos : k > 0) (hi₀ lo₀ hi₁ lo₁ : ConcreteBTField (k - 1)) : join h_pos hi₀ lo₀ = join h_pos hi₁ lo₁ ↔ hi₀ = hi₁ ∧ lo₀ = lo₁

theorem ConcreteBinaryTower.join_eq_bitvec_iff_fromNat {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField k) (hi_btf lo_btf : ConcreteBTField (k - 1)) : x = join h_pos hi_btf lo_btf ↔ hi_btf = fromNat (BitVec.toNat x >>> 2 ^ (k - 1)) ∧ lo_btf = fromNat (BitVec.toNat x &&& 2 ^ 2 ^ (k - 1) - 1)

theorem ConcreteBinaryTower.join_of_split {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField k) (hi_btf lo_btf : ConcreteBTField (k - 1)) (h_split_eq : split h_pos x = (hi_btf, lo_btf)) : x = join h_pos hi_btf lo_btf

theorem ConcreteBinaryTower.split_of_join {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField k) (hi_btf lo_btf : ConcreteBTField (k - 1)) (h_join : x = join h_pos hi_btf lo_btf) : (hi_btf, lo_btf) = split h_pos x

theorem ConcreteBinaryTower.split_join_eq_split {k : ℕ} (h_pos : k > 0) (hi_btf lo_btf : ConcreteBTField (k - 1)) : split h_pos (join h_pos hi_btf lo_btf) = (hi_btf, lo_btf)

theorem ConcreteBinaryTower.join_split_eq_join {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField k) : join h_pos (split h_pos x).1 (split h_pos x).2 = x

theorem ConcreteBinaryTower.eq_iff_split_eq {k : ℕ} (h_pos : k > 0) (x₀ x₁ : ConcreteBTField k) : x₀ = x₁ ↔ split h_pos x₀ = split h_pos x₁

theorem ConcreteBinaryTower.split_sum_eq_sum_split {k : ℕ} (h_pos : k > 0) (x₀ x₁ : ConcreteBTField k) (hi₀ lo₀ hi₁ lo₁ : ConcreteBTField (k - 1)) (h_split_x₀ : split h_pos x₀ = (hi₀, lo₀)) (h_split_x₁ : split h_pos x₁ = (hi₁, lo₁)) : split h_pos (x₀ + x₁) = (hi₀ + hi₁, lo₀ + lo₁)

theorem ConcreteBinaryTower.join_add_join {k : ℕ} (h_pos : k > 0) (hi₀ lo₀ hi₁ lo₁ : ConcreteBTField (k - 1)) : join h_pos hi₀ lo₀ + join h_pos hi₁ lo₁ = join h_pos (hi₀ + hi₁) (lo₀ + lo₁)

theorem ConcreteBinaryTower.split_zero {k : ℕ} (h_pos : k > 0) : split h_pos zero = (zero, zero)

def ConcreteBinaryTower.Z (k : ℕ) : ConcreteBTField k

theorem ConcreteBinaryTower.split_Z {k : ℕ} (h_pos : k > 0) : split h_pos (Z k) = (one, zero)

theorem ConcreteBinaryTower.one_bitvec_toNat {width : ℕ} (h_width : width > 0) : (1#width).toNat = 1

theorem ConcreteBinaryTower.one_bitvec_shiftRight {d : ℕ} (h_d : d > 0) : 1 >>> d = 0

theorem ConcreteBinaryTower.split_one {k : ℕ} (h_k : k > 0) : split h_k one = (zero, one)

theorem ConcreteBinaryTower.join_zero_zero {k : ℕ} (h_k : k > 0) : join h_k zero zero = zero

theorem ConcreteBinaryTower.join_zero_one {k : ℕ} (h_k : k > 0) : join h_k zero one = one

def ConcreteBinaryTower.equivProd {k : ℕ} (h_k_pos : k > 0) : ConcreteBTField k ≃ ConcreteBTField (k - 1) × ConcreteBTField (k - 1)

theorem ConcreteBinaryTower.Z_ne_zero {k : ℕ} : Z k ≠ zero

instance ConcreteBinaryTower.Z_NeZero {k : ℕ} : NeZero (Z k)

theorem ConcreteBinaryTower.mul_trans_inequality {k : ℕ} (x : ℕ) (h_k : k ≤ 2) (h_x : x ≤ 2 ^ 2 ^ k - 1) : x < 16

def ConcreteBinaryTower.coeffsToBitVec {n : ℕ} (coeffs : List (ZMod 2)) : BitVec n

@[irreducible]

def ConcreteBinaryTower.concrete_mul {k : ℕ} (a b : ConcreteBTField k) : ConcreteBTField k

@[implicit_reducible]

instance ConcreteBinaryTower.instHMulConcreteBTField (k : ℕ) : HMul (ConcreteBTField k) (ConcreteBTField k) (ConcreteBTField k)

@[irreducible]

def ConcreteBinaryTower.concrete_inv {k : ℕ} (a : ConcreteBTField k) : ConcreteBTField k

@[irreducible]

def ConcreteBinaryTower.concrete_pow_nat {k : ℕ} (x : ConcreteBTField k) (n : ℕ) : ConcreteBTField k

theorem ConcreteBinaryTower.cast_mul (m n : ℕ) {x y : ConcreteBTField m} (h_eq : m = n) : cast ⋯ (x * y) = cast ⋯ x * cast ⋯ y

@[implicit_reducible]

instance ConcreteBinaryTower.instMulConcreteBTField {k : ℕ} : Mul (ConcreteBTField k)

@[implicit_reducible]

instance ConcreteBinaryTower.instLTConcreteBTField (k : ℕ) : LT (ConcreteBTField k)

@[implicit_reducible]

instance ConcreteBinaryTower.instLEConcreteBTField (k : ℕ) : LE (ConcreteBTField k)

@[implicit_reducible]

instance ConcreteBinaryTower.instPreorderConcreteBTField (k : ℕ) : Preorder (ConcreteBTField k)

theorem ConcreteBinaryTower.toNatInRange {k : ℕ} (b : ConcreteBTField k) : BitVec.toNat b ≤ 2 ^ 2 ^ k * 1

theorem ConcreteBinaryTower.eq_zero_or_eq_one {a : ConcreteBTField 0} : a = zero ∨ a = one

theorem ConcreteBinaryTower.concrete_eq_zero_or_eq_one {k : ℕ} {a : ConcreteBTField k} (h_k_zero : k = 0) : a = zero ∨ a = one

theorem ConcreteBinaryTower.add_eq_one_iff (a b : ConcreteBTField 0) : a + b = 1 ↔ a = 0 ∧ b = 1 ∨ a = 1 ∧ b = 0

@[implicit_reducible]

instance ConcreteBinaryTower.instInvConcreteBTF {k : ℕ} : Inv (ConcreteBTField k)

theorem ConcreteBinaryTower.concrete_inv_zero {k : ℕ} : concrete_inv 0 = 0

theorem ConcreteBinaryTower.concrete_exists_pair_ne {k : ℕ} : ∃ (x : ConcreteBTField k) (y : ConcreteBTField k), x ≠ y

theorem ConcreteBinaryTower.concrete_zero_mul0 (b : ConcreteBTField 0) : concrete_mul zero b = zero

theorem ConcreteBinaryTower.concrete_mul_zero0 (a : ConcreteBTField 0) : concrete_mul a zero = zero

theorem ConcreteBinaryTower.concrete_one_mul0 (a : ConcreteBTField 0) : concrete_mul one a = a

theorem ConcreteBinaryTower.concrete_mul_one0 (a : ConcreteBTField 0) : concrete_mul a one = a

theorem ConcreteBinaryTower.concrete_mul_assoc0 (a b c : ConcreteBTField 0) : concrete_mul (concrete_mul a b) c = concrete_mul a (concrete_mul b c)

theorem ConcreteBinaryTower.concrete_mul_comm0 (a b : ConcreteBTField 0) : concrete_mul a b = concrete_mul b a

theorem ConcreteBinaryTower.if_zero_then_zero_else_self (x : ConcreteBTField 0) : (if x = zero then zero else x) = x

theorem ConcreteBinaryTower.concrete_mul_left_distrib0 (a b c : ConcreteBTField 0) : concrete_mul a (b + c) = concrete_mul a b + concrete_mul a c

theorem ConcreteBinaryTower.concrete_mul_right_distrib0 (a b c : ConcreteBTField 0) : concrete_mul (a + b) c = concrete_mul a c + concrete_mul b c

def ConcreteBinaryTower.natCast {k : ℕ} (n : ℕ) : ConcreteBTField k

def ConcreteBinaryTower.natCast_zero {k : ℕ} : natCast 0 = zero

def ConcreteBinaryTower.natCast_succ {k : ℕ} (n : ℕ) : natCast (n + 1) = natCast n + 1

@[implicit_reducible]

instance ConcreteBinaryTower.instNatCastConcreteBTField {k : ℕ} : NatCast (ConcreteBTField k)

@[simp]

theorem ConcreteBinaryTower.concrete_natCast_zero_eq_zero {k : ℕ} : natCast 0 = 0

@[simp]

theorem ConcreteBinaryTower.concrete_natCast_one_eq_one {k : ℕ} : natCast 1 = 1

@[simp]

theorem ConcreteBinaryTower.natCast_eq {k : ℕ} (n : ℕ) : ↑n = natCast n

def ConcreteBinaryTower.intCast {k : ℕ} (n : ℤ) : ConcreteBTField k

@[implicit_reducible]

instance ConcreteBinaryTower.instIntCastConcreteBTField {k : ℕ} : IntCast (ConcreteBTField k)

def ConcreteBinaryTower.intCast_ofNat {k : ℕ} (n : ℕ) : intCast ↑n = natCast n

@[simp]

theorem ConcreteBinaryTower.my_neg_mod_two (m : ℤ) : -m % 2 = if m % 2 = 0 then 0 else 1

@[simp]

theorem ConcreteBinaryTower.mod_two_eq_zero (m : ℤ) : m % 2 = -m % 2

def ConcreteBinaryTower.intCast_negSucc {k : ℕ} (n : ℕ) : intCast (Int.negSucc n) = -↑(n + 1)

@[implicit_reducible]

instance ConcreteBinaryTower.instHDivConcreteBTF {k : ℕ} : HDiv (ConcreteBTField k) (ConcreteBTField k) (ConcreteBTField k)

theorem ConcreteBinaryTower.concrete_div_eq_mul_inv {k : ℕ} (a b : ConcreteBTField k) : a / b = a * concrete_inv b

@[implicit_reducible]

instance ConcreteBinaryTower.instHPowConcreteBTFℤ {k : ℕ} : HPow (ConcreteBTField k) ℤ (ConcreteBTField k)

@[implicit_reducible]

instance ConcreteBinaryTower.instDivConcreteBTF {k : ℕ} : Div (ConcreteBTField k)

structure ConcreteBinaryTower.ConcreteBTFRingProps (k : ℕ) extends ConcreteBinaryTower.ConcreteBTFAddCommGroupProps k : Prop

• add_assoc (a b c : ConcreteBTField k) : a + b + c = a + (b + c)
• add_comm (a b : ConcreteBTField k) : a + b = b + a
• add_zero (a : ConcreteBTField k) : a + zero = a
• zero_add (a : ConcreteBTField k) : zero + a = a
• add_neg (a : ConcreteBTField k) : a + neg a = zero
• mul_eq (a b : ConcreteBTField k) (h_k : k > 0) {a₁ a₀ b₁ b₀ : ConcreteBTField (k - 1)} (_h_a : (a₁, a₀) = split h_k a) (_h_b : (b₁, b₀) = split h_k b) : concrete_mul a b = join h_k (concrete_mul a₀ b₁ + concrete_mul b₀ a₁ + concrete_mul (concrete_mul a₁ b₁) (Z (k - 1))) (concrete_mul a₀ b₀ + concrete_mul a₁ b₁)
• zero_mul (a : ConcreteBTField k) : concrete_mul zero a = zero
• zero_mul' (a : ConcreteBTField k) : concrete_mul 0 a = 0
• mul_zero (a : ConcreteBTField k) : concrete_mul a zero = zero
• mul_zero' (a : ConcreteBTField k) : concrete_mul a 0 = 0
• one_mul (a : ConcreteBTField k) : concrete_mul one a = a
• mul_one (a : ConcreteBTField k) : concrete_mul a one = a
• mul_assoc (a b c : ConcreteBTField k) : concrete_mul (concrete_mul a b) c = concrete_mul a (concrete_mul b c)
• mul_left_distrib (a b c : ConcreteBTField k) : concrete_mul a (b + c) = concrete_mul a b + concrete_mul a c
• mul_right_distrib (a b c : ConcreteBTField k) : concrete_mul (a + b) c = concrete_mul a c + concrete_mul b c

structure ConcreteBinaryTower.ConcreteBTFDivisionRingProps (k : ℕ) extends ConcreteBinaryTower.ConcreteBTFRingProps k : Prop

• add_assoc (a b c : ConcreteBTField k) : a + b + c = a + (b + c)
• add_comm (a b : ConcreteBTField k) : a + b = b + a
• add_zero (a : ConcreteBTField k) : a + zero = a
• zero_add (a : ConcreteBTField k) : zero + a = a
• add_neg (a : ConcreteBTField k) : a + neg a = zero
• mul_eq (a b : ConcreteBTField k) (h_k : k > 0) {a₁ a₀ b₁ b₀ : ConcreteBTField (k - 1)} (_h_a : (a₁, a₀) = split h_k a) (_h_b : (b₁, b₀) = split h_k b) : concrete_mul a b = join h_k (concrete_mul a₀ b₁ + concrete_mul b₀ a₁ + concrete_mul (concrete_mul a₁ b₁) (Z (k - 1))) (concrete_mul a₀ b₀ + concrete_mul a₁ b₁)
• zero_mul (a : ConcreteBTField k) : concrete_mul zero a = zero
• zero_mul' (a : ConcreteBTField k) : concrete_mul 0 a = 0
• mul_zero (a : ConcreteBTField k) : concrete_mul a zero = zero
• mul_zero' (a : ConcreteBTField k) : concrete_mul a 0 = 0
• one_mul (a : ConcreteBTField k) : concrete_mul one a = a
• mul_one (a : ConcreteBTField k) : concrete_mul a one = a
• mul_assoc (a b c : ConcreteBTField k) : concrete_mul (concrete_mul a b) c = concrete_mul a (concrete_mul b c)
• mul_left_distrib (a b c : ConcreteBTField k) : concrete_mul a (b + c) = concrete_mul a b + concrete_mul a c
• mul_right_distrib (a b c : ConcreteBTField k) : concrete_mul (a + b) c = concrete_mul a c + concrete_mul b c
• mul_inv_cancel (a : ConcreteBTField k) : a ≠ zero → concrete_mul a (concrete_inv a) = one

structure ConcreteBinaryTower.ConcreteBTFieldProps (k : ℕ) extends ConcreteBinaryTower.ConcreteBTFDivisionRingProps k : Prop

• add_assoc (a b c : ConcreteBTField k) : a + b + c = a + (b + c)
• add_comm (a b : ConcreteBTField k) : a + b = b + a
• add_zero (a : ConcreteBTField k) : a + zero = a
• zero_add (a : ConcreteBTField k) : zero + a = a
• add_neg (a : ConcreteBTField k) : a + neg a = zero
• mul_eq (a b : ConcreteBTField k) (h_k : k > 0) {a₁ a₀ b₁ b₀ : ConcreteBTField (k - 1)} (_h_a : (a₁, a₀) = split h_k a) (_h_b : (b₁, b₀) = split h_k b) : concrete_mul a b = join h_k (concrete_mul a₀ b₁ + concrete_mul b₀ a₁ + concrete_mul (concrete_mul a₁ b₁) (Z (k - 1))) (concrete_mul a₀ b₀ + concrete_mul a₁ b₁)
• zero_mul (a : ConcreteBTField k) : concrete_mul zero a = zero
• zero_mul' (a : ConcreteBTField k) : concrete_mul 0 a = 0
• mul_zero (a : ConcreteBTField k) : concrete_mul a zero = zero
• mul_zero' (a : ConcreteBTField k) : concrete_mul a 0 = 0
• one_mul (a : ConcreteBTField k) : concrete_mul one a = a
• mul_one (a : ConcreteBTField k) : concrete_mul a one = a
• mul_assoc (a b c : ConcreteBTField k) : concrete_mul (concrete_mul a b) c = concrete_mul a (concrete_mul b c)
• mul_left_distrib (a b c : ConcreteBTField k) : concrete_mul a (b + c) = concrete_mul a b + concrete_mul a c
• mul_right_distrib (a b c : ConcreteBTField k) : concrete_mul (a + b) c = concrete_mul a c + concrete_mul b c
• mul_inv_cancel (a : ConcreteBTField k) : a ≠ zero → concrete_mul a (concrete_inv a) = one
• mul_comm (a b : ConcreteBTField k) : concrete_mul a b = concrete_mul b a

@[reducible]

def ConcreteBinaryTower.mkRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Ring (ConcreteBTField k)

@[reducible]

def ConcreteBinaryTower.mkDivisionRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : DivisionRing (ConcreteBTField k)

@[reducible]

def ConcreteBinaryTower.mkFieldInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Field (ConcreteBTField k)

structure ConcreteBinaryTower.ConcreteBTFStepResult (k : ℕ) extends ConcreteBinaryTower.ConcreteBTFieldProps k : Type

• add_assoc (a b c : ConcreteBTField k) : a + b + c = a + (b + c)
• add_comm (a b : ConcreteBTField k) : a + b = b + a
• add_zero (a : ConcreteBTField k) : a + zero = a
• zero_add (a : ConcreteBTField k) : zero + a = a
• add_neg (a : ConcreteBTField k) : a + neg a = zero
• mul_eq (a b : ConcreteBTField k) (h_k : k > 0) {a₁ a₀ b₁ b₀ : ConcreteBTField (k - 1)} (_h_a : (a₁, a₀) = split h_k a) (_h_b : (b₁, b₀) = split h_k b) : concrete_mul a b = join h_k (concrete_mul a₀ b₁ + concrete_mul b₀ a₁ + concrete_mul (concrete_mul a₁ b₁) (Z (k - 1))) (concrete_mul a₀ b₀ + concrete_mul a₁ b₁)
• zero_mul (a : ConcreteBTField k) : concrete_mul zero a = zero
• zero_mul' (a : ConcreteBTField k) : concrete_mul 0 a = 0
• mul_zero (a : ConcreteBTField k) : concrete_mul a zero = zero
• mul_zero' (a : ConcreteBTField k) : concrete_mul a 0 = 0
• one_mul (a : ConcreteBTField k) : concrete_mul one a = a
• mul_one (a : ConcreteBTField k) : concrete_mul a one = a
• mul_assoc (a b c : ConcreteBTField k) : concrete_mul (concrete_mul a b) c = concrete_mul a (concrete_mul b c)
• mul_left_distrib (a b c : ConcreteBTField k) : concrete_mul a (b + c) = concrete_mul a b + concrete_mul a c
• mul_right_distrib (a b c : ConcreteBTField k) : concrete_mul (a + b) c = concrete_mul a c + concrete_mul b c
• mul_inv_cancel (a : ConcreteBTField k) : a ≠ zero → concrete_mul a (concrete_inv a) = one
• mul_comm (a b : ConcreteBTField k) : concrete_mul a b = concrete_mul b a
• instFintype : Fintype (ConcreteBTField k)
• fieldFintypeCard : Fintype.card (ConcreteBTField k) = 2 ^ 2 ^ k
• sumZeroIffEq (x y : ConcreteBTField k) : x + y = 0 ↔ x = y
• traceMapEvalAtRootsIs1 : TraceMapProperty (ConcreteBTField k) (Z k) k
• instIrreduciblePoly : Irreducible (definingPoly (Z k))