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:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <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 available definitions and lemmas (all_available_defs, all_available_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:
<all_available_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)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_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:
<all_available_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.append 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.xor in Init.Data.BitVec.Basic
AddCommGroup in Mathlib.Algebra.Group.Defs
Int in Init.Data.Int.Basic
Int.negSucc in Init.Data.Int.Basic
Ring in Mathlib.Algebra.Ring.Defs
NNRat in Mathlib.Data.Rat.Init
NNRat.castRec in Mathlib.Algebra.Field.Defs
Rat in Init.Data.Rat.Basic
Rat.castRec in Mathlib.Algebra.Field.Defs
toFun in ToMathlib.Control.Monad.Hom
RingHom in Mathlib.Algebra.Ring.Hom.Defs
RingHom.toAlgebra in Mathlib.Algebra.Algebra.Defs
invFun in ToMathlib.Control.Monad.Equiv
left_inv in ToMathlib.Control.Monad.Equiv
right_inv in ToMathlib.Control.Monad.Equiv
False.elim in Init.Prelude
Finite in Mathlib.Data.Finite.Defs
absurd in Init.Prelude
instFintypeProd in Mathlib.Data.Fintype.Prod
reduceDIte in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
RingHom.id in Mathlib.Algebra.Ring.Hom.Defs
CommSemiring in Mathlib.Algebra.Ring.Defs
Preorder in Mathlib.Order.Defs.PartialOrder
CommMonoid in Mathlib.Algebra.Group.Defs
Fin in Init.Prelude
Module.Basis in Mathlib.LinearAlgebra.Basis.Defs
Algebra.algebraMap in Mathlib.Algebra.Algebra.Defs
Module.Basis.mk in Mathlib.LinearAlgebra.Basis.Basic
Set in Mathlib.Data.Set.Defs
Submodule in Mathlib.Algebra.Module.Submodule.Defs
PowerBasis in Mathlib.RingTheory.PowerBasis
gen in VCVio.CryptoFoundations.FiatShamir
RingEquiv in Mathlib.Algebra.Ring.Equiv
Decidable in Init.Prelude
Equiv.cast in Mathlib.Logic.Equiv.Defs
AdjoinRoot.powerBasis in Mathlib.RingTheory.AdjoinRoot
Field.toCommRing in Mathlib.Algebra.Field.Defs
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
MonoidHom in Mathlib.Algebra.Group.Hom.Defs
OneHom in Mathlib.Algebra.Group.Hom.Defs
EquivLike in Mathlib.Data.FunLike.Equiv

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

@[simp]
instance AlgebraTower.toIsScalarTower (a : AlgebraTower C) {i j k : ι}
    (h1 : i ≤ j) (h2 : j ≤ k) :
    letI : Algebra (C i) (C j) :=

def split (k : ℕ) (h_k : k > 0) (x : BTField k) : BTField (k-1) × BTField (k-1) :=

def powerBasisSucc (k : ℕ) :
    PowerBasis (BTField k) (BTField (k+1)) :=

def BTField_succ_alg_equiv_adjoinRoot (k : ℕ) :
  AdjoinRoot (poly k) ≃ₐ[BTField k] BTField (k + 1) :=

@[simp]
def poly (k : ℕ) : Polynomial (BTField k) := definingPoly (s:=(Z k))

@[simp]
instance CommRing (k : ℕ) : CommRing (BTField k) := Field.toCommRing

def towerAlgebraMap (l r : ℕ) (h_le : l ≤ r) : BTField l →+* BTField r :=

def canonicalEmbedding (k : ℕ) : BTField k →+* BTField (k+1) :=
  AdjoinRoot.of (poly k)

instance (priority := 1000) algebra_adjacent_tower (l : ℕ) :
  Algebra (BTField l) (BTField (l+1)) :=

instance polyMonic (n : ℕ) : Monic (poly n) := definingPoly_is_monic (Z n)

noncomputable def toMLE (A : Matrix (Fin (2 ^ m)) (Fin (2 ^ n)) R) : R[X Fin n][X Fin m] :=
  MLE' (MLE' ∘ A)

def bitVecToString (width : ℕ) (bv : BitVec width) : String :=
  Fin.foldl width (fun (s : String) (idx : Fin width) =>
    
    
    s.push (if BitVec.getLsb bv (Fin.rev idx) then '1' else '0')
  ) ""

@[inline]
def ofOutputOnly
    (liftStmt : OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtOut × (∀ i, InnerOStmtOut i) →
                OuterStmtOut × (∀ i, OuterOStmtOut i)) :
    OracleStatement.Lens OuterStmtIn OuterStmtOut OuterStmtIn InnerStmtOut
                        OuterOStmtIn OuterOStmtOut OuterOStmtIn InnerOStmtOut :=
  ⟨id, liftStmt⟩

def relHammingDist (u v : ι → F) : ℚ≥0 :=
  hammingDist u v / Fintype.card ι

def Cache.cons (n : ℕ) (leaves : List.Vector α (2 ^ (n + 1))) (cache : Cache α n) :
    Cache α (n + 1) :=
  Fin.snoc cache leaves

instance : MvPolynomialLike σ R (MvPolynomial σ R) where
  X := MvPolynomial.X
  eval₂ := fun f g => eval₂Hom f g
  eval₂_C := fun f g r => by admit /- proof elided -/

def OracleVerifier.addSalt (V : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) :
    OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut (pSpec.addSalt Salt) where
  verify := fun stmtIn challenges => sorry
  
  
  embed := sorry
  hEq := sorry

def OracleSpec.proverOracle (StmtIn : Type) {n : ℕ} (pSpec : ProtocolSpec n) :
    OracleSpec pSpec.MessageIdx :=
  fun i => (StmtIn × pSpec.Transcript i.val.castSucc, pSpec.Message i)

def eval (x : Fin numWires → 𝓡) (g : Gate 𝓡 numWires) : 𝓡 :=
  g.qL * x g.a + g.qR * x g.b + g.qO * x g.c + g.qM * (x g.a * x g.b) + g.qC

PFunctor.Lens in ToMathlib.PFunctor.Basic

instance {k : ℕ} : NeZero (Z k) := (BinaryTowerAux k).snd.specialElementNeZero

Membership.mem in Init.Prelude

HMod in Init.Prelude

output := fun _ => do 
    pure (⟨true, fun _ => ()⟩, ())

inferInstanceAs in Init.Prelude

