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

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

def pSpecFoldRelaySequence (n : ℕ) :=
  ProtocolSpec.seqCompose fun (_: Fin n) ↦ pSpecFoldRelay (L:=L)

def SkeletonNodeIndex.isRoot {s : Skeleton} (idx : SkeletonNodeIndex s) : Bool :=
  match idx with
  | SkeletonNodeIndex.ofLeaf => true
  | SkeletonNodeIndex.ofInternal => true
  | SkeletonNodeIndex.ofLeft _ => false
  | SkeletonNodeIndex.ofRight _ => false

@[reducible, simp]
def ChallengeIdxUpTo (k : Fin (n + 1)) (pSpec : ProtocolSpec n) : Type :=
  (pSpec⟦:k.val⟧).ChallengeIdx

@[inline, specialize]
def oracleProver : OracleProver oSpec
    Statement OStatement Unit Statement OStatement Unit !p[] where
  PrvState := fun _ => Statement × (∀ i, OStatement i)
  input := Prod.fst
  sendMessage := fun i => nomatch i
  receiveChallenge := fun i => nomatch i
  output := fun stmt => pure (stmt, ())

structure FinalSumcheckStatementOut extends
  Statement (L := L) (Context := SumcheckBaseContext L ℓ) (Fin.last ℓ) where
  final_constant : L

protected def cast (pSpec : ProtocolSpec n₁) : ProtocolSpec n₂ :=
  ⟨pSpec.dir ∘ (Fin.cast hn.symm), pSpec.«Type» ∘ (Fin.cast hn.symm)⟩

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

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

def FullData.Equiv {α} (s : Skeleton) :
    FullData α s ≃ InternalData α s × LeafData α s :=

def modByMonic [Field R] (p : UniPoly R) (q : UniPoly R) :
    UniPoly R :=
  (divModByMonicAux p q).2

def modNat [Zero T] [DecidableEq T] [ToNat T]
    (dividend divisor : Cayley T) : Nat → Cayley T
  | 0        => dividend  
  | .succ fuel =>
    
    if (↑divisor : Nat) = 0 then
      dividend
    else
      
      if (↑divisor : Nat) ≤ (↑dividend : Nat) then
        
        modNat (sub dividend divisor) divisor fuel
      else
        dividend

@[simp]
instance BTFieldNoZeroDiv (k : ℕ) : NoZeroDivisors (BTField k) :=

abbrev ScalarField := ZMod scalarFieldSize

def commitKnowledgeError {i : Fin ℓ}
    (m : (pSpecCommit 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i).ChallengeIdx) : ℝ≥0 :=
  match m with
  | ⟨j, hj⟩ => by admit /- proof elided -/

@[reducible]
def permutationOracle (α : Type*) : OracleSpec PermuteDir :=
  forwardPermutationOracle α ++ₒ backwardPermutationOracle α

instance : SpongeUnit UInt8 where

EquivLike in Mathlib.Data.FunLike.Equiv

proj_sound : ∀ outerStmtIn,
    outerStmtIn ∉ outerLangIn → lens.proj outerStmtIn ∉ innerLangIn

List.replicate in Init.Data.List.Basic

def IterType (n : ℕ) : Type := dfoldl' n (fun _ => Type) (fun _ T => T × T) Nat

Fin.foldl in Init.Data.Fin.Fold

Finset.Ico in Mathlib.Order.Interval.Finset.Defs

BitVec.append in Init.Data.BitVec.Basic

def implGroupExpOracle : QueryImpl (GroupExpOracle ι p) (StateT (GroupValTable ι G) Option) where
  impl | query _ ⟨i, a, j⟩ => fun table =>
    match table i with
    | some g => some ((), table.update j (some (g ^ a.val)))
    | none => none

noncomputable def J (q δ : ℚ) : ℝ :=
  let frac := q / (q - 1)
  (1 / frac) * (1 - Real.sqrt (1 - frac * δ))

Polynomial.coeff in Mathlib.Algebra.Polynomial.Basic

example : NestedList 0 = Nat := rfl
example (n : ℕ) : NestedList (n + 1) = List (NestedList n) := rfl

List.getLast in Init.Data.List.Basic

GroupWithZero in Mathlib.Algebra.GroupWithZero.Defs

structure DuplexSponge (U : Type) [SpongeUnit U] [SpongeSize] (C : Type*)
    [SpongeState U C] where
   
  state : C
   
  absorbPos : Fin (SpongeSize.R + 1)
   
  squeezePos : Fin (SpongeSize.R + 1)
deriving Inhabited

Polynomial.charP in Mathlib.Algebra.Polynomial.Coeff

def minDist [DecidableEq F] (IC : MatrixSubmodule κ ι F) : ℕ :=
  sInf { d : ℕ | ∃ U ∈ IC, ∃ V ∈ IC, distCodewords U V = d }

