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>
Fin in Init.Prelude
Nat in Init.Prelude
Polynomial in Mathlib.Algebra.Polynomial.Basic
WithBot in Mathlib.Order.TypeTags
Subspace in Mathlib.Algebra.Module.Submodule.Basic
Set in Mathlib.Data.Set.Defs
Set.Ico in Mathlib.Order.Interval.Set.Defs
Submodule in Mathlib.Algebra.Module.Submodule.Defs
Submodule.span in Mathlib.LinearAlgebra.Span.Defs
Polynomial.C in Mathlib.Algebra.Polynomial.Basic
Fin.castLE in Init.Data.Fin.Basic
Finset in Mathlib.Data.Finset.Defs
Finset.univ in Mathlib.Data.Fintype.Defs
FiniteDimensional in Mathlib.LinearAlgebra.FiniteDimensional.Defs
Polynomial.X in Mathlib.Algebra.Polynomial.Basic
Module in Mathlib.Algebra.Module.Defs
Module.finrank in Mathlib.LinearAlgebra.Dimension.Finrank
Set.range in Mathlib.Data.Set.Operations
Fintype in Mathlib.Data.Fintype.Defs
Semiring in Mathlib.Algebra.Ring.Defs
toFun in ToMathlib.Control.Monad.Hom
LinearIndependent in Mathlib.LinearAlgebra.LinearIndependent.Defs
Matrix in Mathlib.LinearAlgebra.Matrix.Defs
CharP in Mathlib.Algebra.CharP.Defs
Fin.isEmpty' in Mathlib.Logic.IsEmpty
Finset.Icc in Mathlib.Order.Interval.Finset.Defs
Finset.range in Mathlib.Data.Finset.Range
Fintype.card in Mathlib.Data.Fintype.Card
Polynomial.Monic in Mathlib.Algebra.Polynomial.Degree.Definitions
Fact in Mathlib.Logic.Basic
Function.Bijective in Mathlib.Logic.Function.Defs
Function.Injective in Init.Data.Function
LinearIndepOn in Mathlib.LinearAlgebra.LinearIndependent.Defs
Set.InjOn in Mathlib.Data.Set.Operations
Set.image in Mathlib.Data.Set.Defs
Subtype in Init.Prelude
Subtype.val in Init.Prelude
id in Init.Prelude
Field in Mathlib.Algebra.Field.Defs
OrderDual in Mathlib.Order.Basic
OrderDual.toDual in Mathlib.Order.Synonym
AddHom in Mathlib.Algebra.Group.Hom.Defs
LinearMap in Mathlib.Algebra.Module.LinearMap.Defs
Module.Basis in Mathlib.LinearAlgebra.Basis.Defs
AddSubmonoidClass in Mathlib.Algebra.Group.Submonoid.Defs
Finsupp in Mathlib.Data.Finsupp.Defs
Finsupp.linearCombination in Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.sum in Mathlib.Algebra.BigOperators.Finsupp.Basic
Module.Basis.mk in Mathlib.LinearAlgebra.Basis.Basic
Polynomial.coeff in Mathlib.Algebra.Polynomial.Basic
Polynomial.degreeLT in Mathlib.RingTheory.Polynomial.Basic
Polynomial.monomial in Mathlib.Algebra.Polynomial.Basic
SetLike in Mathlib.Data.SetLike.Basic
</used_lib_defs>

<used_repo_defs>
def getBit (k n : Nat) : Nat := (n >>> k) &&& 1

instance finiteDimensional_degreeLT {n : ℕ} (h_n_pos : 0 < n) :
  FiniteDimensional L L⦃< n⦄[X] :=

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

noncomputable def monomialBasisOfDegreeLT {n : ℕ} : Basis (Fin n) L (L⦃< n⦄[X]) :=
</used_repo_defs>

