Concrete binary tower arithmetic

A nominal carrier with low-first bitvector coordinates, explicit word encoding, and executable recursive multiplication, inversion, and powers. Elementary laws and the additive group are available without the recursive field certificates. CompPoly.Fields.Binary.Tower.Concrete.Core re-exports this interface and supplies law records and instance assembly; CompPoly.Fields.Binary.Tower.Concrete.Field constructs the field.

At positive level k, the arithmetic adjoins a generator z satisfying z² = Z (k - 1) * z + 1 over the previous level, with Z 0 = 1. An element lo + hi * z stores lo in the low half and hi in the high half of its word; split returns (hi, lo). This is the quadratic tower of [DP23], §2.3, where the paper's X (k - 1) corresponds to Z k.

References

• Diamond, B. E. and Posen, J., Succinct arguments over towers of binary fields

structure ConcreteBinaryTower.ConcreteBTField (k : ℕ) : Type

A binary tower element with low-first bit coordinates at level k.

• toBitVec : BitVec (2 ^ k)

  The 2 ^ k binary coordinates.

@[inline]

def ConcreteBinaryTower.ConcreteBTField.ofBitVec {k : ℕ} (x : BitVec (2 ^ k)) : ConcreteBTField k

Interpret 2 ^ k bits as the coordinates of a level-k tower element.

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.toBitVec_ofBitVec {k : ℕ} (x : BitVec (2 ^ k)) : (ofBitVec x).toBitVec = x

Reading the coordinates of a constructed element recovers the input word.

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.ofBitVec_toBitVec {k : ℕ} (x : ConcreteBTField k) : ofBitVec x.toBitVec = x

Reconstructing an element from its stored coordinates recovers the element.

def ConcreteBinaryTower.ConcreteBTField.equivBitVec (k : ℕ) : ConcreteBTField k ≃ BitVec (2 ^ k)

The explicit equivalence between tower elements and their stored words.

theorem ConcreteBinaryTower.ConcreteBTField.toBitVec_injective {k : ℕ} : Function.Injective toBitVec

Stored word coordinates uniquely determine a tower element.

theorem ConcreteBinaryTower.ConcreteBTField.ofBitVec_injective {k : ℕ} : Function.Injective ofBitVec

Distinct stored words construct distinct tower elements.

theorem ConcreteBinaryTower.ConcreteBTField.ext {k : ℕ} {x y : ConcreteBTField k} (h : x.toBitVec = y.toBitVec) : x = y

Tower elements with equal stored word coordinates are equal.

@[inline]

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

Read the stored word as an unsigned natural number. This is not a field cast.

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.toNat_ofBitVec {k : ℕ} (x : BitVec (2 ^ k)) : (ofBitVec x).toNat = x.toNat

Reading a constructed word as a natural number preserves its unsigned value.

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.toNat_toBitVec {k : ℕ} (x : ConcreteBTField k) : x.toBitVec.toNat = x.toNat

Reading encoded bits as a natural number agrees with the tower word readback.

theorem ConcreteBinaryTower.ConcreteBTField.toNat_lt {k : ℕ} (x : ConcreteBTField k) : x.toNat < 2 ^ 2 ^ k

A level-k stored word lies below 2 ^ (2 ^ k).

theorem ConcreteBinaryTower.ConcreteBTField.toNat_injective {k : ℕ} : Function.Injective toNat

Unsigned word readback uniquely determines a tower element.

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

@[instance_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.ConcreteBTField.toBitVec_fromNat {k : ℕ} (n : ℕ) : (fromNat n).toBitVec = BitVec.ofNat (2 ^ k) n

The explicit natural-word constructor stores the low 2 ^ k bits.

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.toNat_fromNat {k : ℕ} (n : ℕ) : (fromNat n).toNat = n % 2 ^ 2 ^ k

Reading an explicit natural-word construction reduces modulo its word size.

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.fromNat_toNat {k : ℕ} (x : ConcreteBTField k) : fromNat x.toNat = x

Reconstructing a tower element from its unsigned stored word recovers it.

@[simp]

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

@[instance_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

@[instance_reducible]

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

@[instance_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

@[instance_reducible]

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

@[reducible, inline, deprecated "Use addition inherited from Add." (since := "2026-09-16")]

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

Compatibility name for addition inherited from the homogeneous operation.

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

@[instance_reducible]

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

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))

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)

@[instance_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 (x.toNat >>> 2 ^ (k - 1)) ∧ lo_btf = fromNat (x.toNat &&& 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).toBitVec = dcast ⋯ (hi.toBitVec ++ lo.toBitVec)

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.toBitVec = hi.toBitVec ++ lo.toBitVec

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.toBitVec = dcast ⋯ (BitVec.extractLsb (2 ^ k - 1) (2 ^ (k - 1)) x.toBitVec) ∧ lo_btf.toBitVec = dcast ⋯ (BitVec.extractLsb (2 ^ (k - 1) - 1) 0 x.toBitVec)

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 (x.toNat >>> 2 ^ (k - 1)) ∧ lo_btf = fromNat (x.toNat &&& 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.toNat_Z_succ (k : ℕ) : (Z (k + 1)).toNat = 2 ^ 2 ^ k

The generator at level k + 1 is the word with its only set bit at position 2 ^ k.

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

@[irreducible]

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

@[instance_reducible]

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

@[reducible, inline, deprecated "Use multiplication inherited from Mul." (since := "2026-09-16")]

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

Compatibility name for multiplication inherited from the homogeneous operation.

@[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

@[instance_reducible]

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

Strict unsigned order on stored words, independent of field arithmetic.

@[instance_reducible]

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

Unsigned order on stored words, independent of field arithmetic.

@[instance_reducible]

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

The preorder inherited from unsigned word readback.

theorem ConcreteBinaryTower.toNatInRange {k : ℕ} (b : ConcreteBTField k) : b.toNat ≤ 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

@[instance_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

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

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

@[instance_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

@[instance_reducible]

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

theorem 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

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

@[instance_reducible]

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

@[reducible, inline, deprecated "Use division inherited from Div." (since := "2026-09-16")]

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

Compatibility name for division inherited from the homogeneous operation.

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

@[reducible, inline, deprecated "Use integer powers from the Field instance." (since := "2026-09-16")]

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

Legacy integer-power dictionary using the raw binary-power routine.