instance domain_neg_inst {i : Fin n} : Neg (evalDomain D i.1) where
  neg := fun x => ⟨_, minus_one_in_doms D i.2⟩ * x

ringChar in Mathlib.Algebra.CharP.Defs

def dotProduct [Zero R] [Add R] [Mul R] (a b : Vector R n) : R :=
  a.zipWith (· * ·) b |>.foldl (· + ·) 0

hEq : ∀ i, OStmtOut i = match embed i with
    | Sum.inl j => OStmtIn j
    | Sum.inr j => pSpec.Message j

def sumExceptFirst' (n : ℕ) (h : n > 0) (D : Fin (n - 1) → Finset R) :
    MvPolynomial (Fin n) R →ₗ[R] Polynomial R :=

One in Init.Prelude

def domainEnum (i : Fin (n + 1)) : Fin (2 ^ (n - i)) ↪ evalDomain D i :=
  ⟨domain D n i.1, domain_injective D i.1 (by admit /- proof elided -/
  )⟩

noncomputable def qCompositionChain (i : Fin r) : L[X] :=
  match i with
  | ⟨0, _⟩ => X
  | ⟨k + 1, h_k_add_1⟩ => (qMap 𝔽q β ⟨k, by admit /- proof elided -/
  ⟩).comp (qCompositionChain ⟨k, by admit /- proof elided -/
  ⟩)

local instance : Fintype F := Fintype.ofFinite F

