You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <used_lib_defs>...</used_lib_defs>: Imported library definitions directly used by the theorem.
* <used_repo_defs>...</used_repo_defs>: Definitions from the local project (but outside the current file), directly or transitively used by the theorem.
* <lib_lemmas>...</lib_lemmas>: Imported library lemmas/theorems that may assist the proof.
* <repo_lemmas>...</repo_lemmas>: Lemmas/theorems defined in the local project outside this file.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for used definitions and helpful lemmas (used_lib_defs, used_repo_defs, lib_lemmas, repo_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<used_lib_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</used_lib_defs>

<repo_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) :\n(l₁ ++ l₂)[i] = l₁[i]
</repo_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<used_lib_defs>
Eq in Init.Prelude
id in Init.Prelude
BitVec in Init.Prelude
Nat in Init.Prelude
BitVec.cast in Init.Data.BitVec.Basic
BitVec.extractLsb in Init.Data.BitVec.Basic
Field in Mathlib.Algebra.Field.Defs
Finset in Mathlib.Data.Finset.Defs
Finset.range in Mathlib.Data.Finset.Range
Polynomial.C in Mathlib.Algebra.Polynomial.Basic
Polynomial.X in Mathlib.Algebra.Polynomial.Basic
AdjoinRoot.instField in Mathlib.RingTheory.AdjoinRoot
Fintype in Mathlib.Data.Fintype.Defs
Fintype.card in Mathlib.Data.Fintype.Card
Irreducible in Mathlib.Algebra.Group.Irreducible.Defs
List in Init.Prelude
List.Vector in Mathlib.Data.Vector.Defs
NeZero in Init.Data.NeZero
Polynomial in Mathlib.Algebra.Polynomial.Basic
AdjoinRoot in Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.of in Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.root in Mathlib.RingTheory.AdjoinRoot
Eq.mp in Init.Core
CharP in Mathlib.Algebra.CharP.Defs
DivisionRing in Mathlib.Algebra.Field.Defs
DivisionSemiring in Mathlib.Algebra.Field.Defs
Finset.Icc in Mathlib.Order.Interval.Finset.Defs
GroupWithZero in Mathlib.Algebra.GroupWithZero.Defs
Ne in Init.Core
Equiv in Mathlib.Logic.Equiv.Defs
Equiv.ofBijective in Mathlib.Logic.Equiv.Defs
Fact in Mathlib.Logic.Basic
Fintype.ofEquiv in Mathlib.Data.Fintype.OfMap
Function.Bijective in Mathlib.Logic.Function.Defs
Function.Injective in Init.Data.Function
Function.Surjective in Init.Data.Function
Polynomial.Monic in Mathlib.Algebra.Polynomial.Degree.Definitions
Polynomial.eval₂ in Mathlib.Algebra.Polynomial.Eval.Defs
Prod in Init.Prelude
Semiring in Mathlib.Algebra.Ring.Defs
Fintype.ofFinite in Mathlib.Data.Fintype.EquivFin
List.Vector.cons in Mathlib.Data.Vector.Defs
List.Vector.nil in Mathlib.Data.Vector.Defs
Algebra in Mathlib.Algebra.Algebra.Defs
algebraMap in Mathlib.Algebra.Algebra.Defs
instAlgebra in Mathlib.LinearAlgebra.TensorAlgebra.Basic
BitVec.zero in Init.Data.BitVec.Basic
BitVec.append in Init.Data.BitVec.Basic
EquivLike in Mathlib.Data.FunLike.Equiv
RingEquiv in Mathlib.Algebra.Ring.Equiv
reduceDIte in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
BitVec.ofNat in Init.Prelude
BitVec.extractLsb' in Init.Data.BitVec.Basic
BitVec.setWidth in Init.Data.BitVec.Basic
cast in Init.Prelude
And in Init.Prelude
OfNat in Init.Prelude
pos in ToMathlib.Control.Comonad.Instances
BitVec.toNat in Init.Prelude
</used_lib_defs>

