Concrete Binary Tower Algebra

Algebra maps and embeddings for the concrete bitvector binary tower.

def ConcreteBinaryTower.canonicalAlgMap (k : ℕ) : ConcreteBTField k →+* ConcreteBTField (k + 1)

theorem ConcreteBinaryTower.toNat_canonicalAlgMap (k : ℕ) (x : ConcreteBTField k) : ((canonicalAlgMap k) x).toNat = x.toNat

The embedding into the next level preserves the stored natural word.

@[simp]

theorem ConcreteBinaryTower.generator_is_not_lifted_to_succ (k : ℕ) (x : ConcreteBTField k) : (canonicalAlgMap k) x ≠ Z (k + 1)

Z(k+1) is the adjoined root of poly k to ConcreteBTField (k+1), so it is not lifted to ConcreteBTField (k+1) by canonicalAlgMap

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField_add_eq (k n m : ℕ) : ConcreteBTField (k + n + m) = ConcreteBTField (k + (n + m))

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.RingHom_eq_of_dest_eq (k m n : ℕ) (h_eq : m = n) : (ConcreteBTField k →+* ConcreteBTField m) = (ConcreteBTField k →+* ConcreteBTField n)

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.RingHom_eq_of_source_eq (k n m : ℕ) (h_eq : k = n) : (ConcreteBTField k →+* ConcreteBTField m) = (ConcreteBTField n →+* ConcreteBTField m)

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.RingHom_cast_dest_apply (k m n : ℕ) (h_eq : m = n) (f : ConcreteBTField k →+* ConcreteBTField m) (x : ConcreteBTField k) : (cast ⋯ f) x = cast ⋯ (f x)

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.RingHom_cast_source_apply (k n m : ℕ) (h_eq : k = n) (f : ConcreteBTField k →+* ConcreteBTField m) (x : ConcreteBTField n) : (cast ⋯ f) x = f (cast ⋯ x)

@[irreducible]

def ConcreteBinaryTower.concreteTowerAlgebraMap (l r : ℕ) (h_le : l ≤ r) : ConcreteBTField l →+* ConcreteBTField r

Auxiliary definition for concreteTowerAlgebraMap using structural recursion. This is easier to reason about in proofs than the Nat.rec version.

theorem ConcreteBinaryTower.concreteTowerAlgebraMap_id (k : ℕ) : concreteTowerAlgebraMap k k ⋯ = RingHom.id (ConcreteBTField k)

theorem ConcreteBinaryTower.concreteTowerAlgebraMap_succ_1 (k : ℕ) : concreteTowerAlgebraMap k (k + 1) ⋯ = canonicalAlgMap k

Right associativity of the Tower Map

theorem ConcreteBinaryTower.concreteTowerAlgebraMap_succ (l r : ℕ) (h_le : l ≤ r) : concreteTowerAlgebraMap l (r + 1) ⋯ = (concreteTowerAlgebraMap r (r + 1) ⋯).comp (concreteTowerAlgebraMap l r h_le)

Left associativity of the Tower Map

theorem ConcreteBinaryTower.concreteTowerAlgebraMap_succ_last (r l : ℕ) (h_le : l ≤ r) : concreteTowerAlgebraMap l (r + 1) ⋯ = (concreteTowerAlgebraMap (l + 1) (r + 1) ⋯).comp (concreteTowerAlgebraMap l (l + 1) ⋯)

@[simp]

theorem ConcreteBinaryTower.ConcreteBTField.RingHom_comp_cast {α β γ δ : ℕ} (f : ConcreteBTField α →+* ConcreteBTField β) (g : ConcreteBTField β →+* ConcreteBTField γ) (h : γ = δ) : (cast ⋯ g).comp f = cast ⋯ (g.comp f)

Cast of composition of ConcreteBTField ring homomorphism is composition of casted ConcreteBTField ring homomorphism. Note that this assumes the SAME underlying instances (e.g. NonAssocSemiring) for both the input and output ring homs.

theorem ConcreteBinaryTower.concreteTowerAlgebraMap_assoc (r mid l : ℕ) (h_l_le_mid : l ≤ mid) (h_mid_le_r : mid ≤ r) : concreteTowerAlgebraMap l r ⋯ = (concreteTowerAlgebraMap mid r h_mid_le_r).comp (concreteTowerAlgebraMap l mid h_l_le_mid)

theorem ConcreteBinaryTower.toNat_concreteTowerAlgebraMap {i j : ℕ} (h : i ≤ j) (x : ConcreteBTField i) : ((concreteTowerAlgebraMap i j h) x).toNat = x.toNat

An embedding between any ordered levels preserves the stored natural word.

theorem ConcreteBinaryTower.concreteTowerAlgebraMap_eq_setWidth {i j : ℕ} (h : i ≤ j) (x : ConcreteBTField i) : ((concreteTowerAlgebraMap i j h) x).toBitVec = BitVec.setWidth (2 ^ j) x.toBitVec