<lib_lemmas>
Fin.card_Ico in Mathlib.Order.Interval.Finset.Fin
Fin.coe_ofNat_eq_mod in Mathlib.Data.Fin.Basic
Fintype.card_ofFinset in Mathlib.Data.Fintype.Card
LinearIndependent.injective in Mathlib.LinearAlgebra.LinearIndependent.Defs
Nat.zero_mod in Init.Data.Nat.Div.Basic
Set.card_image_of_injective in Mathlib.Data.Set.Finite.Basic
Set.mem_image in Mathlib.Data.Set.Operations
Set.mem_image_of_mem in Mathlib.Data.Set.Operations
Set.range_comp in Mathlib.Data.Set.Image
Set.toFinset_card in Mathlib.Data.Fintype.Card
Subtype.coe_injective in Mathlib.Data.Subtype
Subtype.mk_eq_mk in Mathlib.Data.Subtype
Subtype.range_coe in Mathlib.Data.Set.Image
finrank_span_set_eq_card in Mathlib.LinearAlgebra.Dimension.Constructions
tsub_zero in Mathlib.Algebra.Order.Sub.Defs
Module.card_eq_pow_finrank in Mathlib.FieldTheory.Finiteness
Finset.card_univ in Mathlib.Data.Fintype.Card
Finset.sum_const in Mathlib.Algebra.BigOperators.Group.Finset.Basic
Polynomial.degree_X_sub_C in Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_prod_of_monic in Mathlib.Algebra.Polynomial.BigOperators
Polynomial.monic_X_sub_C in Mathlib.Algebra.Polynomial.Monic
mul_one in Mathlib.Algebra.Group.Defs
nsmul_eq_mul in Mathlib.Algebra.Ring.Defs
Fact.out in Mathlib.Logic.Basic
Fin.le_zero_iff' in Mathlib.Data.Fin.SuccPred
Nat.not_lt_zero in Init.Prelude
Set.Ico_eq_empty_iff in Mathlib.Order.Interval.Set.Basic
Set.compl_eq_univ_diff in Mathlib.Order.BooleanAlgebra.Set
Set.empty_subset in Mathlib.Data.Set.Basic
Set.image_empty in Mathlib.Data.Set.Image
Set.image_subset_image_iff in Mathlib.Data.Set.Image
Set.mem_Ico in Mathlib.Order.Interval.Set.Defs
Set.subset_compl_singleton_iff in Mathlib.Order.BooleanAlgebra.Set
Submodule.span_mono in Mathlib.LinearAlgebra.Span.Defs
linearIndependent_iff_notMem_span in Mathlib.LinearAlgebra.LinearIndependent.Defs
Finset.prod_ne_zero_iff in Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Polynomial.eval_C in Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_X in Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_prod in Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_sub in Mathlib.Algebra.Polynomial.Eval.Defs
one_mul in Mathlib.Algebra.Group.Defs
sub_eq_zero in Mathlib.Algebra.Group.Basic
Polynomial.degree_C_mul in Mathlib.Algebra.Polynomial.Degree.Lemmas
inv_ne_zero in Mathlib.Algebra.GroupWithZero.NeZero
one_div in Mathlib.Algebra.Group.Defs
CharP.cast_eq_zero in Mathlib.Algebra.CharP.Defs
Fin.coe_castLE in Init.Data.Fin.Lemmas
Fin.sum_univ_eq_sum_range in Mathlib.Data.Fintype.BigOperators
Fin.val_eq_zero_iff in Init.Data.Fin.Lemmas
Finset.sum_congr in Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_empty in Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.univ_eq_empty in Mathlib.Data.Finset.BooleanAlgebra
Nat.and_one_is_mod in Init.Data.Nat.Bitwise.Lemmas
Nat.cast_ite in Mathlib.Data.Nat.Cast.Defs
Nat.cast_ofNat in Mathlib.Data.Nat.Cast.Defs
Nat.cast_one in Mathlib.Data.Nat.Cast.Defs
Nat.cast_pow in Mathlib.Data.Nat.Cast.Basic
Nat.lt_one_iff in Init.Data.Nat.Basic
Nat.mod_two_ne_one in Init.Data.Nat.Lemmas
Nat.range_succ_eq_Icc_zero in Mathlib.Order.Interval.Finset.Nat
Nat.sub_add_cancel in Init.Data.Nat.Basic
Polynomial.degree_pow in Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_prod in Mathlib.Algebra.Polynomial.BigOperators
WithBot.zero_eq_coe in Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
if_false in Init.ByCases
if_true in Init.ByCases
mul_eq_zero_comm in Mathlib.Algebra.GroupWithZero.Defs
or_false in Init.SimpLemmas
pow_zero in Mathlib.Algebra.Group.Defs
Polynomial.coeff_ne_zero_of_eq_degree in Mathlib.Algebra.Polynomial.Degree.Definitions
Matrix.det_of_lowerTriangular in Mathlib.LinearAlgebra.Matrix.Block
Matrix.linearIndependent_rows_of_det_ne_zero in Mathlib.LinearAlgebra.Matrix.Determinant.Basic
AddHom.coe_mk in Mathlib.Algebra.Group.Hom.Defs
LinearMap.coe_mk in Mathlib.Algebra.Module.LinearMap.Defs
OrderDual.toDual_lt_toDual in Mathlib.Order.Synonym
Polynomial.coeff_eq_zero_of_natDegree_lt in Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_eq_of_degree_eq_some in Mathlib.Algebra.Polynomial.Degree.Definitions
LinearIndependent.of_comp in Mathlib.LinearAlgebra.LinearIndependent.Defs
Fintype.card_fin in Mathlib.Data.Fintype.Card
Nat.two_pow_pos in Init.Data.Nat.Basic
Submodule.eq_top_of_finrank_eq in Mathlib.LinearAlgebra.FiniteDimensional.Basic
finrank_span_eq_card in Mathlib.LinearAlgebra.Dimension.Constructions
</lib_lemmas>