<used_repo_defs>
notation : 10 "GF(" term : 10 ")" => GaloisField term 1

class DCast (α : Sort*) (β : α → Sort*) where
  dcast : ∀ {a a' : α}, a = a' → β a → β a'
  dcast_id : ∀ {a : α}, dcast (Eq.refl a) = id

@[simp]
def BTField (k : ℕ) := (BinaryTowerAux k).1

def BinaryTowerAux (k : ℕ) : (Σ' (F : Type 0), BinaryTowerResult F k) :=
  match k with
  | 0 => 
    let curBTField := GF(2)
    let newList : List.Vector (GF(2)) 1 := List.Vector.cons (1 : GF(2)) List.Vector.nil
    let specialElement : GF(2) := newList.1.headI
    let firstElementOfVecIsSpecialElement : newList.1.headI = specialElement := rfl
    let specialElementIs1 : specialElement = 1 := by admit /- proof elided -/

structure BinaryTowerInductiveStepResult (k : ℕ) (prevBTField : Type _)
  (prevBTResult : BinaryTowerResult prevBTField k) [instPrevBTFieldIsField : Field prevBTField]
  (prevPoly : Polynomial prevBTField) (F : Type _) where
  binaryTowerResult : BinaryTowerResult F (k+1)
  eq_adjoin : F = AdjoinRoot prevPoly
  u_is_root : Eq.mp (eq_adjoin) binaryTowerResult.specialElement = AdjoinRoot.root prevPoly
  eval_defining_poly_at_root : Eq.mp (eq_adjoin) binaryTowerResult.specialElement^2 +
    Eq.mp (eq_adjoin) binaryTowerResult.specialElement * (of prevPoly) prevBTResult.specialElement
    + 1 = 0

structure BinaryTowerResult (F : Type _) (k : ℕ) where
  vec : (List.Vector F (k + 1))
  instField : (Field F)
  instFintype : Fintype F
  specialElement : F
  specialElementNeZero : NeZero specialElement
  firstElementOfVecIsSpecialElement [Inhabited F] : vec.1.headI = specialElement
  instIrreduciblePoly : (Irreducible (p := (definingPoly specialElement)))
  sumZeroIffEq : ∀ (x y : F), x + y = 0 ↔ x = y
  fieldFintypeCard : Fintype.card F = 2^(2^k)
  traceMapEvalAtRootsIs1 : TraceMapProperty F specialElement k

@[simp]
def sumZeroIffEq (k : ℕ) : ∀ (x y : BTField k),
  x + y = 0 ↔ x = y := (BinaryTowerAux k).2.sumZeroIffEq

@[simp]
instance Inhabited (k : ℕ) : Inhabited (BTField k) where
  default := (0 : BTField k)

structure TraceMapProperty (F : Type*) [Field F] (u : F) (k : ℕ) : Prop where
  element_trace : ∑ i ∈ Finset.range (2 ^ k), u ^ (2 ^ i) = 1
  inverse_trace : ∑ i ∈ Finset.range (2 ^ k), (u⁻¹) ^ (2 ^ i) = 1

noncomputable def definingPoly {F : Type*} [instField : Field F] (s : F)
  := X ^ 2 + C s * X + 1

def binary_tower_inductive_step
  (k : Nat)
  (prevBTField : Type _) [Field prevBTField]
  (prevBTResult : BinaryTowerResult prevBTField k)
: Σ' (F : Type _), BinaryTowerInductiveStepResult (k:=k) (prevBTField:=prevBTField)
  (prevBTResult:=prevBTResult) (prevPoly:=definingPoly (F:=prevBTField)
    (instField:=prevBTResult.instField) (s:=prevBTResult.specialElement)) (F:=F)
  (instPrevBTFieldIsField:=prevBTResult.instField) :=

def AlgebraTowerEquiv.symm (e : AlgebraTowerEquiv A B) : AlgebraTowerEquiv B A where
  toRingEquiv := fun i => (e.toRingEquiv i).symm
  commutesLeft' := fun i j h r => by admit /- proof elided -/

structure AlgebraTowerEquiv (A : ι → Type*) [∀ i, CommSemiring (A i)] [a : AlgebraTower A]
  (B : ι → Type*) [∀ i, CommSemiring (B i)] [b : AlgebraTower B]
  where
    toRingEquiv : ∀ i, (A i ≃+* B i)
    commutesLeft' : ∀ (i j : ι) (h : i ≤ j) (r : A i),
      (b.algebraMap (i:=i) (j:=j) (h:=h)) ((toRingEquiv i) r) =
      (toRingEquiv j) (a.algebraMap (i:=i) (j:=j) (h:=h) r)

structure SpecialElementRelation {F_prev : Type*} [Field F_prev] (t1 : F_prev)
  {F_cur : Type*} [Field F_cur] (u : F_cur) [Algebra F_prev F_cur] : Prop where
    sum_inv_eq : u + u⁻¹ = algebraMap F_prev F_cur t1
    h_u_square : u^2 = u * (algebraMap F_prev F_cur t1) + 1

instance irreducible_quadratic_defining_poly_of_traceMap_eq_1
  {F : Type*} [Field F] [Fintype F] [CharP F 2] (s : F) [NeZero s] (k : ℕ)
  (trace_map_prop : TraceMapProperty F s k)
  (fintypeCard : Fintype.card F = 2 ^ (2 ^ k))
  : Irreducible (definingPoly s) :=

instance charP_eq_2_of_add_self_eq_zero {F : Type*} [Field F]
    (sumZeroIffEq : ∀ (x y : F), x + y = 0 ↔ x = y) : CharP F 2 :=
  have h_two : (2 : (F)) = 0 := by admit /- proof elided -/

def coeff.{u} {F : Type u} [Semiring F] (f : F[X][Y]) (i j : ℕ) : F := (f.coeff j).coeff i

instance GF_2_fintype : Fintype (GF(2)) := Fintype.ofFinite (GF(2))

def join_via_add_smul {k : ℕ} (h_pos : k > 0) (hi_btf lo_btf : BTField (k - 1)) :
    BTField k :=

def binaryAlgebraTower {l r : ℕ} (h_le : l ≤ r) : Algebra (BTField l) (BTField r) :=

@[simp]
def AlgebraTower.toAlgebra {i j : ι} (h : i ≤ j) : Algebra (A i) (A j) :=
  (AlgebraTower.algebraMap (i:=i) (j:=j) (h:=h)).toAlgebra

@[simp]
def Z (k : ℕ) : BTField k := (BinaryTowerAux k).snd.specialElement 
</used_repo_defs>

<lib_lemmas>
BitVec.extractLsb_ofNat in Init.Data.BitVec.Lemmas
BitVec.zero_eq in Init.Data.BitVec.Basic
Nat.shiftRight_zero in Init.Data.Nat.Bitwise.Basic
Nat.sub_zero in Init.Data.Nat.Basic
Nat.zero_mod in Init.Data.Nat.Div.Basic
Nat.zero_shiftRight in Init.Data.Nat.Lemmas
Equiv.toFun_as_coe in Mathlib.Logic.Equiv.Defs
EquivLike.coe_coe in Mathlib.Logic.Equiv.Defs
Nat.add_eq_zero in Init.Data.Nat.Lemmas
Nat.add_one_sub_one in Init.Data.Nat.Basic
RingEquiv.toEquiv_eq_coe in Mathlib.Algebra.Ring.Equiv
and_false in Init.SimpLemmas
one_ne_zero in Mathlib.Algebra.NeZero
Nat.ne_zero_of_lt in Init.Data.Nat.Basic
Nat.one_lt_two_pow_iff in Init.Data.Nat.Lemmas
Nat.shiftRight_eq_zero in Init.Data.Nat.Bitwise.Basic
BitVec.toNat_ofNat in Init.Data.BitVec.Bootstrap
Nat.one_mod_two_pow_eq_one in Init.Data.Nat.Lemmas
Nat.add_sub_self_left in Init.Data.Nat.Basic
Nat.mul_two in Init.Data.Nat.Basic
Nat.pow_succ in Init.Data.Nat.Basic
Nat.sub_add_cancel in Init.Data.Nat.Basic
Nat.succ_eq_add_one in Init.Data.Nat.Basic
Nat.ofNat_pos in Mathlib.Data.Nat.Cast.Order.Ring
Nat.one_mod_two_pow in Init.Data.Nat.Lemmas
Nat.two_pow_pos in Init.Data.Nat.Basic
Nat.zero_lt_two in Init.Data.Nat.Basic
pow_pos in Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
BitVec.ofNat_toNat in Init.Data.BitVec.Bootstrap
BitVec.setWidth_eq in Init.Data.BitVec.Lemmas
BitVec.toNat_setWidth in Init.Data.BitVec.Bootstrap
Nat.and_two_pow_sub_one_eq_mod in Init.Data.Nat.Bitwise.Lemmas
Nat.mul_comm in Init.Data.Nat.Basic
Nat.two_pow_pred_mul_two in Init.Data.Nat.Lemmas
id_eq in Init.Prelude
Nat.add_sub_cancel in Init.Data.Nat.Basic
Nat.sub_add_comm in Init.Data.Nat.Lemmas
BitVec.extractLsb'_append_eq_of_le in Init.Data.BitVec.Lemmas
Nat.le_refl in Init.Prelude
congrArg in Init.Prelude
eq_mp_eq_cast in Init.PropLemmas
BitVec.append_eq in Init.Data.BitVec.Basic
BitVec.setWidth_append in Init.Data.BitVec.Lemmas
Nat.add_comm in Init.Data.Nat.Basic
Nat.div_eq_sub_mod_div in Init.Data.Nat.Lemmas
Nat.div_lt_of_lt_mul in Init.Data.Nat.Mod
Nat.div_mul_cancel in Init.Data.Nat.Dvd
Nat.dvd_sub_mod in Init.Data.Nat.Lemmas
Nat.mod_eq_of_lt in Init.Data.Nat.Div.Basic
Nat.pow_add in Init.Data.Nat.Lemmas
Nat.shiftLeft_eq in Init.Data.Nat.Bitwise.Basic
Nat.shiftRight_eq_div_pow in Init.Data.Nat.Bitwise.Basic
Nat.mod_le in Init.Data.Nat.Div.Basic
Nat.mod_lt in Init.Prelude
Nat.shiftLeft_add_eq_or_of_lt in Init.Data.Nat.Bitwise.Lemmas
BitVec.eq_of_toNat_eq in Init.Data.BitVec.Bootstrap
BitVec.isLt in Init.Data.BitVec.BasicAux
BitVec.toNat_append in Init.Data.BitVec.Bootstrap
OfNat.ofNat_ne_one in Mathlib.Algebra.CharZero.Defs
ne_eq in Init.SimpLemmas
not_false_eq_true in Init.SimpLemmas
pow_right_inj₀ in Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
Prod.ext_iff in Init.Ext
</lib_lemmas>

<repo_lemmas>
@[simp]
theorem dcast_eq : dcast (Eq.refl a) b = b

lemma join_via_add_smul_zero {k : ℕ} (h_pos : k > 0) :
  ⋘ 0, 0 ⋙ = 0

theorem one_le_sub_consecutive_two_pow (n : ℕ): 1 ≤ 2^(n+1) - 2^n

theorem zero_lt_pow_n (m : ℕ) (n : ℕ) (h_m : m > 0): 0 < m^n

lemma join_via_add_smul_one {k : ℕ} (h_pos : k > 0) :
  ⋘ 0, 1 ⋙ = 1

theorem one_le_two_pow_n (n : ℕ) : 1 ≤ 2 ^ n

theorem dcast_eq_root_cast (h : a = a') : dcast h b = _root_.cast (congrArg β h) b

theorem dcast_symm (ha : a = a') (hb : dcast ha b = b') : dcast (ha.symm) b' = b

theorem dcast_eq_dcast_iff (h : a = a'') (h' : a' = a'') :
    dcast h b = dcast h' b' ↔ b = dcast (h'.trans h.symm) b'

lemma join_via_add_smul_one_zero_eq_Z {k : ℕ} (h_pos : k > 0) :
  ⋘ 1, 0 ⋙ = Z k
</repo_lemmas>

<local_ctx>
import ArkLib.Data.Classes.DCast

import ArkLib.Data.FieldTheory.BinaryField.Tower.Basic

namespace ConcreteBinaryTower

open Polynomial

def ConcreteBTField : ℕ → Type := fun k => BitVec (2 ^ k)

section BitVecDCast

instance BitVec.instDCast : DCast Nat BitVec where
  dcast h := BitVec.cast h
  dcast_id := by admit /- proof elided -/

end BitVecDCast

section ConversionUtils

def fromNat {k : ℕ} (n : Nat) : ConcreteBTField k :=
  BitVec.ofNat (2 ^ k) n

instance ConcreteBTField.instDCast_local : DCast ℕ ConcreteBTField where
  dcast h_k_eq term_k1 := BitVec.cast (congrArg (fun n => 2 ^ n) h_k_eq) term_k1
  dcast_id := by admit /- proof elided -/

end ConversionUtils

section NumericLemmas

end NumericLemmas

section FieldOperationsAndInstances

def zero {k : ℕ} : ConcreteBTField k := BitVec.zero (2 ^ k)

def one {k : ℕ} : ConcreteBTField k := 1#(2 ^ k)

def split {k : ℕ} (h : k > 0) (x : ConcreteBTField k) :
    ConcreteBTField (k - 1) × ConcreteBTField (k - 1) :=
  let lo_bits : BitVec (2 ^ (k - 1) - 1 - 0 + 1) :=
    BitVec.extractLsb (hi := 2 ^ (k - 1) - 1) (lo := 0) x
  let hi_bits : BitVec (2 ^ k - 1 - 2 ^ (k - 1) + 1) :=
    BitVec.extractLsb (hi := 2 ^ k - 1) (lo := 2 ^ (k - 1)) x
  have h_lo : 2 ^ (k - 1) - 1 - 0 + 1 = 2 ^ (k - 1) := by admit /- proof elided -/

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

def Z (k : ℕ) : ConcreteBTField k :=
  if h_k : k = 0 then one
  else
    《 one (k:=k-1), zero (k:=k-1) 》

section FieldLemmasOfLevel0

end FieldLemmasOfLevel0

section NumericCasting

end NumericCasting

end FieldOperationsAndInstances

section BTFieldPropsOneLevelLiftingLemmas

variable {k : ℕ} {h_k : k > 0}

end BTFieldPropsOneLevelLiftingLemmas

section TowerFieldsConstruction

end TowerFieldsConstruction

section ConcreteBTFieldAlgebraConstruction

end ConcreteBTFieldAlgebraConstruction

noncomputable section ConcreteMultilinearBasis

open Module

end ConcreteMultilinearBasis

section TowerEquivalence

open BinaryTower

noncomputable def towerRingEquivFromConcrete0 : ConcreteBTField 0 ≃+* BTField 0 :=

noncomputable def towerRingHomForwardMap (k : ℕ) : ConcreteBTField k → BTField k :=
</local_ctx>

<target_theorem>
lemma towerRingHomForwardMap_Z (k : ℕ) :
  towerRingHomForwardMap k (Z k) = BinaryTower.Z k :=
</target_theorem>