An embedding between ordered levels zero-extends the original bitvector.

theorem ConcreteBinaryTower.concreteTowerAlgebraMap_Z_succ {k j : ℕ} (h : k + 1 ≤ j) : ((concreteTowerAlgebraMap (k + 1) j h) (Z (k + 1))).toBitVec = BitVec.ofNat (2 ^ j) (2 ^ 2 ^ k)

The image of the level-k + 1 generator keeps its set bit at position 2 ^ k.

@[instance_reducible]

instance ConcreteBinaryTower.instAlgebraTowerConcreteBTF : AlgebraTower ConcreteBTField

Formalization of Cross - Level Algebra : For any k ≤ τ, ConcreteBTField τ is an algebra over ConcreteBTField k.

@[reducible, inline]

abbrev ConcreteBinaryTower.ConcreteBTFieldAlgebra {l r : ℕ} (h_le : l ≤ r) : Algebra (ConcreteBTField l) (ConcreteBTField r)

def ConcreteBinaryTower.join_via_add_smul (k : ℕ) (h_pos : k > 0) (hi_btf lo_btf : ConcreteBTField (k - 1)) : ConcreteBTField k

theorem ConcreteBinaryTower.split_algebraMap_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField (k - 1)) : split h_pos ((algebraMap (ConcreteBTField (k - 1)) (ConcreteBTField k)) x) = (0, x)

An element x lifted from the base field ConcreteBTField (k-1) has (0, x) as its split representation in ConcreteBTField k.

theorem ConcreteBinaryTower.algebraMap_succ_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField (k - 1)) : (algebraMap (ConcreteBTField (k - 1)) (ConcreteBTField k)) x = join h_pos 0 x

theorem ConcreteBinaryTower.algebraMap_eq_zero_x {i j : ℕ} (h_le : i < j) (x : ConcreteBTField i) : (algebraMap (ConcreteBTField i) (ConcreteBTField j)) x = join ⋯ 0 ((algebraMap (ConcreteBTField i) (ConcreteBTField (j - 1))) x)

theorem ConcreteBinaryTower.split_smul_Z_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField (k - 1)) : split h_pos (x • Z k) = (x, 0)

theorem ConcreteBinaryTower.smul_Z_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField (k - 1)) : x • Z k = join h_pos x 0

@[simp]

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

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

theorem ConcreteBinaryTower.ConcreteBTFieldAlgebra_def (l r : ℕ) (h_le : l ≤ r) : ConcreteBTFieldAlgebra h_le = (concreteTowerAlgebraMap l r h_le).toAlgebra

theorem ConcreteBinaryTower.algebraMap_ConcreteBTFieldAlgebra_def (l r : ℕ) (h_le : l ≤ r) : algebraMap (ConcreteBTField l) (ConcreteBTField r) = concreteTowerAlgebraMap l r h_le

theorem ConcreteBinaryTower.coe_one_succ (l : ℕ) : (algebraMap (ConcreteBTField l) (ConcreteBTField (l + 1))) 1 = 1

theorem ConcreteBinaryTower.unique_linear_decomposition_succ (k : ℕ) (x : ConcreteBTField (k + 1)) : ∃! p : ConcreteBTField k × ConcreteBTField k, x = join_via_add_smul (k + 1) ⋯ p.1 p.2

@[simp]

theorem ConcreteBinaryTower.ConcreteBTFieldAlgebra_id {l r : ℕ} (h_eq : l = r) : ConcreteBTFieldAlgebra ⋯ = h_eq ▸ Algebra.id (ConcreteBTField l)

theorem ConcreteBinaryTower.ConcreteBTFieldAlgebra_apply_assoc (l mid r : ℕ) (h_l_le_mid : l ≤ mid) (h_mid_le_r : mid ≤ r) (x : ConcreteBTField l) : (algebraMap (ConcreteBTField l) (ConcreteBTField r)) x = (algebraMap (ConcreteBTField mid) (ConcreteBTField r)) ((algebraMap (ConcreteBTField l) (ConcreteBTField mid)) x)

@[reducible, inline]

abbrev ConcreteBinaryTower.binaryTowerModule {l r : ℕ} (h_le : l ≤ r) : Module (ConcreteBTField l) (ConcreteBTField r)

This also provides the corresponding Module instance.

@[instance_reducible]

instance ConcreteBinaryTower.algebra_adjacent_tower (l : ℕ) : Algebra (ConcreteBTField l) (ConcreteBTField (l + 1))

theorem ConcreteBinaryTower.algebraMap_adjacent_tower_def (l : ℕ) : algebraMap (ConcreteBTField l) (ConcreteBTField (l + 1)) = canonicalAlgMap l

theorem ConcreteBinaryTower.aeval_definingPoly_at_Z_succ (k : ℕ) : (Polynomial.aeval (Z (k + 1))) (definingPoly (Z k)) = 0