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>
Fin in Init.Prelude
Subspace in Mathlib.Algebra.Module.Submodule.Basic
Set in Mathlib.Data.Set.Defs
Set.Ico in Mathlib.Order.Interval.Set.Defs
Submodule in Mathlib.Algebra.Module.Submodule.Defs
Submodule.span in Mathlib.LinearAlgebra.Span.Defs
Polynomial.C in Mathlib.Algebra.Polynomial.Basic
Nat in Init.Prelude
Fintype in Mathlib.Data.Fintype.Defs
Fintype.card in Mathlib.Data.Fintype.Card
algebraMap in Mathlib.Algebra.Algebra.Defs
Fin.foldl in Init.Data.Fin.Fold
context in Examples.FrankingProtocol
Finset in Mathlib.Data.Finset.Defs
Finset.univ in Mathlib.Data.Fintype.Defs
Eq in Init.Prelude
Polynomial in Mathlib.Algebra.Polynomial.Basic
DecidableEq in Init.Prelude

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

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

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

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

def g (n : ℕ) (c : ℕ) (x : ℕ) := (x * x + c) % n

Nat.zero in Init.Prelude

instance {k : Fin (n + 1)} : Fintype (pSpec.MessageIdxUpTo k) :=
  inferInstanceAs (Fintype <| MessageIdx (pSpec.take k k.is_le))

structure StatementRound (i : Fin (n + 1)) where
  
  target : R
  
  challenges : Fin i → R

exp : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1), (parℓ_type i j) ↪ ℕ

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

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)

Multiset.map in Mathlib.Data.Multiset.MapFold

def witnessStructuralInvariant {i : Fin (ℓ + 1)} (stmt : Statement (L := L) Context i)
    (wit : Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i): Prop :=
  wit.H = projectToMidSumcheckPoly ℓ wit.t (m:=mp.multpoly stmt.ctx) i stmt.challenges ∧
  wit.f = getMidCodewords 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) wit.t stmt.challenges

@[inline, specialize]
def oracleProver : OracleProver oSpec
    Statement OStatement (∀ i, Witness i)
    Statement (OStatement ⊕ᵥ Witness) Unit
    (oraclePSpec Witness) where
  PrvState := fun _ => (Statement × (∀ i, OStatement i)) × (∀ i, Witness i)
  input := id
  sendMessage | ⟨0, _⟩ => fun ⟨stmt, wit⟩ => pure (wit, ⟨stmt, wit⟩)
  
  receiveChallenge | ⟨0, h⟩ => nomatch h
  output := fun ⟨⟨stmt, oStmt⟩, wit⟩ => pure (⟨stmt, Sum.rec oStmt wit⟩, ())

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)

def PowerType (n : ℕ) : Type := dfoldr' n (fun _ => Type) (fun _ T => T → T) Nat