instance [Fintype F] [Nonempty F] [Semiring F] [DecidableEq ι] [DecidableEq F] {l : ℕ}
  {u : Fin l → ι → F} : Nonempty {x // x ∈ parametrisedCurveFinite u} :=

def nonsquare [Semiring F] (ι' : ℕ) (α : ι → F) : Matrix ι (Fin ι') F :=
  Matrix.of fun i j => (α i) ^ j.1

NatCast in Init.Data.Cast

def sumExceptFirst (n : ℕ) (D : Fin n → Finset R) :
    MvPolynomial (Fin (n + 1)) R →ₗ[R] Polynomial R :=

abbrev drop (m : ℕ) (h : m ≤ n)
    (transcript : FullTranscript pSpec) : FullTranscript (pSpec.drop m h) :=
  Fin.drop m h transcript

def new (domainSeparator : DomainSeparator U H) : HashStateWithInstructions U H :=
  letI stack := domainSeparator.finalize
  letI tag := generateTag domainSeparator.asBytes
  { ds := Initialize.new tag, stack := stack }

hEq := naVerifier.hEq

abbrev Field := ZMod fieldSize

def sub_descending (p q : UniPoly R) : QuotientUniPoly R :=
  Quotient.mk _ (sub p q)

Fin.last in Init.Data.Fin.Basic

instance : ∀ j, OracleInterface ((pSpecFold D x k s).Message j) :=
  instOracleInterfaceMessageSeqCompose

def solutionToE (e k : ℕ) (v : Fin (2 * e + k) → F) : Polynomial F :=
  ⟨
    insert e ((Finset.range e).filter (fun x => liftF v x ≠ 0)),
    fun i => if i = e then 1 else if i < e then liftF v i else 0,
    by admit /- proof elided -/
  ⟩

receiveChallenge | ⟨0, h⟩ => nomatch h

Finset.Iio in Mathlib.Order.Interval.Finset.Defs

def monomialY (n : ℕ) : F[X] →ₗ[F[X]] F[X][Y] where
  toFun t := ⟨Finsupp.single n t⟩
  map_add' x y := by admit /- proof elided -/

def univPolyHom {F : Type} [CommRing F] [IsDomain F] : F[X] →+* RatFunc F :=
  algebraMap (F[X]) (RatFunc F)

Rat in Init.Data.Rat.Basic

StateT.run in Init.Control.State

def pow (S : Finset ι) (φ : ι ↪ F) (k : ℕ) : indexPow S φ k ↪ F :=
    Function.Embedding.subtype fun y => y ∈ indexPow S φ k

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

RatFunc.eval in Mathlib.FieldTheory.RatFunc.AsPolynomial

def hammingClose (i : Fin (ℓ + 1)) (f : OracleFunction 𝔽q β
    (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i) : Prop :=
  2 * Code.distFromCode (u := f)
    (C := BBF_Code 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i) <
    (BBF_CodeDistance ℓ 𝓡 i : ℕ∞)

@[elab_as_elim]
def dconcat {n : ℕ} {motive : Fin (n + 1) → Sort u}
    (u : (i : Fin n) → motive i.castSucc) (a : motive (last n)) (i : Fin (n + 1)) : motive i :=
  match n with
  | 0 => match i with | 0 => a
  | _ + 1 => dcons (u 0) (dconcat (fun i => u (Fin.succ i)) a) i

def inputRelation [DecidableEq F] (δ : ℝ≥0) :
    Set
      (
        (Statement (k := k) F 0 × (∀ j, OracleStatement (k := k) D x s 0 j)) ×
        Witness F s d (0 : Fin (k + 2))
      ) :=
  match k with
  | 0 => FinalFoldPhase.inputRelation D x s d (round_bound dom_size_cond) δ
  | .succ _ => FoldPhase.inputRelation D x s d 0 (round_bound dom_size_cond) δ

instance {relIn : Set (StmtIn × WitIn)} {relOut : Set (StmtOut × WitOut)}
    {verifier : Verifier oSpec StmtIn StmtOut pSpec} {WitMid : Fin (n + 1) → Type}
    {extractor : Extractor.RoundByRound oSpec StmtIn WitIn WitOut pSpec WitMid} :
    CoeFun (verifier.KnowledgeStateFunction init impl relIn relOut extractor)
    (fun _ => (m : Fin (n + 1)) → StmtIn → Transcript m pSpec → WitMid m → Prop) :=
      ⟨fun f => f.toFun⟩

def sumcheckFoldKnowledgeError := fun j : (pSpecSumcheckFold 𝔽q β (ϑ:=ϑ)
    (h_ℓ_add_R_rate := h_ℓ_add_R_rate)).ChallengeIdx =>
    if hj: (j.val % NBlockMessages (ϑ:=ϑ)) % 2 = 1 then
      foldKnowledgeError 𝔽q β (ϑ:=ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
        ⟨j / NBlockMessages (ϑ:=ϑ) * ϑ + ((j % NBlockMessages (ϑ:=ϑ)) / 2 + 1), by admit /- proof elided -/
        ⟩ ⟨1, rfl⟩
    else 0

@[reducible]
def sumcheckFoldOracleReduction :=
  let stmt : Fin (ℓ / ϑ - 1 + 1) → Type :=
    fun i => Statement (L := L) (ℓ := ℓ) Context ⟨i * ϑ, blockIdx_mul_ϑ_lt_ℓ_succ i⟩
  let oStmt := fun i: Fin (ℓ / ϑ - 1 + 1) =>
    OracleStatement 𝔽q β ϑ ⟨i * ϑ, blockIdx_mul_ϑ_lt_ℓ_succ i⟩
  let wit := fun i: Fin (ℓ / ϑ - 1 + 1) =>
    Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (ℓ:=ℓ)
      ⟨i * ϑ, blockIdx_mul_ϑ_lt_ℓ_succ i⟩
  let nonLastBlocksOracleReduction :=
  OracleReduction.seqCompose (oSpec := []ₒ)
      (Stmt := stmt)
      (OStmt := oStmt) (Wit := wit)
      (pSpec := fun (bIdx: Fin (ℓ / ϑ - 1)) => pSpecFullNonLastBlock 𝔽q β bIdx)
      (R := fun bIdx => nonLastBlockOracleReduction (L:=L) 𝔽q β (ϑ:=ϑ) (𝓑:=𝓑) (bIdx:=bIdx))

def foldMatrix (i : Fin r) (steps : Fin (ℓ + 1)) (h_i_add_steps : i.val + steps < ℓ + 𝓡)
    (y : (sDomain 𝔽q β h_ℓ_add_R_rate)
      ⟨↑i + steps, by apply Nat.lt_trans (m := ℓ + 𝓡) (h_i_add_steps) h_ℓ_add_R_rate⟩)
    : Matrix (Fin (2 ^ steps.val)) (Fin (2 ^ steps.val)) L :=

structure ConcreteBTFStepResult (k : ℕ) extends (ConcreteBTFieldProps k) where
  instFintype : Fintype (ConcreteBTField k)
  fieldFintypeCard : Fintype.card (ConcreteBTField k) = 2^(2^k)
  
  sumZeroIffEq : ∀ (x y : ConcreteBTField k), x + y = 0 ↔ x = y
  traceMapEvalAtRootsIs1 :
    letI := mkFieldInstance (k:=k) (props:=toConcreteBTFieldProps)
    TraceMapProperty (ConcreteBTField k) (u:=Z k) k
  instIrreduciblePoly :
    letI := mkFieldInstance (k:=k) (props:=toConcreteBTFieldProps)
    (Irreducible (p := (definingPoly (s:=(Z k)))))

def Prover.liftContext
    (lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut
                        OuterWitIn OuterWitOut InnerWitIn InnerWitOut)
    (P : Prover oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec) :
      Prover oSpec OuterStmtIn OuterWitIn OuterStmtOut OuterWitOut pSpec where
  PrvState := fun i => P.PrvState i × OuterStmtIn × OuterWitIn
  input := fun ctxIn => ⟨P.input <| lens.proj ctxIn, ctxIn⟩
  sendMessage := fun i ⟨prvState, stmtIn, witIn⟩ => do
    let ⟨msg, prvState'⟩ ← P.sendMessage i prvState
    return ⟨msg, ⟨prvState', stmtIn, witIn⟩⟩
  receiveChallenge := fun i ⟨prvState, stmtIn, witIn⟩ => do
    let f ← P.receiveChallenge i prvState
    return fun chal => ⟨f chal, stmtIn, witIn⟩
  output := fun ⟨prvState, stmtIn, witIn⟩ => do
    let ⟨innerStmtOut, innerWitOut⟩ ← P.output prvState
    return lens.lift (stmtIn, witIn) (innerStmtOut, innerWitOut)

ratchetUnchecked : α → α

UInt64 in Init.Prelude

def relHammingBall (C : Code ι F) (y : ι → F) (r : ℝ) : Code ι F :=
  { c | c ∈ C ∧ Code.relHammingDist y c ≤ r }

hlistDecode : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1),
    listDecodable (C i j) (δ i) (dist i j)

noncomputable instance {H : F[X][Y]} : Ring (𝒪 H) :=
  Ideal.Quotient.ring (Ideal.span {H_tilde' H})

instance {pSpec : ProtocolSpec n} {Statement : Type}
    [DecidableEq Statement]
    [∀ i, DecidableEq (pSpec.Message i)]
    [∀ i, DecidableEq (pSpec.Challenge i)] :
    OracleSpec.DecidableEq (srChallengeOracle Statement pSpec) where
  domain_decidableEq' := fun i => by admit /- proof elided -/

inductive ScalarOp where | add | sub | mul | div

List.finRange in Init.Data.List.FinRange

Irreducible in Mathlib.Algebra.Group.Irreducible.Defs

instance instDCast₂OracleProver : DCast₂ Nat ProtocolSpec
    (fun _ pSpec => OracleProver oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec) where
  dcast₂ := OracleProver.cast
  dcast₂_id := OracleProver.cast_id

def take (j : Fin (n + 1)) (challenges : Challenges pSpec) : ChallengesUpTo j pSpec :=

Id.run in Init.Control.Id

instance [Zero T] [DecidableEq T] [ToNat T] : Div (Cayley T) where
  div := div

@[inline] def add (a b : AssocNat) : AssocNat :=
  ⟨a ∘ b, by admit /- proof elided -/
  ⟩

Polynomial.leadingCoeff in Mathlib.Algebra.Polynomial.Degree.Definitions

def ofMvPolynomialDeg1 (p : R⦃≤ 1⦄[X Fin n]) : MlPoly R n :=
  Vector.ofFn (fun i : Fin (2 ^ n) => p.val.coeff (monomialOfNat i))

def churchAnd (p q : ChurchBool α) : ChurchBool α :=
  fun x y => p (q x y) y

instance {α : Type} {s : Skeleton} :
    CoeFun (FullData α s) fun (_ : FullData α s) => SkeletonNodeIndex s → α where
  coe := fun tree idx => tree.get idx

def erase_even (s : Finset ℕ) : Finset ℕ := s.filter Odd

Function.Embedding.subtype in Mathlib.Logic.Embedding.Basic

randomOracle in VCVio.OracleComp.QueryTracking.CachingOracle

return none
</all_available_defs>

<all_available_lemmas>
Ne.dite_eq_left_iff in Mathlib.Logic.Basic
Nat.add_one_sub_one in Init.Data.Nat.Basic
Nat.left_eq_add in Init.Data.Nat.Lemmas
RingHom.comp_id in Mathlib.Algebra.Ring.Hom.Defs
cast_eq in Init.Core
eq_mp_eq_cast in Init.PropLemmas
one_ne_zero in Mathlib.Algebra.NeZero
Function.comp_apply in Init.Core
Polynomial.ext in Mathlib.Algebra.Polynomial.Basic
RingHom.coe_comp in Mathlib.Algebra.Ring.Hom.Defs
Nat.sub_add_cancel in Init.Data.Nat.Basic
Nat.sub_zero in Init.Data.Nat.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.shiftRight_zero in Init.Data.Nat.Bitwise.Basic
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.succ_eq_add_one in Init.Data.Nat.Basic
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
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
BitVec.toNat_ofNat in Init.Data.BitVec.Bootstrap
Nat.ofNat_pos in Mathlib.Data.Nat.Cast.Order.Ring
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
Nat.two_pow_pos in Init.Data.Nat.Basic
Prod.ext_iff in Init.Ext
MonoidHom.coe_mk in Mathlib.Algebra.Group.Hom.Defs
Nat.sub_one_add_one in Init.Data.Nat.Basic
OneHom.coe_mk in Mathlib.Algebra.Group.Hom.Defs
RingHom.coe_mk in Mathlib.Algebra.Ring.Hom.Defs
cast_cast in Init.PropLemmas
eqRec_eq_cast in Batteries.Logic
BitVec.extractLsb_ofNat in Init.Data.BitVec.Lemmas
BitVec.zero_eq in Init.Data.BitVec.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
RingEquiv.toEquiv_eq_coe in Mathlib.Algebra.Ring.Equiv
and_false in Init.SimpLemmas
Nat.add_zero in Init.Core

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

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

theorem one_le_sub_consecutive_two_pow (n : ℕ): 1 ≤ 2^(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_zero {k : ℕ} (h_pos : k > 0) :
  ⋘ 0, 0 ⋙ = 0

lemma algebraMap_eq_zero_x {i j : ℕ} (h_le : i < j) (x : BTField i) :
    letI instAlgebra

lemma algebraMap_succ_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : BTField (k - 1)) :
  letI instAlgebra

lemma split_algebraMap_eq_zero_x {k : ℕ} (h_pos : k > 0) (x : BTField (k - 1)) :
  letI instAlgebra

lemma towerAlgebraMap_succ_1 (k : ℕ) :
  towerAlgebraMap (l:=k) (r:=k+1) (h_le:=by omega) = canonicalEmbedding k

lemma towerAlgebraMap_id (k : ℕ) : towerAlgebraMap (h_le:=by omega) = RingHom.id (BTField k)

theorem eq_join_via_add_smul_eq_iff_split (k : ℕ) (h_pos : k > 0)
    (x : BTField k) (hi_btf lo_btf : BTField (k - 1)) :
    x = ⋘ hi_btf, lo_btf ⋙ ↔
  split (k:=k) (h_k:=h_pos) x = (hi_btf, lo_btf)

theorem unique_linear_decomposition_succ (k : ℕ) :
  ∀ (x : BTField (k+1)), ∃! (p : BTField k × BTField k),
    x = ⋘ p.1, p.2 ⋙

lemma algebraMap_adjacent_tower_succ_eq_Adjoin_of (k : ℕ) :
  (algebraMap (BTField k) (BTField (k + 1))) = of (poly k)

lemma algebraMap_adjacent_tower_def (l : ℕ) :
  (algebraMap (BTField l) (BTField (l + 1))) = canonicalEmbedding l

lemma binaryTowerAlgebra_def (l r : ℕ) (h_le : l ≤ r) :
    @binaryAlgebraTower (l:=l) (r:=r) (h_le:=h_le)
    = (towerAlgebraMap l r h_le).toAlgebra

lemma poly_natDegree_eq_2 (k : ℕ) : (poly (k:=k)).natDegree = 2

lemma BTField.cast_BTField_eq (k m : ℕ) (h_eq : k = m) :
  BTField k = BTField m

@[simp]
theorem BTField.RingHom_cast_dest_apply (k m n : ℕ) (h_eq : m = n)
  (f : BTField k →+* BTField m) (x : BTField k) :
    (cast (BTField.RingHom_eq_of_dest_eq (k:=k) (m:=m) (n:=n) h_eq) f) x
    = cast (by apply cast_BTField_eq (h_eq:=h_eq)) (f x)

@[simp]
theorem BTField.RingHom_eq_of_dest_eq (k m n : ℕ) (h_eq : m = n) :
  (BTField k →+* BTField m) = (BTField k →+* BTField n)

lemma towerAlgebraMap_succ (l r : ℕ) (h_le : l ≤ r) :
  towerAlgebraMap (l:=l) (r:=r+1) (h_le:=by omega) =
  (towerAlgebraMap (l:=r) (r:=r+1) (h_le:=by omega)).comp
  (towerAlgebraMap (l:=l) (r:=r) (h_le:=by omega))

lemma join_eq_join_iff (k : ℕ) (h_pos : k > 0) (hi₁ hi₀ lo₁ lo₀ : BTField (k - 1)) :
    ⋘ hi₁, lo₁ ⋙ = ⋘ hi₀, lo₀ ⋙ ↔
  hi₁ = hi₀ ∧ lo₁ = lo₀

lemma split_join_via_add_smul_eq_iff_split (k : ℕ) (h_pos : k > 0)
    (hi_btf lo_btf : BTField (k - 1)) :
    split (k:=k) (h_k:=h_pos) (⋘ hi_btf, lo_btf ⋙) = (hi_btf, lo_btf)

lemma pow_2_pow_i_mem_Di_of_mem_D {F : Type} [NonBinaryField F] [Finite F] {D : Subgroup Fˣ}
  [DIsCyclicC : IsCyclicWithGen ↥D] {x : Fˣ} :
  ∀ {a : Fˣ} (i : ℕ),
    a ∈ evalDomain D x 0 → a ^ (2 ^ i) ∈ evalDomain D x i

Fin.coe_castSucc in Init.Data.Fin.Lemmas

lemma mem_support_coeff_finSuccEquivNth {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x} :
    x ∈ ((finSuccEquivNth R p f).coeff i).support ↔ x.insertNth p i ∈ f.support

theorem rename_ne_zero_of_injective {τ : Type*} {f : σ → τ} (hf : Function.Injective f)
    {p : MvPolynomial σ R} (h : p ≠ 0) : rename f p ≠ 0

@[simp]
theorem fflatten_embedSum {A : Sort u} {F : A → Sort v} {m : ℕ} {n : Fin m → ℕ}
    {α : (i : Fin m) → (j : Fin (n i)) → A}
    (v : (i : Fin m) → (j : Fin (n i)) → F (α i j)) (i : Fin m) (j : Fin (n i)) :
    fflatten v (embedSum i j) = cast (by simp) (v i j)

@[simp]
theorem insertNth_zero_zero : insertNth p 0 (0 : Fin n →₀ M) = 0

lemma out_of_dom_smpl_2
  {δ l : ℝ≥0} {s : ℕ} {f : ι → F} {degree : ℕ} {φ : ι ↪ F}
  (C : Set (ι → F)) (hC : C = code φ degree)
  (h_decodable : listDecodable C δ l)
  (h_nonempty : Nonempty (domainComplement φ)) :
  listDecodingCollisionProbability φ f δ s degree h_nonempty ≤
    ((l^2 / 2)) * (degree / (Fintype.card F - Fintype.card ι))^s

lemma toImpl_toPoly_of_canonical [LawfulBEq R] (p : UniPolyC R) : p.toPoly.toImpl = p

@[simp]
lemma natDegree_solutionToE :
  (solutionToE e k v).natDegree = e

@[simp]
private lemma oddPart'_coeff {f : Polynomial F} {n : ℕ} :
    (oddPart' f).coeff n = if Even n then f.coeff (n + 1) else 0

@[simp]
theorem LeafData.get_ofRight {s_left s_right : Skeleton} {α : Type}
    (tree : LeafData α (Skeleton.internal s_left s_right))
    (idxRight : SkeletonLeafIndex s_right) :
    tree.get (SkeletonLeafIndex.ofRight idxRight) =
      tree.rightSubtree.get idxRight

@[simp]
lemma addSalt_dir : (pSpec.addSalt Salt).dir = pSpec.dir

lemma getBit_of_lt_two_pow {n: ℕ} (a: Fin (2^n)) (k: ℕ) :
  getBit k a = if k < n then getBit k a else 0

@[simp]
theorem LeafData.optionComposeBuild_leaf {α} (a : α)
    (compose : α → α → Option α) :
    (LeafData.leaf a).optionComposeBuild compose = FullData.leaf (.some a)

theorem hcons_injective2 {α : Sort u} {β : Fin n → Sort u} :
    Function.Injective2 (@hcons n α β)

@[simp]
lemma Rhs_add_one : Rhs (e + 1) ωs f = fun i ↦ Rhs e ωs f i * ωs i

@[simp]
lemma dfoldlM'_zero {α : Fin 1 → Type u} (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x : α 0) :
    dfoldlM' 0 α f x = pure x

lemma combine_eq_cases {F ι : Type*} [Field F] [DecidableEq F]
  (φ : ι ↪ F) (dstar : ℕ) (r : F) (fs : Fin m → ι → F) (degs : Fin m → ℕ)
    (hdegs : ∀ i, degs i ≤ dstar) (φ_neq_0 : ∀ i, φ i ≠ 0) :
  combine φ dstar r fs degs =
    fun x =>
      let q := φ x * r
      if q ≠ 1
      then ∑ i, (ri dstar degs r i) * (fs i x) * (1 - q^(dstar - degs i + 1)) / (1 - q)
      else ∑ i, (ri dstar degs r i) * (fs i x) *  (dstar - degs i + 1)

@[simp]
lemma Basis.baseChangeRight_apply (b : Basis ι K Left) (i : ι) :
    (Basis.baseChangeRight (b:=b) (Right:=Right)) i = b i ⊗ₜ[K] 1

lemma sDomain_card (i : Fin r) (h_i : i < ℓ + R_rate) :
    Fintype.card (sDomain 𝔽q β h_ℓ_add_R_rate i) = (Fintype.card 𝔽q)^(ℓ + R_rate - i)

@[simp]
theorem perfectCompleteness_eq_prob_one :
    reduction.perfectCompleteness init impl relIn relOut ↔
      ∀ stmtIn witIn, (stmtIn, witIn) ∈ relIn →
        [fun ⟨⟨_, (prvStmtOut, witOut)⟩, stmtOut⟩ =>
          (stmtOut, witOut) ∈ relOut ∧ prvStmtOut = stmtOut
        | do (simulateQ (impl ++ₛₒ challengeQueryImpl : QueryImpl _ (StateT σ ProbComp))
            <| reduction.run stmtIn witIn).run' (← init)] = 1

@[simp]
theorem append_cast_right {n m : ℕ} (pSpec : ProtocolSpec n) (pSpec' : ProtocolSpec m) (m' : ℕ)
    (h : n + m = n + m') :
      dcast h (pSpec ++ₚ pSpec') = pSpec ++ₚ (dcast (Nat.add_left_cancel h) pSpec')

theorem challengeOracleInterface_cast {h : n₁ = n₂} {hSpec : pSpec₁.cast h = pSpec₂}
    {i : pSpec₁.ChallengeIdx} :
    pSpec₁.challengeOracleInterface i =
      dcast (by simp) (pSpec₂.challengeOracleInterface (i.cast hn hSpec))

theorem succ_eq_one_add (n : ChurchNat α) : succ n = add one n

@[simp]
theorem drop_drop {m m' : ℕ} (h : m ≤ n - m') (h' : m' ≤ n) (v : (i : Fin n) → α i) :
    drop m h (drop m' h' v) =
      (fun i =>
        letI := drop (m + m') (Nat.add_le_of_le_sub h' h) v (i.cast (by omega))
        dcast (by simp [Fin.cast, add_assoc]) this)

@[simp]
private lemma leadingCoeff_E : (E ωs f p e).leadingCoeff = 1

lemma natDeg_sum_eq_of_unique {α : Type} {s : Finset α} {f : α → F[X]} {deg : ℕ}
  (mx : α) (h : mx ∈ s) :
    (f mx).natDegree = deg →
    (∀ y ∈ s, y ≠ mx → (f y).natDegree < deg ∨ f y = 0) →
    (∑ x ∈ s, f x).natDegree = deg

lemma getBit_of_middleBits {n offset len k : ℕ} :
  getBit k (getMiddleBits offset len n) =
    if k < len then getBit (k + offset) n else 0

lemma dappend_right_of_not_lt {motive : Fin (m + n) → Sort u}
    (u : (i : Fin m) → motive (castAdd n i)) (v : (i : Fin n) → motive (natAdd m i))
    (i : Fin (m + n)) (h : ¬ i.val < m) :
      dappend (motive := motive) u v i = dcast (by ext; simp; omega) (v ⟨i - m, by omega⟩)

lemma concrete_mul_zero0 (a : ConcreteBTField 0) :
  concrete_mul a (zero (k:=0)) = zero (k:=0)

lemma folding_steps_pos : (ϑ : ℕ) > 0

lemma W_monic (i : Fin r) : (W 𝔽q β i).Monic

omit [NeZero ℓ] [NeZero r] [NeZero 𝓡] in
lemma fin_ℓ_lt_r {h_ℓ_add_R_rate : ℓ + 𝓡 < r} (i : Fin ℓ)
    : i.val < r

@[simp]
lemma evalDist_cast (h : α = β) [spec.FiniteRange] :
    evalDist (cast (congrArg (OracleComp spec) h) oa) =
      cast (congrArg (PMF ∘ Option) h) (evalDist oa)

@[simp]
theorem fflatten_succ {A : Sort u} {F : A → Sort v} {m : ℕ} {n : Fin (m + 1) → ℕ}
    {α : (i : Fin (m + 1)) → (j : Fin (n i)) → A}
    {v : (i : Fin (m + 1)) → (j : Fin (n i)) → F (α i j)} :
    fflatten v = fappend (v 0) (fflatten (fun i => v i.succ))

omit [SelectableType R] in
@[simp]
lemma reduction_verifier_eq_verifier {i : Fin n} :
    (reduction R n deg D oSpec i).verifier = verifier R n deg D oSpec i

theorem singleton_happend {β : Fin n → Sort u} (a : α) (v : (i : Fin n) → β i) :
    True

theorem hcons_eq_cons {β : Fin n → Sort u} (a : α) (v : (i : Fin n) → β i) :
    hcons a v = cons (α := vcons α β) (hcons a v 0) (fun i => hcons a v i.succ)

@[simp]
lemma challengeOracleInterface_append_domain_inr (j : pSpec₂.ChallengeIdx) :
    [(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ.domain (.inr j) = Unit

theorem nsmul_raw_succ (n : ℕ) (p : UniPoly Q) :
  nsmul_raw (n + 1) p = add_raw (nsmul_raw n p) p

lemma runWithOracle_buildMerkleTree {s} (leaf_data_tree : LeafData α s) (f) :
    (runWithOracle f (buildMerkleTree leaf_data_tree))
    = buildMerkleTree_with_hash leaf_data_tree fun (left right : α) =>
      (f () ⟨left, right⟩)

lemma schwartz_zippel' {p : MvPolynomial σ R} (hp : p ≠ 0) (S : σ → Finset R) :
    #{x ∈ Finset.pi p.vars S | eval (extendDomain x) p = 0} / ∏ i ∈ p.vars, (#(S i) : ℚ≥0)
      ≤ ∑ i ∈ p.vars, (p.degreeOf i / #(S i) : ℚ≥0)

lemma rank_eq_iff_det_ne_zero {U : Matrix (Fin n) (Fin n) F} :
U.rank = n ↔ U.det ≠ 0

lemma AlgebraTowerEquiv.commutesRight' (e : AlgebraTowerEquiv A B)
    {i j : ι} (h : i ≤ j) (r : B i) :
  AlgebraTower.algebraMap (AT:=A) (i:=i) (j:=j) (h:=h) ((e.toRingEquiv i).symm r) =
  (e.toRingEquiv j).symm (AlgebraTower.algebraMap (AT:=B) (i:=i) (j:=j) (h:=h) r)

@[simp]
theorem Fin.cast_val_eq_val {n m : ℕ} [NeZero n] (a : Fin n) (h_eq : n = m):
  (Fin.cast (h_eq) a).val = a.val

@[simp]
protected lemma elocPoly_two :
  ElocPoly 2 ωs f p =
  if f 1 = eval (ωs 1) p
  then if f 0 = eval (ωs 0) p then 1
       else X - C (ωs 0)
  else if f 0 = eval (ωs 0) p then X - C (ωs 1)
       else (X - C (ωs 0)) * (X - C (ωs 1))

theorem non_zero_map [LawfulBEq R] (f : R → R) (hf : ∀ r, f r = 0 → r = 0) (p : UniPoly R) :
  let fp := UniPoly.mk (p.map f);
  p.trim = p → fp.trim = fp

@[simp]
theorem cast_toReduction
    (R : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec₁) :
    (R.cast hn hSpec hOₘ).toReduction = Reduction.cast hn hSpec R.toReduction

@[simp]
theorem fconcat₂_last {α₁ : Fin n → A} {α₂ : Fin n → B} {β₁ : A} {β₂ : B}
    (v : (i : Fin n) → F₂ (α₁ i) (α₂ i)) (a : F₂ β₁ β₂) :
    fconcat₂ (F := F₂) v a (last n) = cast (by simp [vconcat_last]) a

theorem coreInteractionOracleReduction_perfectCompleteness (hInit : init.neverFails) :
    OracleReduction.perfectCompleteness
      (pSpec := pSpecCoreInteraction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate))
      (relIn := roundRelation (mp := BBF_SumcheckMultiplierParam) 𝔽q β (ϑ:=ϑ)
        (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (𝓑:=𝓑) 0)
      (relOut := finalSumcheckRelOut 𝔽q β (ϑ:=ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate))
      (oracleReduction := coreInteractionOracleReduction 𝔽q β (ϑ:=ϑ) (𝓑:=𝓑))
      (init := init)
      (impl := impl)

List.length_drop in Init.Data.List.TakeDrop

theorem dcast₂_symm (ha : a = a') (hb : dcast ha b = b') (hc : dcast₂ ha hb c = c') :
    dcast₂ ha.symm (dcast_symm ha hb) c' = c

theorem vappend_succ (u : Fin m → α) (v : Fin (n + 1) → α) :
    vappend u v = vconcat (vappend u (v ∘ castSucc)) (v (last n))

theorem linsolve_none {A : Matrix (Fin n) (Fin m) F} {b : Fin n → F}
  (h : linsolve A b = none)
  : ¬∃ x, A.mulVec x = b

@[simp]
lemma dfoldl'_succ_last {n : ℕ} {α : Fin (n + 2) → Type u}
    (f : (i : Fin (n + 1)) → α i.castSucc → α i.succ) (x : α 0) :
    dfoldl' (n + 1) α f x = f (last n) (dfoldl' n (α ∘ castSucc) (fun i => f i.castSucc) x)

lemma last_nonzero_unique {p : UniPoly Q} {k k' : Fin p.size} :
  last_nonzero_prop k → last_nonzero_prop k' → k = k'

lemma twoAdicGenerators_order (bits : Fin (twoAdicity + 1)) :
    orderOf (twoAdicGenerators[bits]) = 2 ^ (bits : Nat)

Nat.lt_trans in Init.Prelude
</all_available_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 add {k : ℕ} (x y : ConcreteBTField k) : ConcreteBTField k := BitVec.xor x y

def neg {k : ℕ} (x : ConcreteBTField k) : ConcreteBTField k := x

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 :=

structure ConcreteBTFAddCommGroupProps (k : ℕ) where
  add_assoc : ∀ a b c : ConcreteBTField k, (a + b) + c = a + (b + c) := add_assoc
  add_comm : ∀ a b : ConcreteBTField k, a + b = b + a := add_comm
  add_zero : ∀ a : ConcreteBTField k, a + zero = a := add_zero
  zero_add : ∀ a : ConcreteBTField k, zero + a = a := zero_add
  add_neg : ∀ a : ConcreteBTField k, a + (neg a) = zero := neg_add_cancel

def mkAddCommGroupInstance {k : ℕ} : AddCommGroup (ConcreteBTField k) := {
  zero := zero
  neg := neg
  sub := fun x y => add x y
  add_assoc := add_assoc
  add_comm := add_comm
  zero_add := zero_add
  add_zero := add_zero
  nsmul := fun n x => if n % 2 = (0 : ℕ) then zero else x
  zsmul := fun (n : ℤ) x => if n % 2 = 0 then zero else x  
  neg_add_cancel := neg_add_cancel
  nsmul_succ := nsmul_succ
  zsmul_succ' := fun n a => zsmul_succ n a
  add := add
  zsmul_neg' := zsmul_neg' (k := k)
}

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

def equivProd {k : ℕ} (h_k_pos : k > 0) :
  ConcreteBTField k ≃ ConcreteBTField (k - 1) × ConcreteBTField (k - 1) where
  toFun := split h_k_pos
  invFun := fun (hi, lo) => 《 hi, lo 》
  left_inv := fun x => Eq.symm (join_of_split h_k_pos x _ _ rfl)
  right_inv := fun ⟨hi, lo⟩ => Eq.symm (split_of_join h_k_pos _ hi lo rfl)

def concrete_mul {k : ℕ} (a b : ConcreteBTField k) : ConcreteBTField k :=
  if h_k_zero : k = 0 then
    if a = zero then zero
    else if b = zero then zero
    else if a = one then b
    else if b = one then a
    else zero 
  else
    have h_k_gt_0 : k > 0 := by admit /- proof elided -/

def concrete_inv {k : ℕ} (a : ConcreteBTField k) : ConcreteBTField k :=
  if h_k_zero : k = 0 then
    if a = 0 then 0 else 1
  else
    if h_a_zero : a = 0 then 0
    else if h_a_one : a = 1 then 1
    else
      let h_k_gt_0 : k > 0 := Nat.zero_lt_of_ne_zero h_k_zero
      let (a_hi, a_lo) := split (k:=k) (h:=h_k_gt_0) a
      let prevZ := Z (k - 1)
      let a_lo_next := a_lo + concrete_mul a_hi prevZ
      let delta := concrete_mul a_lo a_lo_next + concrete_mul a_hi a_hi
      let delta_inverse := concrete_inv delta
      let out_hi := concrete_mul delta_inverse a_hi
      let out_lo := concrete_mul delta_inverse a_lo_next
      let res := 《 out_hi, out_lo 》
      res

section FieldLemmasOfLevel0

end FieldLemmasOfLevel0

section NumericCasting

def natCast {k : ℕ} (n : ℕ) : ConcreteBTField k := if n % 2 = 0 then zero else one

def natCast_zero {k : ℕ} : natCast (k:=k) 0 = zero :=

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

def intCast {k : ℕ} (n : ℤ) : ConcreteBTField k := if n % 2 = 0 then zero else one

def intCast_ofNat {k : ℕ} (n : ℕ) : intCast (k:=k) (n : ℤ) = natCast n :=

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

end NumericCasting

structure ConcreteBTFRingProps (k : ℕ) extends (ConcreteBTFAddCommGroupProps k) where
  
  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 =
      《 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 ConcreteBTFDivisionRingProps (k : ℕ) extends (ConcreteBTFRingProps k) where
  
  mul_inv_cancel : ∀ a : ConcreteBTField k, a ≠ zero → concrete_mul a (concrete_inv a) = one

structure ConcreteBTFieldProps (k : ℕ) extends (ConcreteBTFDivisionRingProps k) where
  
  mul_comm : ∀ a b : ConcreteBTField k, concrete_mul a b = concrete_mul b a

def mkRingInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Ring (ConcreteBTField k) where
  toAddCommGroup := mkAddCommGroupInstance
  toOne := inferInstance
  mul := concrete_mul
  mul_assoc := props.mul_assoc
  one_mul := props.one_mul
  mul_one := props.mul_one
  left_distrib := props.mul_left_distrib
  right_distrib := props.mul_right_distrib
  zero_mul := props.zero_mul
  mul_zero := props.mul_zero

  natCast n := natCast n
  natCast_zero := natCast_zero
  natCast_succ n := natCast_succ n
  intCast n := intCast n
  intCast_ofNat n := intCast_ofNat n
  intCast_negSucc n := intCast_negSucc n

def mkDivisionRingInstance {k : ℕ} (props : ConcreteBTFieldProps k)
    : DivisionRing (ConcreteBTField k) where
  toRing := mkRingInstance (k:=k) props
  inv := concrete_inv
  exists_pair_ne := concrete_exists_pair_ne (k := k)
  mul_inv_cancel := props.mul_inv_cancel
  inv_zero := concrete_inv_zero
  qsmul := (Rat.castRec · * ·)
  nnqsmul := (NNRat.castRec · * ·)

def mkFieldInstance {k : ℕ} (props : ConcreteBTFieldProps k) : Field (ConcreteBTField k) where
  toDivisionRing := mkDivisionRingInstance (k:=k) props
  mul_comm := props.mul_comm

structure ConcreteBTFStepResult (k : ℕ) extends (ConcreteBTFieldProps k) where
  instFintype : Fintype (ConcreteBTField k)
  fieldFintypeCard : Fintype.card (ConcreteBTField k) = 2^(2^k)
  
  sumZeroIffEq : ∀ (x y : ConcreteBTField k), x + y = 0 ↔ x = y
  traceMapEvalAtRootsIs1 :
    letI := mkFieldInstance (k:=k) (props:=toConcreteBTFieldProps)
    TraceMapProperty (ConcreteBTField k) (u:=Z k) k
  instIrreduciblePoly :
    letI := mkFieldInstance (k:=k) (props:=toConcreteBTFieldProps)
    (Irreducible (p := (definingPoly (s:=(Z k)))))

end FieldOperationsAndInstances

section BTFieldPropsOneLevelLiftingLemmas

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

end BTFieldPropsOneLevelLiftingLemmas

section TowerFieldsConstruction

def liftBTFieldProps (k : ℕ) (prevBTFResult : ConcreteBTFStepResult (k := k)) :
  ConcreteBTFieldProps (k + 1) := {
    zero_mul := concrete_zero_mul (prevBTFResult.toConcreteBTFieldProps),
    zero_mul' := fun a => by admit /- proof elided -/

def liftConcreteBTField (k : ℕ) (prevBTFResult : ConcreteBTFStepResult (k := k)) :
  Field (ConcreteBTField (k + 1)) :=

def concreteCanonicalEmbedding (k : ℕ)
    (prevBTFieldProps : ConcreteBTFieldProps (k := (k)))
    (curBTFieldProps : ConcreteBTFieldProps (k := (k + 1))) :
  letI := mkFieldInstance prevBTFieldProps
  letI := mkFieldInstance curBTFieldProps
  ConcreteBTField k →+* ConcreteBTField (k + 1) :=

instance instAlgebraLiftConcreteBTField (k : ℕ)
  (prevBTFResult : ConcreteBTFStepResult (k := k)) :
  letI := mkFieldInstance (prevBTFResult.toConcreteBTFieldProps)
  letI := liftConcreteBTField (k:=k) prevBTFResult
  Algebra (ConcreteBTField k) (ConcreteBTField (k + 1)) :=
  letI := mkFieldInstance (prevBTFResult.toConcreteBTFieldProps)
  letI := liftConcreteBTField (k:=k) prevBTFResult
  RingHom.toAlgebra (R:=ConcreteBTField k) (S:=ConcreteBTField (k + 1))
    (i:=(concreteCanonicalEmbedding (k:=k)
      (prevBTFieldProps:=prevBTFResult.toConcreteBTFieldProps)
      (curBTFieldProps:=liftBTFieldProps (k:=k) (prevBTFResult:=prevBTFResult))))

def getBTFResult (k : ℕ) : ConcreteBTFStepResult k :=
  match k with
  | 0 =>
    let base : ConcreteBTFieldProps 0 := {
      mul_eq := fun a b h_k _ _ _ _ _ _ => by admit /- proof elided -/
| c1_one
        · 
          rw [c1_zero] at h_mul
          
          simp at h_mul
        · 
          rcases c2_cases with c2_zero | c2_one
          · 
            rw [c2_zero] at h_mul
            
            simp at h_mul
          · 
            
            exact ⟨c1_one, c2_one⟩
      
      have specialElement_eq_zero : specialElement = 0 := by admit /- proof elided -/

end TowerFieldsConstruction

section ConcreteBTFieldAlgebraConstruction

def canonicalAlgMap (k : ℕ) := concreteCanonicalEmbedding (k:=k)
  (prevBTFieldProps:= ((getBTFResult k).toConcreteBTFieldProps))
  (curBTFieldProps:= ((getBTFResult (k + 1)).toConcreteBTFieldProps))

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

instance instAlgebraTowerConcreteBTF : AlgebraTower (ConcreteBTField) where
  algebraMap := concreteTowerAlgebraMap
  commutes' := by admit /- proof elided -/

def ConcreteBTFieldAlgebra {l r : ℕ} (h_le : l ≤ r) :
    Algebra (ConcreteBTField l) (ConcreteBTField r) := instAlgebraTowerConcreteBTF.toAlgebra h_le

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

end ConcreteBTFieldAlgebraConstruction

noncomputable section ConcreteMultilinearBasis

open Module

def basisSucc (k : ℕ) : Basis (Fin 2) (ConcreteBTField k) (ConcreteBTField (k + 1)) :=

def powerBasisSucc (k : ℕ) :
    PowerBasis (ConcreteBTField k) (ConcreteBTField (k + 1)) :=

end ConcreteMultilinearBasis

section TowerEquivalence

open BinaryTower

noncomputable def towerEquiv_zero : RingEquiv (R:=GF(2)) (S:=ConcreteBTField 0) :=  {
  toFun := fun x => if x = 0 then 0 else 1,
  invFun := fun x => if x = 0 then 0 else 1,
  left_inv := fun x => by admit /- proof elided -/

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

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

noncomputable def towerRingHomForwardMap (k : ℕ) : ConcreteBTField k → BTField k :=

noncomputable def towerRingHomBackwardMap (k : ℕ) : BTField k → ConcreteBTField k :=

structure TowerEquivResult (k : ℕ) where
  ringEquiv : ConcreteBTField k ≃+* BTField k
  ringEquivForwardMapEq : ringEquiv = towerRingHomForwardMap k

noncomputable def towerEquiv (n : ℕ) : TowerEquivResult n :=
</local_ctx>

<target_theorem>
lemma towerEquiv_commutes_left_diff (i d : ℕ) : ∀ r : ConcreteBTField i,
  (AlgebraTower.algebraMap i (i+d) (by omega)) ((towerEquiv i).ringEquiv r) =
  (towerEquiv (i+d)).ringEquiv ((AlgebraTower.algebraMap i (i+d) (by omega)) r) :=
</target_theorem>