<repo_lemmas>
theorem getBit_repr {ℓ : Nat} : ∀ j, j < 2^ℓ →
  j = ∑ k ∈ Finset.Icc 0 (ℓ-1), (getBit k j) * 2^k

lemma getBit_of_shiftRight {n p : ℕ}:
  ∀ k, getBit k (n >>> p) = getBit (k+p) n

lemma getBit_eq_zero_or_one {k n : Nat} :
  getBit k n = 0 ∨ getBit k n = 1

theorem finrank_degreeLT_n (n : ℕ) : Module.finrank L (L⦃< n⦄[X]) = n
</repo_lemmas>

<local_ctx>
import ArkLib.Data.Nat.Bitwise

import ArkLib.Data.Polynomial.Frobenius

import ArkLib.Data.Polynomial.MonomialBasis

import Mathlib.LinearAlgebra.StdBasis

import Mathlib.Algebra.Polynomial.Degree.Definitions

open Polynomial FiniteDimensional Finset Module

namespace AdditiveNTT

variable {r : ℕ} [NeZero r]

variable {L : Type u} [Field L] [Fintype L] [DecidableEq L]

variable (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q]
  [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [hF₂ : Fact (Fintype.card 𝔽q = 2)]

variable [Algebra 𝔽q L]

variable (h_dim : Module.finrank 𝔽q L = r)

variable (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]

section LinearSubspaces

def U (i : Fin r) : Subspace 𝔽q L := Submodule.span 𝔽q (β '' (Set.Ico 0 i))

noncomputable def W (i : Fin r) : L[X] :=
  ∏ u : U 𝔽q β i, (X - C u.val)

end LinearSubspaces

section LinearityOfSubspaceVanishingPolynomials

noncomputable def normalizedW (i : Fin r) : L[X] :=
  C (1 / (W 𝔽q β i).eval (β i)) * W 𝔽q β i

end LinearityOfSubspaceVanishingPolynomials

section NovelPolynomialBasisProof

noncomputable def basisVectors (ℓ : Nat) (h_ℓ : ℓ ≤ r) :
  Fin (2 ^ ℓ) → L⦃<2^ℓ⦄[X] :=
  fun j => ⟨Xⱼ 𝔽q β ℓ h_ℓ j, by admit /- proof elided -/
  ⟩

abbrev CoeffVecSpace (L : Type u) (ℓ : Nat) := Fin (2^ℓ) → L

def toCoeffsVec (ℓ : Nat) : L⦃<2^ℓ⦄[X] →ₗ[L] CoeffVecSpace L ℓ where
  toFun := fun p => fun i => p.val.coeff i.val
  map_add' := fun p q => by admit /- proof elided -/

noncomputable def changeOfBasisMatrix (ℓ : Nat) (h_ℓ : ℓ ≤ r) : Matrix (Fin (2^ℓ)) (Fin (2^ℓ)) L :=
    fun j i => (toCoeffsVec (L := L) (ℓ := ℓ) (
      basisVectors 𝔽q β ℓ h_ℓ j)) i
</local_ctx>

<target_theorem>
theorem basisVectors_span (ℓ : Nat) (h_ℓ : ℓ ≤ r) :
    Submodule.span L (Set.range (basisVectors 𝔽q β ℓ h_ℓ)) = ⊤ :=
</target_theorem>