noncomputable def listBlockRelDistance
  (i k : ℕ) {S : Finset ι} {φ : ι ↪ F} {φ' : (indexPowT S φ i) ↪ F}
  {m : ℕ} [DecidableEq F] [DecidableEq ι] [Smooth φ]
  (f : (indexPowT S φ i) → F) (S' : Finset (indexPowT S φ i))
  [∀ i : ℕ, Fintype (indexPowT S φ i)] [DecidableEq (indexPowT S φ i)] [Smooth φ']
  (C : Set ((indexPowT S φ i) → F)) (_hcode : C = smoothCode φ' m) (δ : ℝ≥0)
  [h : DecidableBlockDisagreement i k f S' φ'] : (Set ((indexPowT S φ i) → F)) :=
    { u ∈ C | Δᵣ(i, k, f, S', φ', u) ≤ δ }

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

@[inline, specialize]
def eval (x : R) (p : UniPoly R) : R :=
  p.eval₂ (RingHom.id R) x

Subgroup.zpowers in Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

@[reducible]
def pBits : Nat := 31

def α' (x₀ : F) (R : F[X][X][Y]) (H_irreducible : Irreducible H) (t : ℕ) : 𝕃 H :=
  α x₀ R _ (φ := ⟨H_irreducible⟩) t

def InnerStmtIn_Test := ℤ[X] × ℤ

instance {i : Fin (ℓ / ϑ - 1)} : ∀ j, SelectableType ((pSpecFullNonLastBlock 𝔽q β
  (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i).Challenge j) := instSelectableTypeChallengeAppend

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

instance {i : Fin ℓ} : ∀ j, SelectableType ((pSpecFoldCommit 𝔽q β
  (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i).Challenge j) := instSelectableTypeChallengeAppend

protected def cast
    (hOₘ : ∀ i, Oₘ₁ i = dcast (Message.cast_idx hSpec) (Oₘ₂ (i.cast hn hSpec)))
    (V : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec₁) :
    OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec₂ where
  verify := fun stmt challenges =>
    simulateQ sorry (V.verify stmt (dcast₂ hn.symm (dcast_symm hn hSpec) challenges))
  embed := V.embed.trans
    (Embedding.sumMap
      (Equiv.refl _).toEmbedding
      ⟨MessageIdx.cast hn hSpec, MessageIdx.cast_injective hn hSpec⟩)
  hEq := fun i => by admit /- proof elided -/

instance instDecidableEqOption {α : Type*} [DecidableEq α] :
    DecidableEq (Option α) := inferInstance

instance instST₁ : ∀ i, SelectableType ((⟨!v[.P_to_V], !v[R⦃≤ deg⦄[X]]⟩ ++ₚ !p[]).Challenge i) :=
  instSelectableTypeChallengeAppend

@[reducible, simp] def WitOut := Unit

@[inline, specialize]
def oracleVerifier : OracleVerifier oSpec
    Statement OStatement Statement (OStatement ⊕ᵥ (fun _ : Fin 1 => Witness))
    (oraclePSpec Witness) where
  verify := fun stmt _ => pure stmt
  embed := .sumMap (.refl _)
    <| Equiv.toEmbedding
    <|.symm (subtypeUnivEquiv (by admit /- proof elided -/
    ))
  hEq := by admit /- proof elided -/

permute_or_inv_in_trace : ∀ i : Fin outputState.length,
    (inputState[i], outputState[i]) ∈ trace.getQ (.inr .Fwd)
    ∨ (outputState[i], inputState[i]) ∈ trace.getQ (.inr .Bwd)

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

capacitySegment_input_ne_output : ∀ i : Fin outputState.length,
    inputState[i].capacitySegment ≠ outputState[i].capacitySegment

noncomputable def monomialToNovelCoeffs

noncomputable def D_X (rho : ℚ) (n m : ℕ) : ℝ := (m + 1/2) * (Real.sqrt rho) * n

noncomputable def qMap_total_fiber
    
      (i : Fin r) (steps : ℕ) (h_i_add_steps : i.val + steps < ℓ + 𝓡)
        (y : sDomain 𝔽q β h_ℓ_add_R_rate (i := ⟨i.val + steps, by admit /- proof elided -/
        ⟩)) :
    Fin (2 ^ steps) → sDomain 𝔽q β h_ℓ_add_R_rate i :=
  if h_steps : steps = 0 then by
    
    subst h_steps
    simp only [add_zero, Fin.eta] at y
    exact fun _ => y
  else by
    
    let basis_y := sDomain_basis 𝔽q β h_ℓ_add_R_rate (i := ⟨i+steps,by admit /- proof elided -/
    ⟩) (by admit /- proof elided -/
    )
    let y_coeffs : Fin (ℓ + 𝓡 - (↑i + steps)) →₀ 𝔽q := basis_y.repr y

def disagreementSet (i : Fin ℓ) (steps : ℕ) [NeZero steps] (h_i_add_steps : i.val + steps ≤ ℓ)
  (f g : OracleFunction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ⟨i.val + steps, by admit /- proof elided -/
    ⟩) :
  Set ((sDomain 𝔽q β h_ℓ_add_R_rate) ⟨i.val + steps, by admit /- proof elided -/
  ⟩) :=
  {y | f y ≠ g y}

OracleComp.liftComp in VCVio.OracleComp.Coercions.SubSpec

Or.inr in Init.Prelude

input := fun ⟨⟨stmt, oStmt⟩, wit⟩ => (stmt, oStmt, wit)

def getCommitProverFinalOutput (i : Fin ℓ)
    (inputPrvState : commitPrvState (Context := Context) 𝔽q β (ϑ := ϑ)
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i 0) :
  (↥(sDomain 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, by admit /- proof elided -/
  ⟩) → L) ×
  commitPrvState (Context := Context) 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i 1 :=
  let (stmt, oStmtIn, wit) := inputPrvState
  let fᵢ_succ := wit.f
  let oStmtOut := snoc_oracle 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
    oStmtIn fᵢ_succ 
  (fᵢ_succ, (stmt, oStmtOut, wit))

def foldStepRelOutProp (i : Fin ℓ)
    (input : (Statement (L := L) Context i.succ ×
      (∀ j, OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i.castSucc j)) ×
      Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ) : Prop :=
  let stmt := input.1.1
  let oStmt := input.1.2
  let wit := input.2
  masterKStateProp (mp := mp) (𝓑 := 𝓑) 𝔽q β
    (stmtIdx := i.succ) (oracleIdx := i.castSucc)
    (h_le := Nat.le_of_lt (Fin.castSucc_lt_succ i)) stmt wit oStmt (localChecks := True)

Fin.succEmb in Mathlib.Data.Fin.Embedding

instance {α : Type u} : Slice (List α) Nat Nat (fun _ _ _ => True) (fun _ _ _ _ => List α) where
  slice xs start stop _ := xs.extract start stop

HMul in Init.Prelude

φ in ToMathlib.Control.Monad.Relative

@[inline, reducible]
protected def id :
    Witness.Lens OuterStmtIn OuterStmtOut OuterWitIn OuterWitOut OuterWitIn OuterWitOut :=
  ⟨Prod.snd, fun _ => Prod.snd⟩

Units.mulAction' in Mathlib.Algebra.Group.Action.Units

def ConstraintSystem (𝓡 : Type) (numWires numGates : ℕ) := Fin numGates → Gate 𝓡 numWires

def indexPow (S : Finset ι) (φ : ι ↪ F) (k : ℕ) : Finset F :=
  S.image (fun x => (φ x) ^ k)

def Prover.addSalt (P : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec)
    (saltComp : (i : pSpec.MessageIdx) → P.PrvState i.1.castSucc → OracleComp oSpec (Salt i)) :
  Prover oSpec StmtIn WitIn StmtOut WitOut (pSpec.addSalt Salt) where
  PrvState := P.PrvState
  input := P.input
  sendMessage := fun i st => by admit /- proof elided -/

instance [ProverFirst pSpec] : Unique (pSpec.MessageIdx) where
  default := ⟨0, by admit /- proof elided -/
  ⟩
  uniq := fun ⟨i, _⟩ => by admit /- proof elided -/

instance coe_field_adjoinRoot (k : ℕ) : Coe (AdjoinRoot (poly k)) (BTField (k+1)) where
  coe := Eq.mp (BTField_succ_eq_adjoinRoot k)

noncomputable def matching_set_at_x
  (δ : ℚ)
  (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁)
  (x : Fin n)
  : Finset F := @Set.toFinset _ {z : F | ∃ h : z ∈ matching_set k ωs δ u₀ u₁ h_gs,
    u₀ x + z * u₁ x = 
      (Pz (matching_set_is_a_sub_of_coeffs_of_close_proximity k h_gs h)).eval (ωs x)} sorry

class VerifierOnly (pSpec : ProtocolSpec 1) extends VerifierFirst pSpec

@[reducible]
def value (op : MemoryWrite ι α) := op.2

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

def checkInitImports : IO Bool := do
  \n\
      The `header` linter is included in Mathlib.Init, and every file in Mathlib \
      should import Mathlib.Init.\nPlease adjust the imports accordingly."
    return true

protected def basis : F := sorry

MvPolynomial in Mathlib.Algebra.MvPolynomial.Basic

QueryImpl.impl in VCVio.OracleComp.SimSemantics.SimulateQ

instance instDCast₂ : DCast₂ Nat ProtocolSpec (fun _ pSpec => FullTranscript pSpec) where
  dcast₂ h h' T := FullTranscript.cast h h' T
  dcast₂_id := cast_id

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

pos in ToMathlib.Control.Comonad.Instances

BStar : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1),
    (Set ((indexPowT (S i) (P.φ i) j) → F)) → Type → ℝ≥0
  errStar : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1),
    (Set ((indexPowT (S i) (P.φ i) j) → F)) → Type → ℝ → ENNReal

let mut x := powMod a d n
    if x = 1 ∨ x = n - 1 then
      continue

IsEmpty in Mathlib.Logic.IsEmpty

instance instNatPow {n : ℕ} : NatPow (CNat n) := match n with
  | 0 => by admit /- proof elided -/
  | .succ n => by admit /- proof elided -/

Finset.filter in Mathlib.Data.Finset.Filter

instance {k : ℕ} : NeZero (1 : ConcreteBTField k) :=

def proximityChecksSpec (γ_challenges :
    Fin γ_repetitions → sDomain 𝔽q β h_ℓ_add_R_rate ⟨0, by omega⟩)
    (oStmt : ∀ j, OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ (Fin.last ℓ) j)
    (fold_challenges : Fin ℓ → L) (final_constant : L) : Prop :=
  ∀ rep : Fin γ_repetitions,
    let v := γ_challenges rep
    -- For all folding levels k = 0, ..., ℓ/ϑ - 1, we track c_cur through the iterations
    ∀ k_val : Fin (ℓ / ϑ),
      let i := k_val.val * ϑ
      have h_k: k_val ≤ (ℓ/ϑ - 1) := by omega
      have h_i_add_ϑ_le_ℓ : i + ϑ ≤ ℓ := by
        calc i + ϑ = k_val * ϑ + ϑ := by omega
          _ ≤ (ℓ/ϑ - 1) * ϑ + ϑ := by
            apply Nat.add_le_add_right; apply Nat.mul_le_mul_right; omega
          _ = ℓ/ϑ * ϑ :=

instance {U : Type} {H : Type*} {R : Type*} [SpongeUnit U] [DuplexSpongeInterface U H] :
    UnitTranscript (FSProverState U H R) U where
  publicUnits state input := do
    
    
    let newState ← state.addUnits input
    .ok { rng := newState.rng, hashState := newState.hashState,
          nargString := state.nargString } 
  fillChallengeUnits state count :=
    match state.hashState.squeeze count with
    | .ok (newHashState, output) =>
      .ok ({ rng := state.rng, hashState := newHashState, nargString := state.nargString }, output)
    | .error e => .error e

def MessageIdx.inr (i : MessageIdx pSpec₂) : MessageIdx (pSpec₁ ++ₚ pSpec₂) :=
  ⟨Fin.natAdd m i.1, by admit /- proof elided -/
  ⟩

Finset.map in Mathlib.Data.Finset.Image

@[simp]
abbrev OracleStatement.AfterLinearCombination : R1CS.MatrixIdx ⊕ R1CS.MatrixIdx ⊕ Fin 1 → Type :=
  Sum.elim (EvalClaim R) (OracleStatement.AfterFirstSumcheck R pp)

PMF.uniformOfFintype in Mathlib.Probability.Distributions.Uniform

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

@[inline, specialize]
def add (p q : UniPoly R) : UniPoly R :=
  add_raw p q |> trim

def AlgebraTowerEquiv.algebraMapRightUp (e : AlgebraTowerEquiv A B) (i j : ι)
    (h : i ≤ j) : (A i) →+* (B j) :=

@[inline] def ge [Zero T] [ToNat T] (a b : Cayley T) : Prop :=
  (a : Nat) ≥ (b : Nat)

def getFirstOracle {i : Fin (ℓ + 1)}
    (oStmt : (∀ j, OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i j)) :
    sDomain 𝔽q β h_ℓ_add_R_rate 0 → L :=

@[reducible]
def spec : OracleSpec Unit := fun _ => (α × α, α)

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

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

def LawfulInterleavedCode (κ : Type*) [Fintype κ] (ι : Type*) [Fintype ι]
                          (F : Type*) [Semiring F] :=
  { IC : InterleavedCode κ ι F // IC.isInterleaved }

hδLe : ∀ i : Fin (M + 1),
    (δ i) ≤ 1 - Finset.univ.sup (fun j => BStar i j (C i j) (Gen_α i j).parℓ)

def computeInitialSumcheckPoly (t : MultilinearPoly L ℓ)
    (m : MultilinearPoly L ℓ) : MultiquadraticPoly L ℓ :=
  ⟨m * t, by
    rw [MvPolynomial.mem_restrictDegree_iff_degreeOf_le]
    intro i
    have h_t_deg: degreeOf i t.val ≤ 1 :=
      degreeOf_le_iff.mpr fun term a ↦ (t.property) a i
    have h_m_deg: degreeOf i m.val ≤ 1 :=
      degreeOf_le_iff.mpr fun term a ↦ (m.property) a i
    calc
      _ ≤ (degreeOf i m.val) + (degreeOf i t.val) :=
        degreeOf_mul_le i m.val t.val
      _ ≤ 2 :=

Matrix.vecMul in Mathlib.Data.Matrix.Mul

let mut x := start
  let mut y := x
  let mut d := 1

def multilinearBasis (l r : ℕ) (h_le : l ≤ r) :
    letI instAlgebra : Algebra (BTField l) (BTField r) := binaryAlgebraTower (h_le:=h_le)
    Basis (Fin (2 ^ (r - l))) (BTField l) (BTField r) :=

abbrev eqPolynomial (r : σ → R) : R[X σ] :=
  ∏ i : σ, singleEqPolynomial (r i) (X i)

hEq := fun i => by admit /- proof elided -/

@[reducible, inline, specialize]
def ChallengesUpTo (k : Fin (n + 1)) (pSpec : ProtocolSpec n) : Type :=
  ∀ i, (pSpec.take k k.is_le).Challenge i

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

@[reducible]
def baseFieldSize : Nat :=
  21888242871839275222246405745257275088696311157297823662689037894645226208583

structure FSProverState (U : Type) [SpongeUnit U] (H : Type*) [DuplexSpongeInterface U H]
    (R : Type*) extends FSVerifierState U H where
   
  rng : ProverPrivateRng R
deriving Repr

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

def FullData.EquivIndexFun {α : Type} (s : Skeleton) :
    FullData α s ≃ (SkeletonNodeIndex s → α) where
  toFun := fun tree idx => tree.get idx
  invFun := fun f => FullData.ofFun s f
  left_inv := by admit /- proof elided -/

Mathlib.Linter.TextBased.ErrorFormat.github in Mathlib.Tactic.Linter.TextBased

@[reducible, simp] def OStmtOut : Unit → Type := fun _ => R⦃≤ deg⦄[X]

instance : Fact (Nat.Prime baseFieldSize) := ⟨BaseField_is_prime⟩

Submodule.span in Mathlib.LinearAlgebra.Span.Defs

@[inline, reducible]
def lift : OuterStmtIn × (∀ i, OuterOStmtIn i) → InnerStmtOut × (∀ i, InnerOStmtOut i) →
    OuterStmtOut × (∀ i, OuterOStmtOut i) :=
  lens.toFunB

def rbrSoundness
    (langIn : Set (StmtIn × ∀ i, OStmtIn i))
    (langOut : Set (StmtOut × ∀ i, OStmtOut i))
    (verifier : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec)
    (rbrSoundnessError : pSpec.ChallengeIdx → ℝ≥0) : Prop :=
  verifier.toVerifier.rbrSoundness init impl langIn langOut rbrSoundnessError

List.IsSuffix in Init.Data.List.Basic

instance {s} : Functor (fun α => LeafData α s) where
  map f x := x.map f

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

[width_ne_zero : NeZero width]

@[reducible]
def get {αs : List (Type u)} : HList αs → (n : Fin αs.length) → αs.get n
  | x ::ₕ _, ⟨0, _⟩ => x
  | _ ::ₕ xs, ⟨n+1, h⟩ => xs.get ⟨n, Nat.lt_of_succ_lt_succ h⟩

inductive PrattPart : (p : ℕ) → (a : ZMod p) → ℕ → Prop
  | prime : {p : ℕ} → {a : ZMod p} → (n k nk : ℕ) → n.Prime →
      a ^ ((p - 1) / n) ≠ 1 → n ^ k = nk → PrattPart p a nk
  | split : {p : ℕ} → {a : ZMod p} → {n : ℕ} → (l r : ℕ) →
      PrattPart p a l → PrattPart p a r → l * r = n → PrattPart p a n

@[reducible, inline, specialize]
def Challenges' (pSpec : ProtocolSpec n) : Type :=
  ∀ i, (hi : pSpec.dir i = .V_to_P) → pSpec.«Type» i

def commitKState (i : Fin ℓ) (hCR : isCommitmentRound ℓ ϑ i) :
    (commitOracleVerifier 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
      i hCR).KnowledgeStateFunction init impl
      (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)
      (extractor := commitRbrExtractor 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i) where
  toFun := fun m ⟨stmtIn, oStmtIn⟩ tr witMid =>
    commitKStateProp 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (𝓑 := 𝓑)
      (i := i) (m := m) (stmtIn := stmtIn) (witMid := witMid) (oStmtIn := oStmtIn) (mp:=mp)
  toFun_empty := fun stmtIn witMid => by admit /- proof elided -/

noncomputable instance {v : ι → F} {s : AffineSubspace F (ι → F)} [Fintype s] :
    Fintype (v +ᵥ s) := Fintype.ofFinite ↥(v +ᵥ s)

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

instance : IsEmpty (ChallengeIdx ⟨!v[.P_to_V], !v[Msg]⟩) :=
  ⟨fun ⟨i, h⟩ => by admit /- proof elided -/
  ⟩

def relation (cs : ConstraintSystem 𝓡 numWires numGates) (ℓ : ℕ) (hℓ : ℓ ≤ numWires) :
    (publicInputs : Fin ℓ → 𝓡) → (privateWitness : Fin (numWires - ℓ) → 𝓡) → Prop :=
  fun (x : Fin ℓ → 𝓡) (ω : Fin (numWires - ℓ) → 𝓡) =>
    let combined := Fin.append x ω ∘ Fin.cast (by admit /- proof elided -/
    )
    cs.accepts combined

instance [Oₘ : ∀ i, OracleInterface (pSpec.Message i)] :
    ∀ i, OracleInterface ((pSpec.addSalt Salt).Message i) :=
  fun i => {
    Query := (Oₘ i).Query
    Response := (Oₘ i).Response
    answer := fun msg => (Oₘ i).answer (by admit /- proof elided -/
      )
  }

@[inline, reducible]
def lift : OuterStmtIn × OuterWitIn → InnerStmtOut × InnerWitOut → OuterStmtOut × OuterWitOut :=
  fun ctxIn ctxOut =>
    ⟨lens.stmt.toFunB ctxIn.1 ctxOut.1, lens.wit.toFunB ctxIn ctxOut⟩

noncomputable def generateOpening [Fact (Nat.Prime p)] (srs : Vector G₁ (n + 1))
    (coeffs : Fin (n + 1) → ZMod p) (z : ZMod p) : G₁ :=
  letI poly : degreeLT (ZMod p) (n + 1) := (degreeLTEquiv (ZMod p) (n + 1)).invFun coeffs
  letI q : degreeLT (ZMod p) (n + 1) :=
    ⟨Polynomial.div (poly.val - C (poly.val.eval z)) (X - C z), by admit /- proof elided -/
      ⟩
  commit srs (degreeLTEquiv (ZMod p) (n + 1) q)

protected def cast (R : OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec₁) :
    OracleReduction oSpec StmtIn OStmtIn WitIn StmtOut OStmtOut WitOut pSpec₂ where
  prover := R.prover.cast hn hSpec
  verifier := R.verifier.cast hn hSpec hOₘ

instance {i : OracleMessageIdx pSpec} : OracleInterface (pSpec.Message i) :=
  (inst.oracleInterfaces i).get i.2

Finset.sup in Mathlib.Data.Finset.Lattice.Fold

def generator : BaseField × BaseField := (1, 2)

instance {α : Type} [Sampleable α] : DecidableEq α := inferInstance

def relayKStateProp (i : Fin ℓ) (hNCR : ¬ isCommitmentRound ℓ ϑ i)
  (stmtIn : Statement (L := L) Context i.succ)
  (witMid : Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ)
  (oStmtIn : (∀ j, OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i.castSucc j))
  : Prop :=
  masterKStateProp (mp := mp) (ϑ := ϑ) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (𝓑 := 𝓑)
    (stmtIdx := i.succ) (oracleIdx := i.succ)
    (h_le := le_refl _)
    (stmt := stmtIn) (wit := witMid) (oStmt := mapOStmtOutRelayStep
      𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i hNCR oStmtIn)
    (localChecks := True)

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

instance [ProverFirst pSpec] [h : OracleInterface (pSpec.«Type» 0)] :
    ∀ i, OracleInterface (pSpec.Message i)
  | ⟨0, _⟩ => inferInstance

@[reducible]
def GroupEncodeOracle : OracleSpec Unit := fun _ => (ι, BitVec bitLength)

Nat.ceil in Mathlib.Algebra.Order.Floor.Defs

PrvState := foldPrvState 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i

class Initialize (α : Type u) (β : Type v) where
   
  new : β → α

def foldStepRelOut (i : Fin ℓ) :
    Set ((Statement (L := L) Context i.succ ×
      (∀ j, OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i.castSucc j)) ×
      Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ) :=
  { input | foldStepRelOutProp (mp := mp) (𝓑 := 𝓑) 𝔽q β i input}

MvPolynomial.eval in Mathlib.Algebra.MvPolynomial.Eval

def eval₂ (p : MlPoly R n) (f : R →+* S) (x : Vector S n) : S := eval (map f p) x

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

@[ext]
structure Reduction {ι : Type} (oSpec : OracleSpec ι)
    (StmtIn WitIn StmtOut WitOut : Type) {n : ℕ} (pSpec : ProtocolSpec n) where
  prover : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec
  verifier : Verifier oSpec StmtIn StmtOut pSpec

capacitySegment_output_eq_input : ∀ i : Fin outputState.length,
    outputState[i].capacitySegment = inputState[i.val + 1].capacitySegment

def ofFinMatrix {m n : ℕ} (matrix : _root_.Matrix (Fin m) (Fin n) α) : Matrix α m n :=
  Vector.ofFn (fun i => Vector.ofFn (fun j => matrix i j))

(Vector.flatten chunksAfterDiffusion).cast (params.widthDiv4_mul_4_eq_width)

let st2 := Fin.foldl params.numPartialRounds (fun st_acc rc_idx =>
    let rc_val := rcs[rc_idx]'(sorry)
    let st_new := partialRound params st_acc rc_val
    st_new) st1

def SkeletonNodeIndex.rightChild {s : Skeleton} (idx : SkeletonNodeIndex s) :
    Option (SkeletonNodeIndex s) :=
  match idx with
  | SkeletonNodeIndex.ofLeaf => none
  | @SkeletonNodeIndex.ofInternal left right =>
    some (SkeletonNodeIndex.ofRight (getRootIndex right))
  | SkeletonNodeIndex.ofLeft idxLeft =>
    idxLeft.rightChild.map (SkeletonNodeIndex.ofLeft)
  | SkeletonNodeIndex.ofRight idxRight =>
    idxRight.rightChild.map (SkeletonNodeIndex.ofRight)

st3
</all_available_defs>

<all_available_lemmas>
Polynomial.comp_assoc in Mathlib.Algebra.Polynomial.Eval.Defs
implies_true in Init.SimpLemmas
Fin.coe_ofNat_eq_mod in Mathlib.Data.Fin.Basic
Fin.foldl_succ in Init.Data.Fin.Fold
Fin.val_succ in Init.Data.Fin.Lemmas
Nat.zero_mod in Init.Data.Nat.Div.Basic
Polynomial.X_comp in Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.comp_X in Mathlib.Algebra.Polynomial.Eval.Defs
add_zero in Mathlib.Algebra.Group.Defs
Nat.and_one_is_mod in Init.Data.Nat.Bitwise.Lemmas
Nat.mod_succ in Init.Data.Nat.Lemmas
Nat.mul_add_mod_self_right in Init.Data.Nat.Div.Basic
Nat.shiftRight_zero in Init.Data.Nat.Bitwise.Basic
Polynomial.pow_comp in Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.prod_comp in Mathlib.Algebra.Polynomial.Eval.Defs
pow_one in Mathlib.Algebra.Group.Defs

lemma Xⱼ_zero_eq_one (ℓ : ℕ) (h_ℓ : ℓ ≤ r) :
  Xⱼ 𝔽q β ℓ h_ℓ ⟨0, by exact Nat.two_pow_pos ℓ⟩ = 1

lemma getBit_eq_succ_getBit_of_mul_two_add_one {n k : ℕ} : getBit (k+1) (2*n + 1) = getBit k n

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

theorem mul_two_add_bit_lt_two_pow (a b c : ℕ) (i : Fin 2)
    (h_a : a < 2 ^ b) (h_b : b < c) :
    a * 2 + i.val < 2^c

lemma lt_two_pow_of_lt_two_pow_exp_le (x i j: ℕ)
    (h_x_lt_2_pow_i: x < 2^i) (h_i_le_j: i ≤ j): x < 2^j

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

@[simp]
theorem fappend_zero {β : Fin m → A} {α : Fin 0 → A}
    (u : (i : Fin m) → F (β i)) :
    fappend u (!h⦃F⦄⟨α⟩[] : (i : Fin 0) → F (α i)) = u

@[simp]
theorem reduction_completeness (h : init.neverFails) [Nonempty σ] :
    (reduction oSpec Statement pred).perfectCompleteness init impl
    (relIn Statement pred) (relOut Statement)

omit [Finite F] in
private lemma gen_def {i : ℕ} :
    (IsCyclicWithGen.gen : evalDomain D i) =
      ⟨
        DIsCyclicC.gen ^ (2 ^ i),
        by
          apply pow_2_pow_i_mem_Di_of_mem_D
          exact DIsCyclicC.gen.2
      ⟩

@[simp]
theorem reduction_completeness (h : init.neverFails) :
    (reduction oSpec Statement Witness).perfectCompleteness init impl relIn (toRelOut relIn)

@[simp]
theorem poly_form (k : ℕ) : poly k = X^2 + (C (Z k) * X + 1)

@[simp]
lemma halfNumFullRounds_mul_2_eq_numFullRounds :
    params.halfNumFullRounds * 2 = params.numFullRounds

lemma listBlock_subset_listHamming
  (i k : ℕ) {S : Finset ι} {φ : ι ↪ F} {φ' : (indexPowT S φ i) ↪ F}
  {m : ℕ} [DecidableEq F] [DecidableEq ι] [Smooth φ]
  (f : (indexPowT S φ i) → F) (S' : Finset (indexPowT S φ i))
  [h_fintype : ∀ i : ℕ, Fintype (indexPowT S φ i)] [DecidableEq (indexPowT S φ i)] [Smooth φ']
  (C : Set ((indexPowT S φ i) → F)) (hcode : C = smoothCode φ' m)
  [h_dec : DecidableBlockDisagreement i k f S' φ']
  (δ : ℝ≥0) (hδLe : δ ≤ 1) :
  Λᵣ(i, k, f, S', C, hcode, δ) ⊆ relHammingBall C f δ

@[simp]
lemma OracleReduction.append_toReduction
    (R₁ : OracleReduction oSpec Stmt₁ OStmt₁ Wit₁ Stmt₂ OStmt₂ Wit₂ pSpec₁)
    (R₂ : OracleReduction oSpec Stmt₂ OStmt₂ Wit₂ Stmt₃ OStmt₃ Wit₃ pSpec₂) :
      (OracleReduction.append R₁ R₂).toReduction =
        Reduction.append R₁.toReduction R₂.toReduction

@[simp]
lemma eval_solutionToE {x : F} :
  eval x (solutionToE e k v) = x ^ e + ∑ y : Fin e, v ⟨y, by omega⟩ * x ^ y.1

lemma concentration_bounds {deg : ℕ} {domain : ι ↪ F}
  {U : AffineSubspace F (ι → F)} [Nonempty U]
  (hdiv_pos : 0 < (divergence U (RScodeSet domain deg) : ℝ≥0))
  (hdiv_lt : (divergence U (RScodeSet domain deg) : ℝ≥0) < 1 - ReedSolomonCode.sqrtRate deg domain)
  : let δ' := divergence U (RScodeSet domain deg)
    Pr_{let u ← $ᵖ U}[Code.relHammingDistToCode u (RScodeSet domain deg) ≠ δ']
    ≤ errorBound δ' deg domain

theorem unique_repr {R : Type*} [CommRing R] {S : Type*} [CommRing S] [Algebra R S]
    (pb : PowerBasis R S) (repr1 repr2 : Fin pb.dim →₀ R)
    (h : ∑ i : Fin pb.dim, repr1 i • pb.basis i = ∑ i : Fin pb.dim, repr2 i • pb.basis i) :
    repr1 = repr2

@[simp]
theorem vconcat_castSucc (v : Fin n → α) (a : α) (i : Fin n) :
    vconcat v a (castSucc i) = v i

theorem novelToMonomial_monomialToNovel_inverse
  (ℓ : ℕ) (h_ℓ : ℓ ≤ r) :
  ∀ coeffs : Fin (2^ℓ) → L,
    monomialToNovelCoeffs 𝔽q β ℓ h_ℓ
      (novelToMonomialCoeffs 𝔽q β ℓ h_ℓ coeffs) = coeffs

theorem snoc_ne_zero_of_right (h : y ≠ 0) : snoc s y ≠ 0

theorem is_prime : Nat.Prime fieldSize

theorem distEq_trans (mx my mz : OracleComp spec α)
    (hxy : distEq mx my) (hyz : distEq my mz) : distEq mx mz

@[simp]
theorem addCases'_left {m n : ℕ} {α : Fin m → Sort u} {β : Fin n → Sort u}
    (left : (i : Fin m) → α i) (right : (j : Fin n) → β j) (i : Fin m) :
      addCases' left right (Fin.castAdd n i) = (Fin.append_left α β i) ▸ (left i)

lemma add_descends [LawfulBEq R] (a₁ b₁ a₂ b₂ : UniPoly R) :
  equiv a₁ a₂ → equiv b₁ b₂ → add_descending a₁ b₁ = add_descending a₂ b₂

@[simp]
lemma domain_def : (spec α).domain () = (α × α)

lemma zsmul_neg' {k : ℕ} (n : ℕ) (a : ConcreteBTField k) :
  (if ((Int.negSucc n) : ℤ) % (2 : ℤ) = (0 : ℤ) then zero else a) =
    neg (if (↑n.succ : ℤ) % (2 : ℤ) = (0 : ℤ) then zero else a)

lemma rtake_eq_rtake : transcript⟦m:⟧ = transcript.drop m h

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

theorem liftContext_perfectCompleteness
    (h : R.perfectCompleteness init impl innerRelIn innerRelOut) :
      (R.liftContext lens).perfectCompleteness init impl outerRelIn outerRelOut

private lemma solutionToE_from_E
  (h_p_deg : p.natDegree < k)
  (h_dist : (Δ₀(f, p.eval ∘ ωs) : ℕ) ≤ e)
  : solutionToE e k (E_and_Q_to_a_solution e (E ωs f p e) (Q ωs f p e)) = E ωs f p e

lemma separable_iff_discr_eq_zero {F : Type} [Field F] [Inhabited F] (f : F[X]) :
  f.Separable ↔ discriminant f ≠ 0

theorem BerlekampWelchCondition_iff_Solution {e k : ℕ} [NeZero n]
  {ωs f : Fin n → F} {v : Fin (2 * e + k) → F}
  :
  IsBerlekampWelchSolution e k ωs f v
  ↔
  (BerlekampWelchCondition e k ωs f (solutionToE e k v) (solutionToQ e k v))

protected lemma elocPoly_congr {ωs' f' : ℕ → F}
  (h₁ : ∀ {m}, m < n → ωs m = ωs' m) (h₂ : ∀ {m}, m < n → f m = f' m) :
  ElocPoly n ωs f = ElocPoly n ωs' f'

theorem append_comp' {a : Fin m → α} {b : Fin n → α} (f : α → β)
    (i : Fin (m + n)) : append (f ∘ a) (f ∘ b) i = f (append a b i)

lemma oracle_block_k_next_le (i : Fin (ℓ + 1)) (j : Fin (toOutCodewordsCount ℓ ϑ i))
    (hj : j.val + 1 < toOutCodewordsCount ℓ ϑ i) : j.val * ϑ + ϑ ≤ i

lemma runWithOracle_getPutativeRoot {s} (idx : BinaryTree.SkeletonLeafIndex s)
    (leafValue : α) (proof : List α) (f) :
    (runWithOracle f (getPutativeRoot idx leafValue proof))
      =
    getPutativeRoot_with_hash idx leafValue proof fun (left right : α) => (f () ⟨left, right⟩)

lemma exist_bit_diff_if_diff {n: ℕ} (a: Fin (2^n)) (b: Fin (2^n)) (h_a_ne_b: a ≠ b):
  ∃ k: Fin n, getBit k a ≠ getBit k b

theorem is_fiber_iff_generates_quotient_point (i : Fin ℓ) (steps : ℕ)
    (h_i_add_steps : i.val + steps ≤ ℓ)
    (x : sDomain 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩))
    (y : sDomain 𝔽q β h_ℓ_add_R_rate (i := ⟨i.val + steps, by omega⟩)) :
    let qMapFiber := qMap_total_fiber 𝔽q β (i := ⟨i, by omega⟩) (steps := steps)
      (h_i_add_steps := by simp only; exact fin_ℓ_steps_lt_ℓ_add_R i steps h_i_add_steps) (y := y)
    let k := pointToIterateQuotientIndex (i := ⟨i, by omega⟩) (steps := steps)
      (h_i_add_steps := h_i_add_steps) (x := x)
    y = iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i (k := steps) (h_bound := h_i_add_steps) x ↔
    qMapFiber k = x

@[simp]
lemma getTypes_nil : getTypes [] = []

theorem coeff_eq_getElem_of_lt [LawfulBEq R] {p : UniPoly R} {i} (hi : i < p.size) :
  p.trim.coeff i = p[i]

theorem append_comp {a : Fin m → α} {b : Fin n → α} (f : α → β) :
    append (f ∘ a) (f ∘ b) = f ∘ append a b

@[simp]
lemma Rhs_zero_eq_neg' : Rhs 0 ωs f = -f

@[simp]
protected lemma elocPolyF_eq_elocPoly :
  ElocPolyF (n := n) (liftF' ωs) (liftF' f) = ElocPoly n ωs f

lemma cast_join {k n : ℕ} (h_pos : k > 0) (hi lo : ConcreteBTField (k - 1)) (heq : k = n) :
  join (k:=k) h_pos hi lo = cast (by rw [heq])
    (join (k:=n) (by omega) (cast (by subst heq; rfl) hi) (lo:=cast (by subst heq; rfl) lo))

omit [NeZero ϑ] hdiv in
lemma toOutCodewordsCountOf0 : toOutCodewordsCount ℓ ϑ 0 = 1

theorem FullTranscript.mk2_eq_snoc_snoc {pSpec : ProtocolSpec 2} (msg0 : pSpec.«Type» 0)
    (msg1 : pSpec.«Type» 1) :
      FullTranscript.mk2 msg0 msg1 = ((default : pSpec.Transcript 0).concat msg0).concat msg1

@[simp]
theorem drop_apply (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin (n - m)) :
    (drop m h v) i = v (Fin.cast (Nat.sub_add_cancel h) (addNat i m))

@[simp]
lemma deevenize_coeff {f : Polynomial F} {n : ℕ} :
    (deevenize f).coeff n = f.coeff (2 * n)

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

theorem vflatten_eq_vappend_last {m : ℕ} {n : Fin (m + 1) → ℕ}
    {v : (i : Fin (m + 1)) → Fin (n i) → α} :
    vflatten v =
      vappend (vflatten (fun i => v i.castSucc)) (v (last _)) ∘ Fin.cast vsum_castSucc

@[simp]
theorem dconcat_last {motive : Fin (n + 1) → Sort u} (v : (i : Fin n) → motive (castSucc i))
    (a : motive (last n)) : (v :+ᵈ⟨motive⟩ a) (last n) = a

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

@[simp]
theorem dflatten_embedSum {m : ℕ} {n : Fin m → ℕ} {motive : (k : Fin (vsum n)) → Sort*}
    (v : (i : Fin m) → (j : Fin (n i)) → motive (embedSum i j)) (i : Fin m) (j : Fin (n i)) :
    dflatten (motive := motive) v (embedSum i j) = v i j

lemma galois_eval_in_BTField
    {curBTField : Type*} [Field curBTField]
    (u : curBTField) (t1 : curBTField) -- here t1 is already lifted to curBTField
    (k : ℕ)
    (sumZeroIffEq : ∀ (x y : curBTField), x + y = 0 ↔ x = y)
    (prevSpecialElementNeZero : t1 ≠ 0)
    (u_plus_inv_eq_t1 : u + u⁻¹ = t1)
    (h_u_square : u^2 = u*t1 + 1)
    (h_t1_pow : t1^(2^(2^k)-1) = 1 ∧ (t1⁻¹)^(2^(2^k)-1) = 1)
    (h_t1_pow_2_pow_2_pow_k :  t1^(2^(2^k)) = t1)
    (h_t1_inv_pow_2_pow_2_pow_k :  (t1⁻¹)^(2^(2^k)) = t1⁻¹)
    (trace_map_at_inv : ∑ i ∈ Finset.range (2 ^ k), t1⁻¹ ^ (2 ^ i) = 1) :
    u^(2^(2^k)) = u⁻¹

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

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

theorem oddRefinement_eq_novel_poly_of_1_leading_suffix (i : Fin ℓ) (v : Fin (2 ^ i.val))
    (original_coeffs : Fin (2 ^ ℓ) → L) :
    have h_v: v.val ||

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

lemma extract_start_zero_eq_take {n : ℕ} {α : Fin n → Sort*} (stop : ℕ) (h : stop ≤ n)
    (v : (i : Fin n) → α i) : extract 0 stop (Nat.zero_le _) h v = take stop h v

theorem is_prime : Nat.Prime fieldSize

@[simp]
theorem Set.mem_language_iff {α β} (rel : Set (α × β)) (stmt : α) :
    stmt ∈ rel.language ↔ ∃ wit, (stmt, wit) ∈ rel

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)

theorem Nat.shiftRight_eq_sub_mod_then_div_two_pow {n lo_len : ℕ} :
  n >>> lo_len = (n - n % 2 ^ lo_len) / 2 ^ lo_len

private lemma le_sum_sum_choose_K [Zero F]
  (h_n : 0 < n)
  (h_B : B.card ≠ 0)
  (h_card : 2 ≤ Fintype.card F)
  :
  n * (choose_2 (k B) + (Fintype.card (α := F) - 1)
    * choose_2 ((B.card - k B) / ((Fintype.card (α := F) - 1))))
  ≤ ∑ i, sum_choose_K_i B i

theorem succ_mul {a b : AssocNat} : (succ a) * b = a * b + b

omit [Fintype σ] in
theorem singleEqPolynomial_degreeOf (r : R) (i j : σ) :
    degreeOf i (singleEqPolynomial r (X j)) ≤ if i = j then 1 else 0

theorem toNat_ofNat (n : ℕ) : toNat (ofNat n) = n

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

theorem nsmul_succ [LawfulBEq R] (n : ℕ) {p : UniPoly R} : nsmul (n + 1) p = nsmul n p + p

lemma cast_mul (m n : ℕ) {x y : ConcreteBTField m} (h_eq : m = n) :
  (cast (by exact cast_ConcreteBTField_eq m n h_eq) (x * y)) =
  (cast (by exact cast_ConcreteBTField_eq m n h_eq) x) *
  (cast (by exact cast_ConcreteBTField_eq m n h_eq) y)

theorem natDegree_finSuccEquivNth (f : MvPolynomial (Fin (n + 1)) R) :
    (finSuccEquivNth R p f).natDegree = degreeOf p f

theorem congrArg₃ {α β γ δ : Sort*} {f : α → β → γ → δ} {a a' : α} {b b' : β} {c c' : γ}
    (h : a = a') (h' : b = b') (h'' : c = c') : f a b c = f a' b' c'

theorem rightpad_getElem_eq_getD {a : Array α} {n : Nat} {unit : α} {i : Nat}
    (h : i < (a.rightpad n unit).size) : (a.rightpad n unit)[i] = a.getD i unit

theorem toImpl_toPoly [LawfulBEq R] (p : UniPoly R) : p.toPoly.toImpl = p.trim

let listBlock : Set ((indexPowT S φ 0) → F) := Λᵣ(0, k, f, S', C, hcode, δ)
                      let fold := fold_k f αs hLe
                      let foldSet := fold_k_set listBlock αs hLe
                      let kFin : Fin (k + 1) := ⟨k, Nat.lt_succ_self k⟩
                      let Cₖ := (params.Gen_α kFin).C
                      let listHamming := relHammingBall Cₖ fold δ

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

@[simp] lemma toMvPolynomialAlgHom_X (s : σ) :
    toMvPolynomialAlgHom (X s : P) = (MvPolynomial.X s : MvPolynomial σ R)

@[simp]
theorem rightpad_apply_ge (n : ℕ) (a : α) (v : Fin m → α) (i : Fin n)
    (h : m ≤ i.val) : rightpad n a v i = a

theorem fappend_ext {α : Fin m → A} {β : Fin n → A}
    (u₁ u₂ : (i : Fin m) → F (α i)) (v₁ v₂ : (i : Fin n) → F (β i)) :
    fappend u₁ v₁ = fappend u₂ v₂ ↔ u₁ = u₂ ∧ v₁ = v₂

omit [DecidableEq 𝔽q] hF₂ in
lemma initial_tiled_coeffs_correctness (h_ℓ : ℓ ≤ r) (a : Fin (2 ^ ℓ) → L) :
    let b: Fin (2^(ℓ + R_rate)) → L := tileCoeffs a
    additiveNTTInvariant 𝔽q β h_ℓ_add_R_rate b a (i := ⟨ℓ, by omega⟩)

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

theorem cast_run (stmt : StmtIn) (wit : WitIn)
    (P : Prover oSpec StmtIn WitIn StmtOut WitOut pSpec₁) :
    P.run stmt wit =
      cast (sorry) ((P.cast hn hSpec).run stmt wit)

lemma twoAdicGenerator_unit_mem_rootsOfUnity
    (bits : Fin (twoAdicity + 1)) (h : twoAdicGenerators[bits] ≠ 0) :
    Units.mk0 (twoAdicGenerators[bits]) h ∈ rootsOfUnity (2 ^ (bits : Nat)) (Field)

theorem snoc_left_injective : Injective (Finsupp.snoc · y : (Fin n →₀ M) → Fin (n + 1) →₀ M)

omit [Finite F] in
lemma dom_n_eq_triv : evalDomain D n = ⊥

theorem eq_iff_split_eq {k : ℕ} (h_pos : k > 0) (x₀ x₁ : ConcreteBTField k) :
  x₀ = x₁ ↔ (split h_pos x₀ = split h_pos x₁)

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

@[simp] theorem zero_add {a : AssocNat} : 0 + a = a

@[simp]
theorem oracleReduction_completeness (h : init.neverFails)
    (hRel : ∀ stmtIn oStmtIn witIn,
      ((stmtIn, oStmtIn), witIn) ∈ relIn →
      ((mapStmt stmtIn, mapOStmt embedIdx hEq oStmtIn), mapWit stmtIn witIn) ∈ relOut) :
    (oracleReduction oSpec mapStmt mapWit embedIdx hEq).perfectCompleteness init impl
      relIn relOut

Nat.pos_of_neZero in Init.Data.Nat.Basic

theorem append_completeness (R₁ : OracleReduction oSpec Stmt₁ OStmt₁ Wit₁ Stmt₂ OStmt₂ Wit₂ pSpec₁)
    (R₂ : OracleReduction oSpec Stmt₂ OStmt₂ Wit₂ Stmt₃ OStmt₃ Wit₃ pSpec₂)
    {completenessError₁ completenessError₂ : ℝ≥0}
    (h₁ : R₁.completeness init impl rel₁ rel₂ completenessError₁)
    (h₂ : R₂.completeness init impl rel₂ rel₃ completenessError₂) :
      (R₁.append R₂).completeness init impl
        rel₁ rel₃ (completenessError₁ + completenessError₂)

Nat.mul_le_mul_right in Init.Data.Nat.Basic

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

lemma xor_eq_sub_iff_submask {n m : ℕ} (h: m ≤ n) : n ^^^ m = n - m ↔ n &&& m = m

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

@[simp]
theorem dflatten_zero {n : Fin 0 → ℕ} {motive : (k : Fin (vsum n)) → Sort*}
    {v : (i : Fin 0) → (j : Fin (n i)) → motive (embedSum i j)} :
    dflatten (motive := motive) v = fun k => Fin.elim0 k

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

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 support_finSuccEquivNth (f : MvPolynomial (Fin (n + 1)) R) :
    (finSuccEquivNth R p f).support = Finset.image (fun m : Fin (n + 1) →₀ ℕ => m p) f.support

theorem vcons_injective2 : Function.Injective2 (@vcons α n)

@[simp]
lemma degreeY_monomialXY {n m : ℕ} {a : F} (ha : a ≠ 0) :
  natDegreeY (monomialXY n m a) = m

@[csimp] lemma dfoldr_eq_dfoldr' : @dfoldr = @dfoldr'

@[simp]
theorem toNat_succ (n : ChurchNat ℕ) : toNat (succ n) = n.toNat.succ
</all_available_lemmas>

<local_ctx>
import ArkLib.Data.FieldTheory.AdditiveNTT.NovelPolynomialBasis

import Mathlib.Tactic

import Mathlib.Data.Finsupp.Defs

import Mathlib.LinearAlgebra.LinearIndependent.Defs

open Polynomial AdditiveNTT Module

namespace AdditiveNTT

variable {r : ℕ} [NeZero r]

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

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

variable [Algebra 𝔽q L]

variable (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)]
  [h_β₀_eq_1 : Fact (β 0 = 1)]

variable {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r)-- ℓ ∈ {1, ..., r-1}

section IntermediateStructures

noncomputable def qMap (i : Fin r) : L[X] :=
  let constMultiplier := ((W 𝔽q β i).eval (β i))^(Fintype.card 𝔽q)
    / ((W 𝔽q β (i + 1)).eval (β (i + 1)))
  C constMultiplier * ∏ c: 𝔽q, (X - C (algebraMap 𝔽q L c))

noncomputable section DomainBijection

end DomainBijection

noncomputable def intermediateNormVpoly
    
    (i: Fin (ℓ+1)) (k : Fin (ℓ - i + 1)) : L[X] :=
  
  Fin.foldl (n:=k) (fun acc j =>
    (qMap 𝔽q β ⟨(i : ℕ) + (j : ℕ), by admit /- proof elided -/
    ⟩).comp acc) (X)

noncomputable def intermediateNovelBasisX (i : Fin (ℓ + 1)) (j : Fin (2 ^ (ℓ - i))) : L[X] :=
  (Finset.univ: Finset (Fin (ℓ - i)) ).prod (fun k =>
    (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate i (k:=⟨k, by admit /- proof elided -/
    ⟩)) ^ (Nat.getBit k j))
</local_ctx>

<target_theorem>
lemma odd_index_intermediate_novel_basis_decomposition
    (i : Fin ℓ) (j : Fin (2 ^ (ℓ - i - 1))) :
    intermediateNovelBasisX 𝔽q β h_ℓ_add_R_rate ⟨i, by omega⟩ ⟨j * 2 + 1, by
      apply mul_two_add_bit_lt_two_pow j (ℓ-i-1) (ℓ-i) ⟨1, by omega⟩ (by omega) (by omega)
    ⟩  = X * (intermediateNovelBasisX 𝔽q β h_ℓ_add_R_rate ⟨i+1, by omega⟩ ⟨j, by
      apply lt_two_pow_of_lt_two_pow_exp_le j (ℓ-i-1) (ℓ-(i+1)) (by omega) (by omega)
    ⟩).comp (qMap 𝔽q β ⟨i, by omega⟩) :=
</target_theorem>