class Statement.Lens.IsSound {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
    (outerLangIn : Set OuterStmtIn) (outerLangOut : Set OuterStmtOut)
    (innerLangIn : Set InnerStmtIn) (innerLangOut : Set InnerStmtOut)
    (compatStmt : OuterStmtIn → InnerStmtOut → Prop)
    (lens : Statement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut) where

Field.toCommRing in Mathlib.Algebra.Field.Defs

sendMessage 
  | ⟨0, _⟩ => fun ⟨stmt, oStmt, wit⟩ => do
    let curH : ↥L⦃≤ 2⦄[X Fin (ℓ - ↑i.castSucc)] := wit.H
    let h_i : L⦃≤ 2⦄[X] := by admit /- proof elided -/

instance [Zero T] [ToNat T] : LT (Cayley T) where
  lt := lt

def vflatten {m : ℕ} {n : Fin m → ℕ} (v : (i : Fin m) → Fin (n i) → α) :
    Fin (vsum n) → α :=
  dflatten v

Fin.append in Mathlib.Data.Fin.Tuple.Basic

@[reducible, inline]
instance instMvPolynomialDegreeLE : OracleInterface (R⦃≤ d⦄[X σ]) where
  Query := σ → R
  Response := R
  answer := fun ⟨poly, _⟩ point => eval point poly

List.drop in Init.Data.List.Basic

let stmtOut : FinalSumcheckStatementOut (L := L) (ℓ := ℓ) := {
      ctx := stmt.ctx,
      sumcheck_target := stmt.sumcheck_target,
      challenges := stmt.challenges,
      final_constant := c
    }

Polynomial.degree in Mathlib.Algebra.Polynomial.Degree.Definitions

def concat' {k : Fin n}
    (challenges : (i : Fin k) → (pSpec.dir (i.castLE (by admit /- proof elided -/
    )) = .V_to_P
      → pSpec.«Type» (i.castLE (by admit /- proof elided -/
      ))))
    (chal : (h : pSpec.dir k = .V_to_P) → pSpec.Challenge ⟨k, h⟩) :
    (i : Fin (k + 1)) → (pSpec.dir (i.castLE (by admit /- proof elided -/
    )) = .V_to_P) →
      pSpec.«Type» (i.castLE (by admit /- proof elided -/
      )) :=
  Fin.dconcat challenges chal

instance : DeserializeOption UInt8 ByteArray where
  deserialize bytes :=
    if h : bytes.size = 1 then
      some bytes[0]
    else
      none

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

instance instSelectableTypeChallengePSpec [SelectableType R] :
    ∀ i, SelectableType ((pSpec R deg).Challenge i) :=
  instSelectableTypeChallengeAppend

class PrimeOrderWith (G : Type*) [Group G] (p : outParam ℕ) [Fact (Nat.Prime p)] where
  hCard : Nat.card G = p

def Fin.traverseM {β : Fin n → Type u}
    (f : (i : Fin n) → m (β i)) : m ((i : Fin n) → β i) :=
  let rec aux (k : ℕ) (h : k ≤ n) : m ((i : Fin k) → β (Fin.castLE h i)) :=
    match k with
    | 0 => pure (fun i => i.elim0)
    | k' + 1 => do
      let tail ← aux k' (Nat.le_of_succ_le h)
      let head ← f (Fin.castLE h (Fin.last k'))
      return (Fin.snoc tail head)
  aux n (le_refl n)

def map (f : R →+* S) (p : MlPolyEval R n) : MlPolyEval S n :=
  Vector.map (fun a => f a) p

def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
  let style : ErrorFormat := match args.hasFlag "github" with
    | true => ErrorFormat.github
    | false => ErrorFormat.humanReadable
  let fix := args.hasFlag "fix"
  
  let mut allModuleNames := #[]
  for s in ["ArkLib.lean"] do
    allModuleNames := allModuleNames.append (← findImports s)
  
  allModuleNames := allModuleNames.erase `Batteries
  let mut numberErrors ← lintModules allModuleNames style fix
  if ← checkInitImports then numberErrors := numberErrors + 1
  
  
  
  
  if args.hasFlag "fix" then
    return 0
  else return min numberErrors 125

def findFinIdxIfTrue (p : α → Bool) (l : List α) (h : ∃ x ∈ l, p x) : Fin l.length :=
  ⟨List.findIdx' p l, by admit /- proof elided -/
  ⟩

def subNat (c : AssocNat) : Nat → AssocNat
| 0            => c 
| Nat.succ k   => pred (subNat c k)

instance {s} : LawfulFunctor (fun α => LeafData α s) :=

finProdFinEquiv in Mathlib.Logic.Equiv.Fin.Basic

noncomputable def P
  (δ : ℚ) (x₀ : F)
  (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁)
  :
  F[Z][X] :=
  let v₀ := Classical.choose (solution_gamma_is_linear_in_Z k (δ := δ) (x₀ := x₀) h_gs)
  let v₁ := Classical.choose 
    (Classical.choose_spec <| solution_gamma_is_linear_in_Z k (δ := δ) (x₀ := x₀) h_gs)
  (
    (Polynomial.map Polynomial.C v₀) +
    (Polynomial.C Polynomial.X) * (Polynomial.map Polynomial.C v₁)
  )

instance [VCVCompatible A] : ∀ i, VCVCompatible ((vPSpec.toProtocolSpec A).Challenge i) :=
  fun _ => by admit /- proof elided -/

BitVec.ofFin in Init.Prelude

instance {k : ℕ} : NatCast (ConcreteBTField k) where
  natCast n:= natCast n

@[reducible]
def Statement (F : Type) (i : Fin (k + 1)) : Type := Fin i.val → F

Fintype in Mathlib.Data.Fintype.Defs

@[simp]
def finRangeTo {k : ℕ} (i : ℕ) : Finset (Fin k) :=
  (List.take i (List.finRange k)).toFinset

def interleaveCode [Semiring F] [DecidableEq F] (C : Submodule F (n → F)) (ι : Type*)
  : Submodule F ((ι × n) → F) :=
  Submodule.span F {v | ∀ i, ∃ c ∈ C, c = fun j => v (i, j)}

Fin.succAboveEmb in Mathlib.Data.Fin.Embedding

instance : Field BaseField := ZMod.instField baseFieldSize

def oracleVerifier : OracleVerifier oSpec Statement OStatement Unit (OStatement ⊕ᵥ OStatement)
    (pSpec OStatement) where

@[reducible, simp] def OStmtOut := fun _ : Fin 2 => OStatement

@[simp]
abbrev SecondSumcheckChallenge : Type := Fin pp.ℓ_n → R

Nonempty in Init.Prelude

String.intercalate in Init.Data.String.Defs

@[reducible, inline]
instance instPolynomialDegreeLT : OracleInterface (R⦃< d⦄[X]) where
  Query := R
  Response := R
  answer := fun ⟨poly, _⟩ point => poly.eval point

def D_YZ (Q : F[Z][X][Y]) : ℕ :=
  Option.getD (dflt := 0) <| Finset.max
    (Finset.image
            (
              fun j =>
                Option.getD (
                  Finset.max (
                    Finset.image
                      (fun k => j + (Bivariate.coeff Q j k).natDegree)
                      (Q.coeff j).support
                  )
                ) 0
            )
            Q.support
    )

is_complete : vectorIOP.perfectCompleteness (pure ()) ⟨isEmptyElim⟩ relation

multiplicity in Mathlib.RingTheory.Multiplicity

def Verifier.fiatShamir (V : Verifier oSpec StmtIn StmtOut pSpec) :
    NonInteractiveVerifier (∀ i, pSpec.Message i) (oSpec ++ₒ fsChallengeOracle StmtIn pSpec)
      StmtIn StmtOut where
  verify := fun stmtIn proof => do
    let messages : pSpec.Messages := proof 0
    let transcript ← messages.deriveTranscriptFS stmtIn
    V.verify stmtIn transcript

Sum in Init.Core

@[simp]
abbrev Statement.AfterSendEvalClaim : Type := Statement.AfterFirstSumcheck R pp

instance : ∀ j, OracleInterface ((pSpecRelay).Message j)
  | ⟨x, h⟩ => by admit /- proof elided -/

MvPolynomial.renameEquiv in Mathlib.Algebra.MvPolynomial.Rename

def Extractor.RoundByRound.id :
    Extractor.RoundByRound oSpec Statement Witness Witness !p[] (fun _ => Witness) where
  eqIn := rfl
  extractMid := fun i => Fin.elim0 i
  extractOut := fun _ _ => _root_.id

@[reducible]
def fieldSize : Nat := 2 ^ 31 - 1

def SkeletonLeafIndex.isRoot {s : Skeleton} (idx : SkeletonLeafIndex s) : Bool :=
  match idx with
  | SkeletonLeafIndex.ofLeaf => true
  | SkeletonLeafIndex.ofLeft _ => false
  | SkeletonLeafIndex.ofRight _ => false

def fst (T : (pSpec₁ ++ₚ pSpec₂).Transcript k) : pSpec₁.Transcript ⟨min k m, by admit /- proof elided -/
⟩ :=
  if hk : k ≤ m then
    fun i => by admit /- proof elided -/

abbrev OutputStatement := StatementRound R _ (.last n)

@[inline, reducible]
def lift : OuterStmtIn × OuterWitIn → InnerStmtOut × InnerWitOut → OuterWitOut :=
  lens.toFunB

def buildLayer (n : ℕ) (leaves : List.Vector α (2 ^ (n + 1))) :
    OracleComp (spec α) (List.Vector α (2 ^ n)) := do
  let leaves : List.Vector α (2 ^ n * 2) :=

CommRing.toRing in Mathlib.Algebra.Ring.Defs

def oracleReduction.sendEvalClaim :
    OracleReduction oSpec
      (Statement.AfterFirstSumcheck R pp) (OracleStatement.AfterFirstSumcheck R pp) (Witness R pp)
      (Statement.AfterSendEvalClaim R pp) (OracleStatement.AfterSendEvalClaim R pp) Unit
      ⟨!v[.P_to_V], !v[∀ i, EvalClaim R i]⟩ :=
  sorry

def nonsquareTranspose [Field F] (ι' : ℕ) (α : ι ↪ F) : Matrix (Fin ι') ι F :=
  (Vandermonde.nonsquare ι' α)ᵀ

noncomputable instance finiteDimensionalCoeffVecSpace (ℓ : ℕ) :
  FiniteDimensional (K := L) (V := CoeffVecSpace L ℓ) :=

embed := sorry

noncomputable def sDomain.lift (i j : Fin r) (h_j : j < ℓ + R_rate) (h_le : i ≤ j)
    (y : sDomain 𝔽q β h_ℓ_add_R_rate j) :
    sDomain 𝔽q β h_ℓ_add_R_rate i :=

def splitPointIntoCoeffs (i : Fin r) (h_i : i < ℓ + R_rate)
  (x : sDomain 𝔽q β h_ℓ_add_R_rate i) :
  Fin (ℓ + R_rate - i.val) → ℕ := fun j =>
    if ((sDomain_basis 𝔽q β
    h_ℓ_add_R_rate i h_i).repr x j = 0) then
      0 else 1

def leftModNat {m n : ℕ} (h_m : m > 0) (i : Fin (m * n)) : Fin m := ⟨i % m, by admit /- proof elided -/
⟩

inductive member (a : α) : List α → Type v where
  | first : member a (a :: is)
  | next : member a is → member a (b :: is)

def duplexSpongeToBasicFSAlgo
    (P : OracleComp (oSpec ++ₒ duplexSpongeChallengeOracle StmtIn U)
    (StmtIn × pSpec.Messages)) :
    OracleComp (oSpec ++ₒ fsChallengeOracle StmtIn pSpec) (StmtIn × pSpec.Messages) :=
  sorry

def proverInput (i : Fin n) : ProverInput
    ((StatementRound R n i.castSucc) × (∀ i, OracleStatement R n deg i))
    Unit ((proverState R n deg i).PrvState 0) where
  input := Prod.fst

RingHom.comp in Mathlib.Algebra.Ring.Hom.Defs

exp : ∀ i : Fin (k + 1), (parℓ_type i) ↪ ℕ

alias E_time_h := outOfOrderHash

@[inline]
def seqCompose {m : ℕ} (Stmt : Fin (m + 1) → Type) (Wit : Fin (m + 1) → Type)
    {n : Fin m → ℕ} {pSpec : ∀ i, ProtocolSpec (n i)}
    (R : (i : Fin m) →
      Reduction oSpec (Stmt i.castSucc) (Wit i.castSucc) (Stmt i.succ) (Wit i.succ) (pSpec i)) :
    Reduction oSpec (Stmt 0) (Wit 0) (Stmt (Fin.last m)) (Wit (Fin.last m)) (seqCompose pSpec) where
  prover := Prover.seqCompose Stmt Wit (fun i => (R i).prover)
  verifier := Verifier.seqCompose Stmt (fun i => (R i).verifier)

noncomputable def batchOracleReduction :
  OracleReduction []ₒ
    Unit (OracleStatement D x m) (Witness F s d m)
    ((Fin m → F) × Fri.Spec.Statement F (0 : Fin (k + 1)))
    (OracleStatement D x m)
    (Fri.Spec.Witness F s d (0 : Fin (k + 2)))
    (batchSpec F m) where
  prover := batchProver D x s d m
  verifier := batchVerifier (k := k) D x m

@[reducible, inline, specialize, simp]
def MessageIdx (vPSpec : VectorSpec n) := {i : Fin n // vPSpec.dir i = .P_to_V}

abbrev Bwd : PermuteDir := Sum.inr ()

Polynomial.modByMonic in Mathlib.Algebra.Polynomial.Div

instance : ∀ j, OracleInterface ((batchSpec F m).Message j)
  | ⟨0, h⟩ => nomatch h

def relHammingDistRange (ι : Type*) [Fintype ι] : Set ℚ≥0 :=
  {d : ℚ≥0 | ∃ d' : ℕ, d' ≤ Fintype.card ι ∧ d = d' / Fintype.card ι}

def Polynomial.toImpl {R : Type*} [Semiring R] (p : R[X]) : UniPoly R :=
  match p.degree with
  | ⊥ => #[]
  | some d  => .ofFn (fun i : Fin (d + 1) => p.coeff i)

def OracleReduction.toReduction {ι : Type} {oSpec : OracleSpec ι}
    {StmtIn : Type} {ιₛᵢ : Type} {OStmtIn : ιₛᵢ → Type} {WitIn : Type}
    {StmtOut : Type} {ιₛₒ : Type} {OStmtOut : ιₛₒ → Type} {WitOut : Type}
    {n : ℕ} {pSpec : ProtocolSpec n}
    [Oₛᵢ : ∀ i, OracleInterface (OStmtIn i)] [Oₘ : ∀ i, OracleInterface (pSpec.Message i)]
    (oracleReduction : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec) :
      Reduction oSpec (StmtIn × (∀ i, OStmtIn i)) WitIn
        (StmtOut × (∀ i, OStmtOut i)) WitOut pSpec :=
  ⟨oracleReduction.prover, oracleReduction.verifier.toVerifier⟩

noncomputable def polyQuotient (S : Finset F) (fPoly : F[X]) : F[X] :=
    (fPoly - (ansPoly S (fun s => fPoly.eval s))) / (vanishingPoly S)

Inv in Init.Prelude

Int.ofNat in Init.Data.Int.Basic

@[inline, specialize]
def OracleReduction.run [∀ i, OracleInterface (pSpec.Message i)]
    (stmt : StmtIn) (oStmt : ∀ i, OStmtIn i) (wit : WitIn)
    (reduction : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec) :
      OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ)
        ((FullTranscript pSpec × (StmtOut × ∀ i, OStmtOut i) × WitOut) ×
          (StmtOut × ∀ i, OStmtOut i)) := do
  let proverResult ← reduction.prover.run ⟨stmt, oStmt⟩ wit
  let stmtOut ← liftM (reduction.verifier.run stmt oStmt proverResult.1)
  return ⟨proverResult, stmtOut⟩

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

def buildMerkleTree {s} (leaf_tree : LeafData α s) : OracleComp (spec α) (FullData α s) :=
  match leaf_tree with
  | LeafData.leaf a => do return (FullData.leaf a)
  | LeafData.internal left right => do
    let leftTree ← buildMerkleTree left
    let rightTree ← buildMerkleTree right
    let rootHash ← singleHash leftTree.getRootValue rightTree.getRootValue
    return FullData.internal rootHash leftTree rightTree

Vector.replicate in Init.Data.Vector.Basic

BEq in Init.Prelude

instance : ∀ i, NeZero (toOutCodewordsCount ℓ ϑ i) :=

is_rbr_knowledge_sound :
    OracleProof.rbrKnowledgeSoundness (pure ()) ⟨isEmptyElim⟩ soundRelation vectorIOP.verifier ε_rbr

Option.bind in Init.Data.Option.Basic

StrongRankCondition in Mathlib.LinearAlgebra.InvariantBasisNumber

instance (priority := low) : DCast₃ α β γ δ where
  dcast₃ ha hb hc d := by admit /- proof elided -/

TensorProduct in Mathlib.LinearAlgebra.TensorProduct.Basic

@[reducible, simp] def StmtIn := Unit

noncomputable def fold_k_core {S : Finset ι} {φ : ι ↪ F} (f : (indexPowT S φ 0) → F)
  [∀ i : ℕ, Neg (indexPowT S φ i)] : (i : ℕ) → (αs : Fin i → F) →
    indexPowT S φ i → F
| 0, _ => fun x₀ => f x₀
| k+1, αs => fun y =>
    let α := αs 0
    let αs' : Fin k → F := fun i => αs (Fin.succ i)
    let fk := fold_k_core f k αs'
    foldf S φ y fk α

Array.map in Init.Data.Array.Basic

def cons {α} {n : ℕ} (hd : α) (tl : Vector α n) : Vector α (n + 1) :=
  tl.insertIdx 0 hd

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

@[simp]
def oCtxLens (i : Fin n) : OracleContext.Lens
    (StatementRound R n i.castSucc) (StatementRound R n i.succ) (Simple.StmtIn R) (Simple.StmtOut R)
    (OracleStatement R n deg) (OracleStatement R n deg)
    (Simple.OStmtIn R deg) (Simple.OStmtOut R deg)
    Unit Unit Unit Unit where
  wit := Witness.Lens.trivial
  stmt := oStmtLens R n deg D i

noncomputable def modBivar (P P' : MvPolynomial (Fin 2) F)
    (hlg : IsUnit ((MonomialOrder.lex).leadingCoeff P')) : MvPolynomial (Fin 2) F :=
      
      let ord : MonomialOrder (Fin 2) := MonomialOrder.lex
      
      let b : Unit → MvPolynomial (Fin 2) F := fun _ => P'
      
      have hb : ∀ i : Unit, IsUnit (ord.leadingCoeff (b i)) := by admit /- proof elided -/

def internalLinearLayer (state : Vector KoalaBear.Field params.width) :
    Vector KoalaBear.Field params.width :=
  
  
  let sumAll := state.foldl (fun acc x => acc + x) 0

instance {α : Type u} [ToNat α] : CoeHead α Nat where
  coe := ToNat.toNat

instance {ι : Type u} (v : ι → Type v) [O : ∀ i, OracleInterface (v i)]
    [h : ∀ i, Fintype (Response (v i))]
    [h' : ∀ i, Inhabited (Response (v i))] :
    [v]ₒ.FiniteRange where
  range_fintype' := h
  range_inhabited' := h'

def natDegreeY (f : F[X][Y]) : ℕ := Polynomial.natDegree f

for rep in (List.finRange γ_repetitions) do
      let mut c_cur : L := 0 
      let v := fold_challenges rep

structure InterleavedCode (κ ι : Type*) [Fintype κ] [Fintype ι] (F : Type*) [Semiring F] where
  MF : MatrixSubmodule κ ι F
  LC : LinearCode ι F

private noncomputable def E (ωs : Fin n → F)
  (f : Fin n → F) (p : Polynomial F) (e : ℕ) : Polynomial F :=
  X ^ (e - (Δ₀(f, p.eval ∘ ωs) : ℕ)) * ElocPolyF ωs f p

def queryCodeword (k : ℕ) (s : Fin (k + 1) → ℕ+) {i : Fin (k + 1)}
      (w : evalDomain D x (∑ j' ∈ (List.take i.1 (List.finRange (k + 1))).toFinset, (s j').1)) :
    OracleComp [FinalOracleStatement D x s]ₒ F :=
      OracleComp.lift <| by
        simpa using
          OracleSpec.query
            (spec := [FinalOracleStatement D x s]ₒ)
            ⟨i.1, Nat.lt_succ_of_lt i.2⟩
            (by admit /- proof elided -/
            )

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

Bool in Init.Prelude

def eval₂ [Semiring S] (f : R →+* S) (x : S) (p : UniPoly R) : S :=
  p.zipIdx.foldl (fun acc ⟨a, i⟩ => acc + f a * x ^ i) 0

@[reducible]
def messageLength (vPSpec : VectorSpec n) (i : MessageIdx vPSpec) : Nat := vPSpec.length i

@[ext]
structure ProverOutput {ι : Type} (oSpec : OracleSpec ι) (Output PrvState : Type) where
  output : PrvState → OracleComp oSpec Output

@[reducible]
def pSpec : ProtocolSpec 2 :=
  ⟨
    !v[.V_to_P, .P_to_V],
    !v[
        F,
        (evalDomain D x (∑ j' ∈ (List.take (i.1 + 1) (List.finRange (k + 1))).toFinset, s j')) → F
      ]
  ⟩

def MlPolyEval.mk {R : Type*} (n : ℕ) (v : Vector R (2 ^ n)) : MlPolyEval R n := v

queryOStmt : StmtIn → (∀ i, pSpec.Challenge i) → List ((i : ιₛᵢ) × (Oₛᵢ i).Query)

class Context.Lens.IsComplete {OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type}
    {OuterWitIn OuterWitOut InnerWitIn InnerWitOut : Type}
    (outerRelIn : Set (OuterStmtIn × OuterWitIn))
    (innerRelIn : Set (InnerStmtIn × InnerWitIn))
    (outerRelOut : Set (OuterStmtOut × OuterWitOut))
    (innerRelOut : Set (InnerStmtOut × InnerWitOut))
    (compat : (OuterStmtIn × OuterWitIn) → (InnerStmtOut × InnerWitOut) → Prop)
    (lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut
                        OuterWitIn OuterWitOut InnerWitIn InnerWitOut) where

Function.RightInverse in Init.Data.Function

instance : Field BaseField := ZMod.instField BASE_FIELD_CARD

Ne in Init.Core

none
</all_available_defs>

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

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

theorem is_prime : Nat.Prime fieldSize

@[simp]
theorem dcons_succ {motive : Fin (n + 1) → Sort u} (a : motive 0)
    (v : (i : Fin n) → motive i.succ) (i : Fin n) : (a ::ᵈ⟨motive⟩ v) i.succ = v i

theorem support_C {r : R} [h : Decidable (r = 0)] :
    (@C R σ _ r).support = if r = 0 then ∅ else { 0 }

theorem decoder_dist_impl_mem
  {k r D e : ℕ}
  (h_e : e ≤ n - Real.sqrt (k * n))
  {ωs : Fin n ↪ F}
  {f : Fin n → F}
  {p : F[X]}
  (h_dist : Δ₀(f, p.eval ∘ ωs) ≤ e)
  :
  p ∈ decoder k r D e ωs f

theorem intermediateNormVpoly_comp_qmap (i : Fin (ℓ))
    (k : Fin (ℓ - i - 1)) : -- corresponds to intermediateNormVpoly_comp

theorem happend_assoc {α : Fin m → Sort u} {β : Fin n → Sort u} {p : ℕ} {γ : Fin p → Sort u}
    (u : (i : Fin m) → α i) (v : (i : Fin n) → β i) (w : (i : Fin p) → γ i) :
    happend (happend u v) w =
      fun i => cast (by simp [vappend_assoc])
        (happend u (happend v w) (i.cast (by omega)))

Nat.le_of_succ_le in Init.Data.Nat.Basic

lemma f_eq_evenPart_plus_x_oddPart {f : Polynomial F} :
  f = evenPart f + Polynomial.X * oddPart f

theorem foldl_succ
 {α β} {n : ℕ} [NeZero n] (f : β → α → β) (init : β) (v : Vector α n) :
  v.foldl (f:=f) (b:=init) = v.tail.foldl (f:=f) (b:=f init v.head)

congrArg in Init.Prelude

Fin.is_le' in Init.Data.Fin.Lemmas

lemma matchSize_size_eq {p q : UniPoly Q} :
    let (p', q') := Array.matchSize p q 0
    p'.size = q'.size

lemma bIdx_succ_mul_ϑ_lt_ℓ_succ (bIdx : Fin (ℓ / ϑ - 1)) :
    (↑bIdx + 1) * ϑ < ℓ + 1

theorem nsmul_zero : nsmul 0 p = 0

lemma natDegree_definingPoly {F : Type*} [Field F] [Fintype F] (s : F) [NeZero s] :
  (definingPoly s).natDegree = 2

@[simp]
theorem InternalData.ofFun_get {α} {s} (tree : InternalData α s) :
    InternalData.ofFun s (fun idx => tree.get idx) = tree

lemma concrete_mul_zero
  (prevBTFieldProps : ConcreteBTFieldProps (k := k - 1))
  (a : ConcreteBTField k) : concrete_mul a (zero (k:=k)) = zero (k:=k)

lemma getLast_toImpl {p : Q[X]} (hp : p ≠ 0) : let h : p.toImpl.size > 0 := toImpl_nonzero hp;
    p.toImpl[p.toImpl.size - 1] = p.leadingCoeff

@[simp]
lemma finite_possibleDeltas : (possibleDeltas U V).Finite

theorem randomOracle_cache_neverFails_iff_runWithOracle_neverFails {β}
    [DecidableEq ι] [spec.DecidableEq] [(i : ι) → SelectableType (OracleSpec.range spec i)]
    (oa : OracleComp (spec) β) (preexisting_cache : spec.QueryCache)
    :
    ((oa.simulateQ randomOracle).run preexisting_cache).neverFails
    ↔
    (∀ (f : spec.FunctionType),
      Oracle.containsCache f preexisting_cache →
      (runWithOracle f oa).isSome)

theorem empty_unique (v : Fin 0 → α) : v = !v[]

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

lemma subLeftFull_of_vandermonde_is_vandermonde (h : m ≤ n) :
  Matrix.vandermonde α = Matrix.subLeftFull (nonsquare n α) (Fin.castLE h)

@[simp]
theorem fcons_zero {β : Fin n → A} (a : F α) (b : (i : Fin n) → F (β i)) :
    fcons a b 0 = cast (by simp [vcons_zero]) a

lemma Z_square_mul_form
  (k : ℕ)
  (prev : ConcreteBTFStepResult (k := k)) :
  letI : Field (ConcreteBTField k) := mkFieldInstance (prev.toConcreteBTFieldProps)
  letI : Field (ConcreteBTField (k + 1)) := mkFieldInstance (k:=k+1)
    (props:=liftBTFieldProps (k:=k) (prevBTFResult:=prev))
  letI : Algebra (ConcreteBTField k) (ConcreteBTField (k + 1)) :=
    instAlgebraLiftConcreteBTField k prev
  Z (k + 1) ^ 2
    = Z (k + 1)
      * (algebraMap (ConcreteBTField k) (ConcreteBTField (k + 1))) (Z k)
      + 1

@[simp]
theorem embedSum_succ_succ {n : Fin (m + 1) → ℕ} {i : Fin m} (j : Fin (n i.succ)) :
    embedSum (i.succ) j = Fin.natAdd _ (embedSum i j)

lemma NTTStage_correctness (i : Fin (ℓ))
    (input_buffer : Fin (2 ^ (ℓ + R_rate)) → L) (original_coeffs : Fin (2 ^ ℓ) → L) :
    additiveNTTInvariant 𝔽q β h_ℓ_add_R_rate (evaluation_buffer:=input_buffer)
      (original_coeffs:=original_coeffs) (i := ⟨i.val+1, by omega⟩) →
    additiveNTTInvariant 𝔽q β h_ℓ_add_R_rate (evaluation_buffer:=NTTStage 𝔽q β h_ℓ_add_R_rate
      ⟨i, by omega⟩ input_buffer) (original_coeffs:=original_coeffs) ⟨i, by omega⟩

lemma BerlekampWelch_E_ne_zero {e k : ℕ}
  {ωs f : Fin n → F}
  {E Q : Polynomial F}
  (h_cond : BerlekampWelchCondition e k ωs f E Q)
  : E ≠ 0

theorem split_sum_eq_sum_split {k : ℕ} (h_pos : k > 0) (x₀ x₁ : ConcreteBTField k)
  (hi₀ lo₀ hi₁ lo₁ : ConcreteBTField (k - 1))
  (h_split_x₀ : split h_pos x₀ = (hi₀, lo₀))
  (h_split_x₁ : split h_pos x₁ = (hi₁, lo₁)) :
  split h_pos (x₀ + x₁) = (hi₀ + hi₁, lo₀ + lo₁)

theorem prime_23 : Nat.Prime 23

@[simp]
theorem rtake_self (v : (i : Fin n) → α i) :
    rtake n (by omega) v = fun i : Fin n => dcast (by simp [Fin.cast]) (v i)

private lemma sum_K_eq_card : ∑ (α : F), K B i α = B.card

@[simp]
theorem runWithOracle_freeMonad_pure (f : spec.FunctionType) (a : Option α) :
    runWithOracle f (FreeMonad.pure a) = a

beq_iff_eq in Init.Core

theorem decoder_eq_some {e k : ℕ} [NeZero n] {ωs f : Fin n → F} {p : Polynomial F}
  (he : 2 * e < n - k + 1)
  (hn : k ≤ n)
  (h_inj : Function.Injective ωs)
  (h_deg : p.natDegree < k)
  (h_dist : Δ₀(f, p.eval ∘ ωs) ≤ e)
  : decoder e k ωs f = some p

lemma evenPart_x_eval_eq {f : Polynomial F} {s : F} :
    (evenPart_x f).eval (s * s) = (evenPart f).eval s

theorem seqCompose_soundness
    (lang : (i : Fin (m + 1)) → Set (Stmt i))
    (V : (i : Fin m) → Verifier oSpec (Stmt i.castSucc) (Stmt i.succ) (pSpec i))
    (soundnessError : Fin m → ℝ≥0)
    (h : ∀ i, (V i).soundness init impl (lang i.castSucc) (lang i.succ) (soundnessError i)) :
      (Verifier.seqCompose Stmt V).soundness init impl (lang 0) (lang (Fin.last m))
        (∑ i, soundnessError i)

lemma getBit_zero_eq_self {n : ℕ} (h_n : n < 2) : getBit 0 n = n

omit [Finite F] in
lemma minus_one_in_doms {i : ℕ} (h : i < n) :
    -1 ∈ evalDomain D i

Fin.isLt in Init.Prelude

omit [Fintype L] [DecidableEq L] [Fintype 𝔽q] h_Fq_char_prime in
theorem root_U_lift_down
  (i : Fin r) (h_i_add_1 : i + 1 < r) (a : L) :
  a ∈ (U 𝔽q β (i+1)) → ∃! x: 𝔽q, a - x • β i ∈ (U 𝔽q β i)

lemma rootMultiplicity_some_implies_root {F : Type} [CommSemiring F] [DecidableEq F]
  {x y : F} {f : F[X][Y]} (h : some 0 < (rootMultiplicity (f := f) x y))
  : (f.eval 0).eval 0 = 0

private lemma johnson_unrefined [Zero F]
  (h_n : 0 < n)
  (h_B : 2 ≤ B.card)
  (h_card : 2 ≤ (Fintype.card F))
  :
  (1 - e B 0 / n) ^ 2 * B.card + B.card * (e B 0) ^ 2 / ((Fintype.card F - 1) * n^2) - 1
  ≤
  (B.card - 1) * (1 - d B/n)

lemma one_bitvec_toNat {width : ℕ} (h_width : width > 0) : (1#width).toNat = 1

@[simp]
lemma bIdx_mul_ϑ_add_i_cast_lt_ℓ_succ (bIdx : Fin (ℓ / ϑ - 1)) (i : Fin (ϑ - 1 + 1))
    : ↑bIdx * ϑ + i < ℓ + 1

@[simp]
lemma addSalt_Type (i : Fin n) :
    (pSpec.addSalt Salt).«Type» i = match hDir : pSpec.dir i with

@[simp]
theorem shift_left_mem {s : Finset ℕ} {d : ℕ} : d ∈ shift_left s ↔ (d + 1) ∈ s

theorem comp_x_square_coeff {f : Polynomial F} {n : ℕ} :
  (f.comp (X * X)).coeff n = if Even n then f.coeff (n / 2) else 0

lemma monoToLagrange_eq_monoToLagrange_segment (n : ℕ) [NeZero n] (v : Vector R (2 ^ n)) :
  have h_n_ne_zero: n ≠ 0

Nat.add_sub_cancel in Init.Data.Nat.Basic

@[simp]
theorem runWithOracle_freeMonad_pure_some (f : spec.FunctionType) (a : α) :
    runWithOracle f (FreeMonad.pure (a : Option α)) = a

theorem append_run (tr : (pSpec₁ ++ₚ pSpec₂).FullTranscript) :
      (V₁.append V₂).run stmt tr =
        (do
          let stmt₂ ← V₁.run stmt tr.fst
          let stmt₃ ← V₂.run stmt₂ tr.snd
          return stmt₃)

theorem split_zero {k : ℕ} (h_pos : k > 0) : split h_pos zero = (zero, zero)

Nat.lt_of_le_of_lt in Init.Prelude

private lemma evenPart_eq_evenPart' {f : Polynomial F} : evenPart f = evenPart' f

@[to_additive (attr := simp)]
theorem prod_insertNth [CommMonoid β] {n : ℕ} (x : β) (f : Fin n → β) (p : Fin (n + 1)) :
    ∏ i, insertNth p x f i = x * ∏ i, f i

@[simp]
theorem cast_id : Transcript.cast rfl rfl rfl = (id : pSpec₁.Transcript k → _)

omit [NoZeroDivisors 𝔽] in
lemma foldNth_zero {s : ℕ} {α : 𝔽} : foldNth (2 ^ s) 0 α = 0

omit hF₂ in
theorem kernel_W_eq_U (i : Fin r) :
  LinearMap.ker (polyEvalLinearMap (W 𝔽q β i)
    (W_is_additive 𝔽q β i)) = U 𝔽q β i

@[simp]
theorem zero_vappend {u : Fin 0 → α} (v : Fin n → α) :
    vappend u v = v ∘ Fin.cast (Nat.zero_add n)

theorem relayOracleReduction_perfectCompleteness (hInit : init.neverFails) (i : Fin ℓ)
    (hNCR : ¬ isCommitmentRound ℓ ϑ i) :
    OracleReduction.perfectCompleteness
      (pSpec := pSpecRelay)
      (relIn := foldStepRelOut (mp := mp) 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
        (𝓑 := 𝓑) i)
      (relOut := roundRelation (mp := mp) 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
        (𝓑 := 𝓑) i.succ)
      (oracleReduction := relayOracleReduction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
        i hNCR)
      (init := init)
      (impl := impl)

private lemma oddPart_eq_oddPart' {f : Polynomial F} : oddPart f = oddPart' f

theorem dconcat_dcons_eq_dcons_dconcat {motive : Fin (n + 2) → Sort u} (a : motive 0)
    (v : (i : Fin n) → motive (succ (castSucc i))) (b : motive (last (n + 1))) :
    (a ::ᵈ v) :+ᵈ⟨motive⟩ b = a ::ᵈ⟨motive⟩ (v :+ᵈ b)

@[simp]
theorem insertNth_apply_same : insertNth p y s p = y

@[simp]
theorem oracleReduction_perfectCompleteness (hInit : init.neverFails) :
    (oracleReduction oSpec Statement OStatement Witness).perfectCompleteness init impl rel rel

@[simp] -- main lemma for bIdx: Fin (ℓ / ϑ - 1) bounds
lemma bIdx_mul_ϑ_add_x_lt_ℓ_sub_ϑ (bIdx : Fin (ℓ / ϑ - 1)) (x : ℕ) {hx : x ≤ ϑ} :
    ↑bIdx * ϑ + x ≤ ℓ - ϑ

Polynomial.degree_sum_le in Mathlib.Algebra.Polynomial.Degree.Definitions

Fin.val_injective in Mathlib.Data.Fin.Basic

@[simp]
theorem cast_id : ChallengeIdx.cast (Eq.refl n₁) rfl = (id : pSpec₁.ChallengeIdx → _)

private lemma johnson_unrefined_by_M [Zero F]
  (h_n : 0 < n)
  (h_B : 2 ≤ B.card)
  (h_card : 2 ≤ (Fintype.card F))
  :
  B.card * ((1 - e B 0 / n) ^ 2  + (e B 0) ^ 2 / ((Fintype.card F - 1) * n^2) - 1 + d B/n)
  ≤
  d B/n

theorem fcons_inj {β : Fin n → A} (a₁ a₂ : F α) (b₁ b₂ : (i : Fin n) → F (β i)) :
    fcons a₁ b₁ = fcons a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

omit [NoZeroDivisors 𝔽] in
lemma foldNth_degree_le {n : ℕ} {f : 𝔽[X]} {α : 𝔽} [inst : NeZero n] :
    (foldNth n f α).natDegree ≤ f.natDegree / n

lemma concrete_exists_pair_ne {k : ℕ} : ∃ x y : ConcreteBTField k, x ≠ y

theorem towerEquiv_commutes_left (i j : ℕ) (h : i ≤ j) : ∀ r : ConcreteBTField i,
  (AlgebraTower.algebraMap i j h) ((towerEquiv i).ringEquiv r) =
  (towerEquiv j).ringEquiv ((AlgebraTower.algebraMap i j h) r)

private lemma Bi_biUnion_F2i :
  Bi B i = Finset.univ.biUnion (F2i B i)

theorem hconcat_init_self {α : Fin n.succ → Sort u} (v : (i : Fin (n + 1)) → α i) :
    True

@[simp]
theorem dconcat_zero {motive : Fin 1 → Sort u} (a : motive (last 0)) :
    !d⟨fun _ : Fin 0 => motive (castSucc _)⟩[] :+ᵈ⟨motive⟩ a = !d⟨motive⟩[a]

theorem singletonBound [CommRing F] [StrongRankCondition F]
  (LC : LinearCode ι F) :
  dim LC ≤ length LC - Code.minDist (LC : Set (ι → F)) + 1

theorem fold_advances_evaluation_poly
  (i : Fin (ℓ)) (h_i_succ_lt : i + 1 < ℓ + 𝓡)
  (coeffs : Fin (2 ^ (ℓ - ↑i)) → L) (r_chal : L) :
  let P_i : L[X] := intermediateEvaluationPoly 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by
    exact Nat.lt_trans (n := i) (k := ℓ+1) (m := ℓ) (h₁ := i.isLt) (by exact Nat.lt_add_one ℓ)
  ⟩) coeffs
  let f_i

lemma sum_of_and_eq_zero_is_xor {n m : ℕ} (h_n_AND_m : n &&& m = 0) : n + m = n ^^^ m

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

lemma take_eq_take : transcript⟦:m⟧ = transcript.take m h

Fin.append_left in Mathlib.Data.Fin.Tuple.Basic

lemma Fin.val_sub_one (a : Fin r) (h_a_sub_1 : a > 0) : (a - 1).val = a.val - 1

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

@[simp]
theorem partialSum_nil : [].partialSum = [0]

lemma zero_def [Zero R] : zero = Vector.replicate (2 ^ n) 0

@[simp]
theorem take_append_left' : (pSpec₁ ++ₚ pSpec₂)⟦:m⟧ = pSpec₁

@[simp]
lemma cons_empty_tail_eq_nil {α} (hd : α) (tl : Vector α 0) :
    cons hd tl = ⟨#[hd], rfl⟩

theorem withBot_lt_one_cases (x : WithBot ℕ) (h : x < (1 : ℕ)) : x = ⊥ ∨ x = (0 : ℕ)

theorem eqPolynomial_mem_restrictDegree (r : σ → R) : (eqPolynomial r) ∈ R⦃≤ 1⦄[X σ]

theorem mul_join_via_add_smul (k : ℕ) (h_pos : k > 0) (a₁ a₀ b₁ b₀ : BTField (k - 1)) :
  ⋘ a₁, a₀ ⋙ * ⋘ b₁, b₀ ⋙ = ⋘ a₁ * b₁ * Z (k - 1) + a₁ * b₀ + a₀ * b₁, a₀ * b₀ + a₁ * b₁ ⋙

private lemma natDegree_Q
  (h : (Δ₀(f, p.eval ∘ ωs) : ℕ) ≤ e) :
  (Q ωs f p e).natDegree ≤ e + p.natDegree

@[simp]
lemma polynomialOfCoeffs_mem_degreeLT [NeZero deg] :
  polynomialOfCoeffs coeffs ∈ degreeLT F deg

theorem oracleVerifier_toVerifier_run {stmt : Statement} {oStmt : ∀ i, OStatement i}
    {tr : (oraclePSpec Witness).FullTranscript} :
    (oracleVerifier oSpec Statement OStatement Witness).toVerifier.run ⟨stmt, oStmt⟩ tr =
      pure ⟨stmt, Sum.rec oStmt (fun i => match i with | 0 => tr 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 foldl_NTTStage_inductive_aux (h_ℓ : ℓ ≤ r) (k : Fin (ℓ + 1))
    (original_coeffs : Fin (2 ^ ℓ) → L) :
    additiveNTTInvariant 𝔽q β h_ℓ_add_R_rate
    (Fin.foldl k (fun current_b i ↦ NTTStage 𝔽q β h_ℓ_add_R_rate
      ⟨ℓ - i -1, by omega⟩ current_b) (tileCoeffs original_coeffs))
    original_coeffs ⟨ℓ - k, by omega⟩

NeZero.ne in Init.Data.NeZero

theorem finSuccEquivNth_eq :
    (finSuccEquivNth R p : MvPolynomial (Fin (n + 1)) R →+* Polynomial (MvPolynomial (Fin n) R)) =
      eval₂Hom (Polynomial.C.comp (C : R →+* MvPolynomial (Fin n) R))
        (Fin.insertNth p Polynomial.X (Polynomial.C ∘ X))

@[simp] lemma twoAdicGenerators_succ_square_eq' (idx : Fin twoAdicity) :
    twoAdicGenerators[idx.val + 1] ^ 2 = twoAdicGenerators[idx]
</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 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>

