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
Algebra in Mathlib.Algebra.Algebra.Defs
Field in Mathlib.Algebra.Field.Defs
IsLinearMap in Mathlib.Algebra.Module.LinearMap.Defs
toFun in ToMathlib.Control.Monad.Hom
Submodule.map in Mathlib.Algebra.Module.Submodule.Map
Module.Basis in Mathlib.LinearAlgebra.Basis.Defs
Disjoint in Mathlib.Order.Disjoint
Fact in Mathlib.Logic.Basic
LinearEquiv in Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.ofBijective in Mathlib.Algebra.Module.Submodule.Equiv
LinearIndependent in Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearMap in Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.codRestrict in Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.ker in Mathlib.Algebra.Module.Submodule.Ker
Module.Basis.span in Mathlib.LinearAlgebra.Basis.Basic
Set.range in Mathlib.Data.Set.Operations
Submodule.subtype in Mathlib.Algebra.Module.Submodule.LinearMap
Subtype in Init.Prelude
Finsupp in Mathlib.Data.Finsupp.Defs
Finsupp.equivFunOnFinite in Mathlib.Data.Finsupp.Defs
Finset in Mathlib.Data.Finset.Defs
Finset.univ in Mathlib.Data.Fintype.Defs
Ne in Init.Core
NeZero in Init.Data.NeZero
DecidableEq in Init.Prelude
Inhabited in Init.Prelude
Repr in Init.Data.Repr
Fin.cast in Init.Data.Fin.Basic
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
Polynomial in Mathlib.Algebra.Polynomial.Basic
Set.univ in Mathlib.Data.Set.Defs
reduceDIte in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
Module in Mathlib.Algebra.Module.Defs
Nat.succ in Init.Prelude
Polynomial.eval in Mathlib.Algebra.Polynomial.Eval.Defs
Decidable in Init.Prelude
Eq in Init.Prelude
id in Init.Prelude

noncomputable def sDomain (i : Fin r) : Subspace 𝔽q L :=
  let W_i_norm := normalizedW 𝔽q β i
  let h_W_i_norm_is_additive : IsLinearMap 𝔽q (fun x : L => W_i_norm.eval x) :=
    AdditiveNTT.normalizedW_is_additive 𝔽q β i
  Submodule.map (polyEvalLinearMap W_i_norm h_W_i_norm_is_additive)
    (U 𝔽q β ⟨ℓ + R_rate, h_ℓ_add_R_rate⟩)

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

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

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

noncomputable def polyEvalLinearMap {L 𝔽q : Type*} [Field L] [Field 𝔽q] [Algebra 𝔽q L]
  (p : L[X]) (hp_add : IsLinearMap 𝔽q (fun x : L => p.eval x)) : L →ₗ[𝔽q] L :=
{
  toFun    := fun x => p.eval x,
  map_add' := hp_add.map_add,
  map_smul' := hp_add.map_smul
}

noncomputable def sDomain_basis (i : Fin r) (h_i : i < ℓ + R_rate) :
    Basis (Fin (ℓ + R_rate - i)) 𝔽q (
      sDomain 𝔽q β h_ℓ_add_R_rate i) :=

def sBasis (i : Fin r) (h_i : i < ℓ + R_rate) : Fin (ℓ + R_rate - i) → L :=
  fun k => β ⟨i + k.val, by admit /- proof elided -/
  ⟩

def binaryFinMapToNat {n : ℕ} (m : Fin n → ℕ) (h_binary : ∀ j: Fin n, m j ≤ 1) : Fin (2^n) :=

def symm (eqv : Equiv pSpec pSpec') : Equiv pSpec' pSpec where
  round_eq := eqv.round_eq.symm
  dir_eq := fun i => by admit /- proof elided -/

@[ext]
structure Equiv {m n : ℕ} (pSpec : ProtocolSpec m) (pSpec' : ProtocolSpec n) where
  round_eq : m = n
  dir_eq : ∀ i, pSpec.dir i = pSpec'.dir (Fin.cast round_eq i)
  typeEquiv : ∀ i, pSpec.«Type» i ≃ pSpec'.«Type» (Fin.cast round_eq i)

@[ext]
structure ProtocolSpec (n : ℕ) where
   
  dir : Fin n → Direction
   
  «Type» : Fin n → Type
deriving Inhabited

inductive Direction where
  | P_to_V  
  | V_to_P 
deriving DecidableEq, Inhabited, Repr

noncomputable def iteratedQuotientMap (i : Fin ℓ) (k : ℕ)
    (h_bound : i.val + k ≤ ℓ) (x : (sDomain 𝔽q β
    h_ℓ_add_R_rate) ⟨i, by omega⟩) :
    (sDomain 𝔽q β h_ℓ_add_R_rate) ⟨i.val + k, by omega⟩ :=

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

def trans (eqv : Equiv pSpec pSpec') (eqv' : Equiv pSpec' pSpec'') : Equiv pSpec pSpec'' where
  round_eq := eqv.round_eq.trans eqv'.round_eq
  dir_eq := fun i => by admit /- proof elided -/

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

@[elab_as_elim] def Fin.succRecOnSameFinType {motive : Fin r → Sort _}
    (zero : motive (0 : Fin r))
    (succ : ∀ i : Fin r, i + 1 < r → motive i → motive (i + 1)) : ∀ (i : Fin r), motive i
  | ⟨0, _⟩ => by admit /- proof elided -/
  | ⟨Nat.succ i_val, h⟩ => by admit /- proof elided -/

noncomputable def intermediateEvaluationPoly (i : Fin (ℓ + 1))
    (coeffs : Fin (2 ^ (ℓ - i)) → L) : L[X] :=
  ∑ (⟨j, hj⟩: Fin (2^(ℓ-i))), C (coeffs ⟨j, by admit /- proof elided -/
  ⟩) *
    (intermediateNovelBasisX 𝔽q β h_ℓ_add_R_rate i ⟨j, by admit /- proof elided -/
    ⟩)

@[reducible]
def C : R →+* P := algebraMap R P

def srSoundnessGame (P : Prover.StateRestoration.Soundness oSpec StmtIn pSpec) :
    OracleComp (oSpec ++ₒ (srChallengeOracle StmtIn pSpec))
      (pSpec.FullTranscript × StmtIn) := do
  let ⟨stmtIn, messages⟩ ← P
  let transcript ← messages.deriveTranscriptSR stmtIn
  return ⟨transcript, stmtIn⟩

def drop {n : ℕ} {α : Fin n → Sort*} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) :
    (i : Fin (n - m)) → α (Fin.cast (Nat.sub_add_cancel h) (addNat i m)) :=
  fun i ↦ v (Fin.cast (Nat.sub_add_cancel h) (addNat i m))

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

@[inline, reducible]
protected def id :
    Statement.Lens OuterStmtIn OuterStmtOut OuterStmtIn OuterStmtOut :=
  PFunctor.Lens.id _

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

δ : Fin (M + 1) → ℝ≥0
  dist : (i : Fin (M + 1)) → Fin ((P.foldingParam i) + 1) → ℝ≥0

@[reducible]
def combineMap : StmtIn × WitIn → OracleComp oSpec (StmtOut × WitOut) :=
  fun ⟨stmt, wit⟩ => do return (← mapStmt stmt, ← mapWit stmt wit)

Set.Finite in Mathlib.Data.Finite.Defs

def foldPrvState (i : Fin ℓ) : Fin (2 + 1) → Type := fun
  
  | ⟨0, _⟩ => (Statement (L := L) Context i.castSucc ×
    (∀ 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.castSucc)
  
  | ⟨1, _⟩ => Statement (L := L) Context i.castSucc ×
    (∀ 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.castSucc × L⦃≤ 2⦄[X]
  
  | _ => Statement (L := L) Context i.castSucc ×
    (∀ 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.castSucc × L⦃≤ 2⦄[X] × L

let stmtOut : FinalSumcheckStatementOut (L := L) (ℓ := ℓ) := {
      ctx := stmtIn.ctx,
      sumcheck_target := eq_tilde_eval * c, 
      challenges := stmtIn.challenges,
      final_constant := c
    }
    pure stmtOut

Finset.filter in Mathlib.Data.Finset.Filter

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

def powContraction :
  MvPolynomial (Fin m) F →ₗ[F] Polynomial F :=
  powAlgHom.toLinearMap

Finset.Iic in Mathlib.Order.Interval.Finset.Defs

Polynomial.natDegree in Mathlib.Algebra.Polynomial.Degree.Definitions

List.idxOf in Init.Data.List.Basic

instance : SubSpec [pSpec₂.Challenge]ₒ ([(pSpec₁ ++ₚ pSpec₂).Challenge]ₒ) where
  monadLift | query i t => instSubSpecOfProtocolSpecAppendChallenge.monadLift (query (Sum.inr i) t)

class IsCyclicWithGen (G : Type) [Pow G ℤ] where
  gen : G
  zpow_surjective : Function.Surjective (gen ^ · : ℤ → G)

def collisionPerm : Prop :=
  collisionFwdFwd trace ∨ collisionBwdBwd trace ∨ collisionFwdBwd trace ∨ collisionBwdFwd trace

def CEmbedding : R ↪ MvPolynomial σ R := ⟨C, C_injective σ R⟩

@[reducible, inline, specialize]
def getChallenge (pSpec : ProtocolSpec n) (i : pSpec.ChallengeIdx) :
    OracleComp ([pSpec.Challenge]ₒ'challengeOracleInterface) (pSpec.Challenge i) :=
  (query i () : OracleQuery ([pSpec.Challenge]ₒ'challengeOracleInterface) (pSpec.Challenge i))

Module.Basis.smulTower in Mathlib.RingTheory.AlgebraTower

def Function.interleave₂ {α β : Type*} (u v : α → β) : (Fin 2) × α → β :=
  Function.uncurry (fun a => if a = 0 then u else v)

def bool (j : Fin numWires) : Gate 𝓡 numWires :=
  { qL := -1, qR := 0, qO := 0, qM := 1, qC := 0, a := j, b := j, c := j }

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

protected def basis : F := sorry

Finset.max in Mathlib.Data.Finset.Max

def finUInt8Equiv : Fin (2 ^ 8) ≃ UInt8 where
  toFun := fun i => UInt8.ofFin i
  invFun := fun u => u.toFin
  left_inv _ := rfl
  right_inv _ := rfl

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

verify : StmtIn → (∀ i, pSpec.Challenge i) →
    List ((i : ιₛᵢ) × ((Oₛᵢ i).Query × (Oₛᵢ i).Response)) →
    List ((i : pSpec.MessageIdx) × ((Oₘ i).Query × (Oₘ i).Response)) → OracleComp oSpec StmtOut

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

AddGroup in Mathlib.Algebra.Group.Defs

OracleComp.inductionOn in VCVio.OracleComp.OracleComp

alias E_h := capacitySegmentDupHash

def AlgebraTowerEquiv.toAlgebraOverLeft (e : AlgebraTowerEquiv A B) (i j : ι)
    (h : i ≤ j) : Algebra (A i) (B j) :=

abbrev Size.n_x : ℕ := sz.n - sz.n_w

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

@[inline]
def neg [Neg R] (p : MlPolyEval R n) : MlPolyEval R n := p.map (fun a => -a)

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

def getFoldingChallenges (i : Fin (ℓ + 1)) (challenges : Fin i → L)
    (k : ℕ) (h : k + ϑ ≤ i) : Fin ϑ → L :=
  fun cId => challenges ⟨k + cId, by admit /- proof elided -/
  ⟩

def fappend {A : Sort u} {F : A → Sort v} {m n : ℕ} {α : Fin m → A} {β : Fin n → A}
    (u : (i : Fin m) → F (α i)) (v : (i : Fin n) → F (β i)) :
    (i : Fin (m + n)) → F (Fin.vappend α β i) :=
  match n with
  | 0 => u
  | k + 1 => fconcat (fappend u (fun i => v (Fin.castSucc i))) (v (Fin.last k))

instance : Repr ByteArray where
  reprPrec b n := List.repr b.toList n

@[simp]
abbrev LinearCombinationChallenge : Type := R1CS.MatrixIdx → R

abbrev sqrtRate [Fintype ι] (deg : ℕ) (domain : ι ↪ F) : ℝ≥0 :=
  (LinearCode.rate (ReedSolomon.code domain deg) : ℝ≥0).sqrt

input := id

def squeezeUnchecked [Permute C] (sponge : DuplexSponge U C) (arr : Array U) :
    DuplexSponge U C × Array U :=
  simulateQ' (m := Id) forwardPermutationOracleImpl (squeezeInto sponge arr) (by admit /- proof elided -/
  )

instance : ∀ i, SelectableType (↑(sDomain 𝔽q β h_ℓ_add_R_rate i)) := fun i => sorry

structure ProximityGenerator
  (ι : Type) [Fintype ι] [Nonempty ι]
  (F : Type) [Semiring F] [Fintype F] [DecidableEq F] where
  
  C : LinearCode ι F
  
  parℓ : Type
  hℓ : Fintype parℓ
  
  Gen : Finset (parℓ → F)
  Gen_nonempty : Nonempty Gen
  
  rate : ℝ
  
  B : (LinearCode ι F) → Type → ℝ
  
  err : (LinearCode ι F) → Type → ℝ → ENNReal
   
  proximity:
    ∀ (f : parℓ → ι → F)
      (δ : ℝ≥0) 
      (_hδ : 0 < δ ∧ δ < 1 - (B C parℓ)) ,
      Pr_{ let r ← $ᵖ Gen }[ (proximityCondition f δ r C) ] > (err C parℓ δ) →
        ∃ S : Finset ι,
          S.card ≥ (1 - δ) * (Fintype.card ι) ∧
        ∀ i : parℓ, ∃ u ∈ C, ∀ x ∈ S, f i x = u x

instDecidableEqOfLawfulBEq in Init.Core

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

@[reducible, simp]
def toRelOut : Set ((Statement × Witness) × Unit) :=
  Prod.fst ⁻¹' relIn

example : !d⟨!v[]⟩[] = (Fin.dempty : (i : Fin 0) → !v[] i) := rfl

Even in Mathlib.Algebra.Group.Even

LE.le in Init.Prelude

def fappend₂ {A : Sort u} {B : Sort v} {F : A → B → Sort w} {m n : ℕ}
    {α₁ : Fin m → A} {β₁ : Fin n → A} {α₂ : Fin m → B} {β₂ : Fin n → B}
    (u : (i : Fin m) → F (α₁ i) (α₂ i)) (v : (i : Fin n) → F (β₁ i) (β₂ i)) :
    (i : Fin (m + n)) → F (Fin.vappend α₁ β₁ i) (Fin.vappend α₂ β₂ i) :=
  match n with
  | 0 => u
  | k + 1 => fconcat₂ (fappend₂ u (fun i => v (Fin.castSucc i))) (v (Fin.last k))

noncomputable def batchProver :
  OracleProver []ₒ
    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
  PrvState
  | 0 => (∀j, OracleStatement D x m j) × Witness F s d m
  | 1 => (Fin m → F) × (∀j, OracleStatement D x m j) × Fri.Spec.Witness F s d (0 : Fin (k + 2))

LinearOrder in Mathlib.Order.Defs.LinearOrder

Classical.propDecidable in Init.Classical

def toOracleVerifier
    (naVerifier : OracleVerifier.NonAdaptive oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec) :
    OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec where
  verify := fun stmt challenges => do
    let queryResponsesOStmt : List ((i : ιₛᵢ) × ((Oₛᵢ i).Query × (Oₛᵢ i).Response)) ←
      (naVerifier.queryOStmt stmt challenges).mapM
      (fun q => do
        let resp ← liftM <| query (spec := [OStmtIn]ₒ) q.1 q.2
        return ⟨q.1, (q.2, by admit /- proof elided -/
        )⟩)
    let queryResponsesOMsg : List ((i : pSpec.MessageIdx) × ((Oₘ i).Query × (Oₘ i).Response)) ←
      (naVerifier.queryMsg stmt challenges).mapM
      (fun q => do
        let resp ← liftM <| query (spec := [pSpec.Message]ₒ) q.1 q.2
        return ⟨q.1, ⟨q.2, by admit /- proof elided -/
        ⟩⟩)
    let stmtOut ← liftM <| naVerifier.verify stmt challenges queryResponsesOStmt queryResponsesOMsg
    return stmtOut

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

instance : Fintype BTF₃ := (inferInstance : Fintype (ConcreteBTField 3))

def take (j : Fin (n + 1)) (messages : Messages pSpec) : MessagesUpTo j pSpec :=

def mul_by_2 (s : Finset ℕ) : Finset ℕ :=
  s.map ⟨fun n => 2 * n, by admit /- proof elided -/
  ⟩

abbrev MatrixSubmodule.{u, v, w} (κ : Type u) [Fintype κ] (ι : Type v) [Fintype ι]
                                 (F : Type w) [Semiring F] : Type (max u v w) :=
  Submodule F (Matrix κ ι F)

def snoc (s : Fin n →₀ M) (y : M) : Fin (n + 1) →₀ M :=
  Finsupp.equivFunOnFinite.symm (Fin.snoc s y : Fin (n + 1) → M)

@[reducible]
def OracleStatement : Unit → Type := fun _ => R⦃≤ deg⦄[X Fin n]

noncomputable instance : DecidableEq (GF(2)) :=
  fun x y =>
    
    let φ : GF(2) ≃ₐ[ZMod 2] ZMod 2 := GaloisField.equivZmodP 2
    
    if h : φ x = φ y then
      isTrue (by admit /- proof elided -/
        )
    else
      isFalse (by admit /- proof elided -/
        )

instance [inst : SelectableType Chal] : ∀ i, SelectableType (Challenge ⟨!v[.V_to_P], !v[Chal]⟩ i)
  | ⟨0, _⟩ => inst

def quotient (f g : F[X][Y]) : Prop := ∃ q : F[X][Y], g = q * f

instance : ∀ i, VCVCompatible ((pSpec Witness).Challenge i) | ⟨0, h⟩ => nomatch h

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

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

def RoundByRound.append
    {WitMid₁ : Fin (m + 1) → Type} {WitMid₂ : Fin (n + 1) → Type}
    (E₁ : Extractor.RoundByRound oSpec Stmt₁ Wit₁ Wit₂ pSpec₁ WitMid₁)
    (E₂ : Extractor.RoundByRound oSpec Stmt₂ Wit₂ Wit₃ pSpec₂ WitMid₂) :
      Extractor.RoundByRound oSpec Stmt₁ Wit₁ Wit₃ (pSpec₁ ++ₚ pSpec₂)
        (Fin.append (m := m + 1) WitMid₁ (Fin.tail WitMid₂) ∘ Fin.cast (by admit /- proof elided -/
        )) where
  eqIn := by admit /- proof elided -/

instance : Slice (ProtocolSpec n) ℕ ℕ
    (fun _ start stop => start ≤ stop ∧ stop ≤ n)
    (fun _ start stop _ => ProtocolSpec (stop - start))
    where
  slice := fun v start stop h => extract start stop h.1 h.2 v

@[reducible, simp]
def toRelInput : Set ((Statement × (∀ i, OStatement i)) × Unit) :=
  { ⟨⟨stmt, oStmt⟩, _⟩ | simulateQ' (toOracleImpl OStatement oStmt) (pred stmt) (hPred stmt) }

noncomputable def foldOracleProver (i : Fin ℓ) :
  OracleProver (oSpec := []ₒ)
    
    (StmtIn := Statement (L := L) Context i.castSucc)
    (OStmtIn := OracleStatement 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.castSucc)
    (WitIn := Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (ℓ := ℓ) i.castSucc)
    
    (StmtOut := Statement (L := L) Context i.succ)
    (OStmtOut := OracleStatement 𝔽q β (ϑ := ϑ) (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.castSucc)
    (WitOut := Witness (L := L) 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (ℓ := ℓ) i.succ)
    (pSpec := pSpecFold (L := L)) where

EquivLike in Mathlib.Data.FunLike.Equiv

def AlgebraTowerEquiv.toAlgEquivOverLeft (e : AlgebraTowerEquiv A B) (i j : ι) (h : i ≤ j) :
  letI : Algebra (A i) (A j) :=

def accepts (x : Fin numWires → 𝓡) (g : Gate 𝓡 numWires) : Prop :=
  g.eval x = 0

structure RoundByRound
    (oSpec : OracleSpec ι) (StmtIn WitIn WitOut : Type) {n : ℕ} (pSpec : ProtocolSpec n)
    (WitMid : Fin (n + 1) → Type) where
   
  eqIn : WitMid 0 = WitIn
   
  extractMid : (m : Fin n) → StmtIn → Transcript m.succ pSpec → WitMid m.succ → WitMid m.castSucc
   
  extractOut : StmtIn → FullTranscript pSpec → WitOut → WitMid (.last n)

@[reducible]
def twoAdicity : Nat := 24

def SumFunEquivProd (α β γ : Type) : ((α ⊕ β) → γ) ≃ (α → γ) × (β → γ) :=
{ toFun := fun f => (fun a => f (.inl a), fun b => f (.inr b))
  , invFun := fun p x => match x with | .inl a => p.fst a | .inr b => p.snd b
  , left_inv := by admit /- proof elided -/

let lastOracleVerifier := lastBlockOracleVerifier 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)

inductive VectorOp where | dotProd

def equivBool : Direction ≃ Bool where
  toFun := fun dir => match dir with | .V_to_P => false | .P_to_V => true
  invFun := fun b => match b with | false => .V_to_P | true => .P_to_V
  left_inv := fun dir => match dir with | .P_to_V => rfl | .V_to_P => rfl
  right_inv := fun b => match b with | false => rfl | true => rfl

inst1 : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1), Fintype (indexPowT (S i) (P.φ i) j)
  inst2 : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1),
    Nonempty (indexPowT (S i) (P.φ i) j)
  inst3 : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1),
    DecidableEq (indexPowT (S i) (P.φ i) j)
  inst4 : ∀ i : Fin (M + 1), ∀ j : Fin ((P.foldingParam i) + 1), Smooth (φ i j)

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

@[reducible, inline, specialize]
def MessagesUpTo (k : Fin (n + 1)) (pSpec : ProtocolSpec n) : Type :=
  ∀ i, pSpec.MessageUpTo k i

Polynomial.ofFinsupp in Mathlib.Algebra.Polynomial.Basic

@[inline]
def neg [Neg R] (p : MlPoly R n) : MlPoly R n := p.map (fun a => -a)

Subtype.mk in Init.Prelude

def canonical (p : UniPoly R) := p.trim = p

def subNat [Zero T] [ToNat T] (a : Cayley T) : Nat → Cayley T
  | 0        => a
  | .succ k  => pred (subNat a k)

instance [ProverFirst pSpec] : ∀ i, VCVCompatible (pSpec.Challenge i) := isEmptyElim

List.replicate in Init.Data.List.Basic

instance {langIn : Set StmtIn} {langOut : Set StmtOut}
    {verifier : Verifier oSpec StmtIn StmtOut pSpec} :
    CoeFun (verifier.StateFunction init impl langIn langOut)
    (fun _ => (m : Fin (n + 1)) → StmtIn → Transcript m pSpec → Prop) := ⟨fun f => f.toFun⟩

def evalX (a : F) (f : F[X][Y]) : Polynomial F :=
  ⟨Finsupp.mapRange (Polynomial.eval a) eval_zero f.toFinsupp⟩

def checkSrs (proveSrs : Vector G₁ (n + 1)) (verifySrs : Vector G₂ 2) : Prop :=
  ∀ i : Fin n,
    pairing (proveSrs[i.succ]) (verifySrs[0]) = pairing (proveSrs[i.castSucc]) (verifySrs[1])

noncomputable def byCheckMatrix [CommRing F] (H : Matrix ι κ F) : LinearCode κ F :=
  LinearMap.ker H.mulVecLin

def nonDoomedFoldingProp (i : Fin (ℓ + 1)) (challenges : Fin i → L)
    (oStmt : ∀ j, OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i j)
    : Prop :=
  let oracleFoldingConsistency := oracleFoldingConsistencyProp 𝔽q β i (challenges := challenges)
    (oStmt := oStmt)
  let foldingBadEventExists := badEventExistsProp 𝔽q β i (challenges := challenges)
    (oStmt := oStmt)
  oracleFoldingConsistency ∨ foldingBadEventExists

noncomputable def polynomialAlgEquiv : P ≃ₐ[R] R[X] where
  toFun := toPolynomialAlgHom
  invFun := ofPolynomialAlgHom
  left_inv := by admit /- proof elided -/

def verifier : Verifier oSpec (StmtIn R × (∀ i, OStmtIn R deg i))
                              (StmtOut R × (∀ i, OStmtOut R deg i)) (pSpec R deg) where
  verify := fun ⟨target, oStmt⟩ transcript => do
    letI polyLE := transcript 0
    guard (∑ x ∈ (univ.map D), polyLE.val.eval x = target)
    letI chal := transcript 1
    pure ⟨⟨(oStmt ()).val.eval chal, chal⟩, fun _ => oStmt ()⟩

def parametrisedCurve {l : ℕ} [Semiring F] (u : Fin l → ι → F) : Set (ι → F)
  := {v | ∃ r : F, v = ∑ i : Fin l, (r ^ (i : ℕ)) • u i}

def bitsToU (i : Fin r) (k : Fin (2 ^ i.val)) :
    AdditiveNTT.U (L := L) (𝔽q := 𝔽q) (β := β) i :=
  let val := (Finset.univ : Finset (Fin i)).sum fun j =>
    if (Nat.getBit (n := k.val) (k := j.val) == 1) then
      β ⟨j, by admit /- proof elided -/
      ⟩
    else 0

outputState_eq_next_inputState : ∀ i : Fin (outputState.length - 1),
    outputState[i] = inputState[i.val + 1]

def vconcat {n : ℕ} (v : Fin n → α) (a : α) : Fin (n + 1) → α :=
  dconcat v a

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

class GenMutualCorrParams (P : Params ι F) (S : ∀ i : Fin (M + 1), Finset (ι i)) where

Fin.succAboveEmb in Mathlib.Data.Fin.Embedding

@[reducible]
def OracleStatement (i : Fin (k + 1)) : Fin (i.val + 1) → Type :=
  fun j =>
    evalDomain D x (∑ j' ∈ finRangeTo j.1, s j')
      → F

@[reducible]
def coeffs {R : Type*} (p : UniPoly R) : Array R := p

BStar : ∀ i : Fin (k + 1), (Set (indexPowT S φ i → F)) → Type → ℝ≥0
  errStar : ∀ i : Fin (k + 1), (Set (indexPowT S φ i → F)) → Type → ℝ → ENNReal

def HList.toDVec (l : HList) : DVec (m := Fin l.length) (fun i => l[i].1) := fun i => l[i].2

@[reducible]
def capacitySegment (state : CanonicalSpongeState U) : Vector U SpongeSize.C :=
  Vector.drop state SpongeSize.R

ZMod in Mathlib.Data.ZMod.Defs
</all_available_defs>

<all_available_lemmas>
Fin.eta in Init.Data.Fin.Lemmas
add_zero in Mathlib.Algebra.Group.Defs
Module.Basis.repr_linearCombination in Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.repr_symm_apply in Mathlib.LinearAlgebra.Basis.Defs
Nat.add_zero in Init.Core
cast_eq in Init.Core
eq_mp_eq_cast in Init.PropLemmas
not_lt_zero' in Mathlib.Algebra.Order.GroupWithZero.Canonical
tsub_zero in Mathlib.Algebra.Order.Sub.Defs
nonpos_iff_eq_zero in Mathlib.Algebra.Order.Monoid.Canonical.Defs
not_lt in Mathlib.Order.Defs.LinearOrder
Polynomial.ext in Mathlib.Algebra.Polynomial.Basic
add_lt_iff_neg_right in Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_tsub_cancel_right in Mathlib.Algebra.Order.Sub.Defs
Decidable.not_not in Init.PropLemmas
Nat.le_of_not_lt in Init.Data.Nat.Basic
Nat.sub_lt_sub_right in Init.Data.Nat.Basic
Nat.sub_sub in Init.Data.Nat.Basic
dite_eq_right_iff in Init.PropLemmas
false_or in Init.SimpLemmas
forall_const in Init.PropLemmas
imp_false in Init.Core
ite_eq_left_iff in Init.PropLemmas
one_ne_zero in Mathlib.Algebra.NeZero
Finset.disjoint_iff_inter_eq_empty in Mathlib.Data.Finset.Lattice.Lemmas
Finset.mem_of_mem_inter_left in Mathlib.Data.Finset.Lattice.Basic
Finset.mem_of_mem_inter_right in Mathlib.Data.Finset.Lattice.Basic
Finset.nonempty_of_ne_empty in Mathlib.Data.Finset.Empty
Set.mem_image in Mathlib.Data.Set.Operations
Set.mem_toFinset in Mathlib.Data.Fintype.Sets

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

@[simp]
lemma lt_add_of_pos_right_of_le (a b c : ℕ) [NeZero c] (h : a ≤ b) : a < b + c

omit [DecidableEq 𝔽q] hF₂ in
lemma getSDomainBasisCoeff_of_iteratedQuotientMap
    [NeZero R_rate] (i : Fin ℓ) (k : ℕ)
    (h_bound : i.val + k ≤ ℓ) (x : (sDomain 𝔽q β
    h_ℓ_add_R_rate) ⟨i, by omega⟩) :
    let y

theorem base_intermediateNormVpoly
  (k : Fin (ℓ + 1)) :
  intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate ⟨0, by
    by_contra ht
    simp only [not_lt, nonpos_iff_eq_zero] at ht
    contradiction
  ⟩ ⟨k, by simp only [tsub_zero]; omega⟩ =
  normalizedW 𝔽q β ⟨k, by omega⟩

lemma normalizedW_eq_qMap_composition (ℓ R_rate : ℕ) (i : Fin r) :
    normalizedW 𝔽q β i = qCompositionChain 𝔽q β (ℓ:=ℓ) (R_rate:=R_rate) i

lemma qMap_comp_normalizedW (i : Fin r) (h_i_add_1 : i + 1 < r) :
  (qMap 𝔽q β i).comp (normalizedW 𝔽q β i) = normalizedW 𝔽q β (i + 1)

lemma qCompositionChain_eq_foldl (i : Fin r) :
  qCompositionChain 𝔽q β (ℓ:=ℓ) (R_rate:=R_rate) i =
  Fin.foldl (n:=i) (fun acc j =>
    (qMap 𝔽q β ⟨j, by omega⟩).comp acc) (X)

omit [DecidableEq 𝔽q] hF₂ h_β₀_eq_1 in
lemma getSDomainBasisCoeff_of_sum_repr [NeZero R_rate] (i : Fin (ℓ + 1))
    (x : (sDomain 𝔽q β h_ℓ_add_R_rate) ⟨i, by omega⟩)
    (x_coeffs : Fin (ℓ + R_rate - i) → 𝔽q)
    (hx : x = ∑ j_x, (x_coeffs j_x) • (sDomain_basis 𝔽q β
      h_ℓ_add_R_rate (i := ⟨i, by omega⟩) (h_i := by
        simp only; apply Nat.lt_add_of_pos_right_of_le; omega) j_x).val) :
    ∀ (j: Fin (ℓ + R_rate - i)), ((sDomain_basis 𝔽q β
      h_ℓ_add_R_rate (i := ⟨i, by omega⟩) (h_i := by
        simp only; apply Nat.lt_add_of_pos_right_of_le; omega)).repr x) j = x_coeffs j

omit [DecidableEq 𝔽q] hF₂ h_β₀_eq_1 in
lemma get_sDomain_basis (i : Fin r) (h_i : i < ℓ + R_rate) :
    ∀ (k : Fin (ℓ + R_rate - i)),
    (sDomain_basis 𝔽q β h_ℓ_add_R_rate
      i (by omega)) k = eval (β ⟨i + k.val, by omega⟩) (normalizedW 𝔽q β i)

omit [DecidableEq L] [DecidableEq 𝔽q] h_Fq_char_prime hF₂ hβ_lin_indep h_β₀_eq_1 in
theorem intermediateNormVpoly_comp (i : Fin ℓ) (k : Fin (ℓ - i + 1))
  (l : Fin (ℓ - (i.val + k.val) + 1)) :
  intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩) (k:=⟨k + l, by
      simp only; omega⟩) =
    (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate (i := ⟨i+k, by omega⟩) (k:=⟨l, by
      simp only; omega⟩)).comp (
  intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩) (k:=⟨k, by
      simp only; omega⟩)
  )

omit [DecidableEq L] [DecidableEq 𝔽q] hF₂ hβ_lin_indep h_β₀_eq_1 in
lemma intermediateNormVpoly_eval_is_linear_map (i : Fin (ℓ + 1)) (k : Fin (ℓ - i + 1)) :
  IsLinearMap 𝔽q (fun x : L =>
    (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate i k).eval x)

theorem qMap_is_linear_map (i : Fin r) :
  IsLinearMap 𝔽q (f:=fun inner_p ↦ (qMap 𝔽q β i).comp inner_p)

omit h_Fq_char_prime in
lemma 𝔽q_element_eq_zero_or_eq_one : ∀ c: 𝔽q, c = 0 ∨ c = 1

lemma getBit_of_binaryFinMapToNat {n : ℕ} (m : Fin n → ℕ) (h_binary: ∀ j: Fin n, m j ≤ 1) :
    ∀ k: ℕ, Nat.getBit k (binaryFinMapToNat m h_binary).val
      = if h_k: k < n then m ⟨k, by omega⟩ else 0

lemma and_two_pow_eq_zero_of_getBit_0 {n i : ℕ} (h_getBit : getBit i n = 0)
    : n &&& (2 ^ i) = 0

lemma and_eq_zero_iff_and_each_getBit_eq_zero {n m : ℕ} :
    n &&& m = 0 ↔ ∀ k, Nat.getBit k n &&& Nat.getBit k m = 0

lemma eq_iff_eq_all_getBits {n m : ℕ} : n = m ↔ ∀ k, getBit k n = getBit k m

lemma shiftRight_and_one_distrib {n m k : ℕ} :
    Nat.getBit k (n &&& m) = Nat.getBit k n &&& Nat.getBit k m

lemma getBit_two_pow {i k : ℕ} : (getBit k (2^i) = if i == k then 1 else 0)

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

lemma getBit_eq_testBit (k n : Nat) : getBit k n = if n.testBit k then 1 else 0

lemma getBit_lt_2 {k n : Nat} : getBit k n < 2

lemma getBit_of_xor {n m k: ℕ} : getBit k (n ^^^ m) = getBit k n ^^^ getBit k m

lemma getBit_zero_eq_zero {k : Nat} : getBit k 0 = 0

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

lemma sum_eq_xor_plus_twice_and (n : Nat) : ∀ m : ℕ, n + m = (n ^^^ m) + 2 * (n &&& m)

lemma and_by_split_lowBits {n m n1 m1 bn bm : ℕ} (h_bn : bn < 2) (h_bm : bm < 2)
  (h_n : n = n1 * 2 + bn) (h_m : m = m1 * 2 + bm):
  n &&& m = (n1 &&& m1) * 2 + (bn &&& bm)

lemma div_2_form {nD2 b : ℕ} (h_b : b < 2):
  (nD2 * 2 + b) / 2 = nD2

lemma or_by_split_lowBits {n m n1 m1 bn bm : ℕ} (h_bn : bn < 2) (h_bm : bm < 2)
  (h_n : n = n1 * 2 + bn) (h_m : m = m1 * 2 + bm):
  n ||

lemma xor_by_split_lowBits {n m n1 m1 bn bm : ℕ} (h_bn : bn < 2) (h_bm : bm < 2)
  (h_n : n = n1 * 2 + bn) (h_m : m = m1 * 2 + bm):
  n ^^^ m = (n1 ^^^ m1) * 2 + (bn ^^^ bm)

@[simp]
theorem rtake_self' {α : Sort*} (v : Fin n → α) : rtake n (by omega) v = v

theorem cast_symm {α β : Sort u} {h : α = β} {a : α} {b : β} :
    cast h a = b ↔ a = cast h.symm b

Nat.zero_add in Init.Data.Nat.Basic

nonpos_iff_eq_zero in Mathlib.Algebra.Order.Monoid.Canonical.Defs

beq_iff_eq in Init.Core

lemma rowRank_eq_colRank : rowRank U = colRank U

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

@[simp]
theorem LeafData.optionComposeBuild_internal {α} {s_left s_right : Skeleton}
    (left : LeafData α s_left) (right : LeafData α s_right)
    (compose : α → α → Option α) :
    (LeafData.internal left right).optionComposeBuild compose =
      FullData.internal
        (Option.doubleBind compose
          (left.optionComposeBuild compose).getRootValue
          (right.optionComposeBuild compose).getRootValue)
        (left.optionComposeBuild compose)
        (right.optionComposeBuild compose)

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

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)

@[simp]
lemma relHammingDist_mem_relHammingDistRange [DecidableEq F] : δᵣ(u, v) ∈ relHammingDistRange ι

@[simp]
theorem cast_dir_idx {hn} (hSpec : pSpec₁.cast hn = pSpec₂) {i : Fin n₁} :
    pSpec₂.dir (Fin.cast hn i) = pSpec₁.dir i

private theorem toNat_mulNat (a : AssocNat) (k : Nat) : toNat (mulNat a k) = toNat a * k

@[simp] theorem ofNat_succ (n : Nat) : ofNat n.succ = succ (ofNat n)

@[to_additive (attr := simp)]
theorem prod_Iic_zero : ∏ j ∈ Iic 0, v j = v 0

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

lemma h_sum_two_same_pow2 {k : ℕ} (h_pos : k > 0) : 2 ^ (k - 1) + 2 ^ (k - 1) = 2 ^ k

theorem ofNat_toNat (n : ChurchNat ℕ) : ofNat (toNat n) = n

@[simp]
lemma Verifier.id_rbrKnowledgeSoundness {rel : Set (Statement × Witness)} :
    (Verifier.id : Verifier oSpec Statement _ _).rbrKnowledgeSoundness
      init impl rel rel 0

lemma getBit_of_highBits {n: ℕ} (numLowBits : ℕ) : ∀ k, getBit k (getHighBits numLowBits n) =
    if k < numLowBits then 0 else getBit (k) (n)

private lemma le_sum_choose_K [Zero F]
  (h_card : 2 ≤ (Fintype.card F)) :
  choose_2 (K B i 0) + (Fintype.card (α := F) - 1) *
  choose_2 ((B.card - K B i 0) / (Fintype.card (α := F) - 1)) ≤ sum_choose_K_i B i

omit [CharP L 2] [DecidableEq 𝔽q] hF₂ h_β₀_eq_1 [NeZero 𝓡] in
lemma take_snoc_oracle_eq_oStmtIn (i : Fin ℓ)
    (oStmtIn : (j : Fin (toOutCodewordsCount ℓ ϑ i.castSucc)) →
      OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i.castSucc j)
    (newOracleFn : OracleFunction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ) :
    (take_snoc_oracle 𝔽q β i oStmtIn newOracleFn) = oStmtIn

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

lemma BerlekampWelch_Q_ne_zero {e k : ℕ}
  [NeZero n]
  {ωs f : Fin n → F}
  {E Q : Polynomial F}
  (h_bw : BerlekampWelchCondition e k ωs f E Q)
  (h_dist : e < Δ₀(f, 0))
  (h_inj : Function.Injective ωs)
  : Q ≠ 0

lemma concrete_mul_left_distrib
  {h_k : k > 0} (prevBTFieldProps : ConcreteBTFieldProps (k := k - 1))
  (a b c : ConcreteBTField k) :
    concrete_mul a (b + c) = concrete_mul a b + concrete_mul a c

private lemma sum_of_not_equals :
  ∑ x ∈ B ×ˢ B with x.1 ≠ x.2, (if x.1 i ≠ x.2 i then 1 else 0)
  =
  2 * choose_2 #B - 2 * ∑ α, choose_2 (K B i α)

lemma cube_map_bijective :
    Function.Bijective (fun x : (Field)ˣ => x ^ (3 : Nat))

@[simp]
theorem vflatten_splitSum {m : ℕ} {n : Fin m → ℕ} (v : (k : Fin (vsum n)) → α) (k : Fin (vsum n)) :
    vflatten (fun i j => v (embedSum i j)) k = v k

@[simp]
theorem cast_id :
    OracleVerifier.cast rfl rfl (fun i => rfl) =
      (id : OracleVerifier oSpec StmtIn OStmtIn StmtOut OStmtOut pSpec₁ → _)

@[simp]
theorem simulateQ'_query_bind (q : OracleQuery spec α)
    (ob : α → OracleComp spec β) (h : ∀ x, (ob x).neverFails) :
    simulateQ' so (liftM q >>= ob) (by simp [h]) =
      so.impl q >>= (fun x => simulateQ' so (ob x) (h x))

theorem eval_zeroOne_eq_MLE_toEvalsZeroOne (p : MvPolynomial σ R) (x : σ → Fin 2) :
    eval (x : σ → R) p = eval (x : σ → R) (MLE p.toEvalsZeroOne)

theorem simulateQ'_eq_simulateQ [AlternativeMonad m] [LawfulMonad m]
    {so : QueryImpl spec m} (oa : OracleComp spec α) (h : oa.neverFails) :
      simulateQ' so oa h = simulateQ so oa

@[simp] theorem equiv_symm {p q : UniPoly Q} : equiv p q → equiv q p

theorem mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials
  {n : ℕ} [NeZero n] {v : ι ↪ F} {p : F[X]} (h_deg : p.natDegree < n) :
  (Vandermonde.nonsquare (ι' := n) v).mulVecLin (Fin.liftF' p.coeff) =
  fun i => p.eval (v i)

@[simp, grind =]
lemma leadingCoeffY_ne_zero (f : F[X][Y]) : leadingCoeffY f ≠ 0 ↔ f ≠ 0

theorem append_rbrSoundness (V₁ : OracleVerifier oSpec Stmt₁ OStmt₁ Stmt₂ OStmt₂ pSpec₁)
    (V₂ : OracleVerifier oSpec Stmt₂ OStmt₂ Stmt₃ OStmt₃ pSpec₂)
    {rbrSoundnessError₁ : pSpec₁.ChallengeIdx → ℝ≥0}
    {rbrSoundnessError₂ : pSpec₂.ChallengeIdx → ℝ≥0}
    (h₁ : V₁.rbrSoundness init impl lang₁ lang₂ rbrSoundnessError₁)
    (h₂ : V₂.rbrSoundness init impl lang₂ lang₃ rbrSoundnessError₂) :
      (V₁.append V₂).rbrSoundness init impl lang₁ lang₃
        (Sum.elim rbrSoundnessError₁ rbrSoundnessError₂ ∘ ChallengeIdx.sumEquiv.symm)

Nat.pow_lt_pow_right in Init.Data.Nat.Lemmas

@[simp]
lemma finite_offDiag [Finite F] : C.offDiag.Finite

@[simp] theorem rightpad_eq_self (l : List α) (n : Nat) (h : n ≤ l.length) :
    rightpad n unit l = l

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

@[simp]
theorem Basis_cast_dest_apply {ι : Type*} (α β γ : ℕ)
    (h_le1 : α ≤ β) (h_le2 : α ≤ γ)
    (h_eq : β = γ) {k : ι} (b : @Basis ι (ConcreteBTField α) (ConcreteBTField β) _ _
    (@ConcreteBTFieldAlgebra (l := α) (r := β) (h_le := h_le1)).toModule) :
    let castBasis : @Basis ι (ConcreteBTField α) (ConcreteBTField γ) _ _
      (@ConcreteBTFieldAlgebra (l := α) (r := γ) (h_le := h_le2)).toModule :=
      cast (by
        exact Basis_cast_dest_eq α γ β h_le2 h_le1 h_eq
      ) b
    (castBasis k) = cast (by
      exact cast_ConcreteBTField_eq β γ h_eq) (b k)

theorem verifier_rbrKnowledgeSoundness [Fintype R] :
    (verifier R deg D oSpec).rbrKnowledgeSoundness init impl
    (inputRelation R deg D) (outputRelation R deg) (fun _ => (deg : ℝ≥0) / (Fintype.card R))

theorem cast_eq_dcast {h : n₁ = n₂} {pSpec : ProtocolSpec n₁} :
    pSpec.cast h = dcast h pSpec

theorem range_vcons {α : Type*} (a : α) (v : Fin n → α) :
    Set.range (a ::ᵛ v) = insert a (Set.range v)

theorem liftContext_soundness
    {soundnessError : ℝ≥0}
    {lens : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut
                                OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut}
    (V : OracleVerifier oSpec InnerStmtIn InnerOStmtIn InnerStmtOut InnerOStmtOut pSpec)
    [lensSound : lens.IsSound outerLangIn outerLangOut innerLangIn innerLangOut
      (V.toVerifier.compatStatement lens)]
    (h : V.soundness init impl innerLangIn innerLangOut soundnessError) :
      (V.liftContext lens).soundness init impl outerLangIn outerLangOut soundnessError

lemma one_bitvec_shiftRight {d : ℕ} (h_d : d > 0) : 1 >>> d = 0

theorem GF_2_one_add_one_eq_zero : (1 + 1 : GF(2)) = 0

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

theorem castSum_castLT {l' : List ℕ} {i : ℕ} (j : Fin i) :
    castSum (i :: l') (by simp) j =
      castLT j (Nat.lt_of_lt_of_le j.isLt (List.le_sum_of_mem (by simp)))

theorem unique_linear_decomposition_succ (k : ℕ) :
  letI : Algebra (ConcreteBTField k) (ConcreteBTField (k+1)) :=
    ConcreteBTFieldAlgebra (l:=k) (r:=k+1) (h_le:=by omega)
  ∀ (x : ConcreteBTField (k+1)), ∃! (p : ConcreteBTField k × ConcreteBTField k),
    x = join_via_add_smul (k+1) (by omega) p.1 p.2

@[simp]
theorem runWithOracle_pure (f : spec.FunctionType) (a : α) :
    runWithOracle f (pure a) = some a

lemma and_eq_zero_iff {n m : ℕ} : n &&& m = 0 ↔ ∀ k, (n >>> k) &&& (m >>> k) = 0

lemma algebraMap_ConcreteBTFieldAlgebra_def (l r : ℕ) (h_le : l ≤ r) :
    (@ConcreteBTFieldAlgebra (l:=l) (r:=r) (h_le:=h_le)).algebraMap
    = concreteTowerAlgebraMap l r h_le

lemma getLowBits_zero_eq_zero {n : ℕ} : getLowBits 0 n = 0

@[simp]
theorem impl_run {i : ι} {t : spec.domain i} :
    (loggingOracle.impl (query i t)).run = (do let u ← query i t; return (u, [⟨i, ⟨t, u⟩⟩]))

private lemma f_convex {x₁ x₂ : ℚ} {α₁ α₂ : ℚ}
  (h_noneg_1 : 0 ≤ α₁)
  (h_noneg_2 : 0 ≤ α₂)
  (h_conv : α₁ + α₂ = 1)
  :
  f (α₁ * x₁ + α₂ * x₂) ≤ α₁ * f x₁ + α₂ * f x₂

theorem fconcat_inj {α : Fin n → A} {β : A}
    (v₁ v₂ : (i : Fin n) → F (α i)) (a₁ a₂ : F β) :
    fconcat v₁ a₁ = fconcat v₂ a₂ ↔ v₁ = v₂ ∧ a₁ = a₂

lemma eval₂_eq' {S : Type w} [CommSemiring S] (g : P →+* S) (p : P) :
    g p = eval₂ (g.comp (Algebra.ofId R P)) (g X) p

Nat.cast_pow in Mathlib.Data.Nat.Cast.Basic

@[ext]
theorem ext' {a b : AssocNat} (h : a 0 = b 0) : a = b

@[simp]
theorem fappend₂_left {α₁ : Fin m → A} {α₂ : Fin m → B} {β₁ : Fin n → A} {β₂ : Fin n → B}
    (u : (i : Fin m) → F₂ (α₁ i) (α₂ i)) (v : (i : Fin n) → F₂ (β₁ i) (β₂ i)) (i : Fin m) :
    fappend₂ (F := F₂) u v (castAdd n i) =
      cast (by simp [vappend_left]) (u i)

theorem zero_add {n : ℕ} (a : CNat (n + 1)) : 0 + a = a

theorem rtake_rev_eq_take_of_rev {α : Sort*} (m : ℕ) (h : m ≤ n) (v : Fin n → α) :
    rtake m h v ∘ Fin.rev = (take m h (v ∘ Fin.rev))

omit [Finite F] in
lemma domain_surjective (i : ℕ) : i ≤ n → Function.Surjective (domain D n i)

theorem dfoldl_congr_dcast {n : ℕ}
    {ι : Type v} {α α' : Fin (n + 1) → ι} {β : ι → Type u} [DCast ι β]
    {f : (i : Fin n) → β (α i.castSucc) → β (α i.succ)}
    {f' : (i : Fin n) → β (α' i.castSucc) → β (α' i.succ)}
    {init : β (α 0)} {init' : β (α' 0)}
    (hα : ∀ i, α i = α' i)
    (hf : ∀ i a, f i a = (dcast (hα _).symm (f' i (dcast (hα _) a))))
    (hinit : init = dcast (hα 0).symm init') :
      dfoldl n (fun i => β (α i)) f init =
        cast (by have := funext hα; subst this; simp) (dfoldl n (fun i => β (α' i)) f' init')

omit [Fintype 𝔽q] h_Fq_char_prime hβ_lin_indep in
lemma eval_W_eq_zero_iff_in_U (i : Fin r) (a : L) :
  (W 𝔽q β i).eval a = 0 ↔ a ∈ U 𝔽q β i

@[simp]
theorem cast_idx_symm {i : MessageIdx pSpec₂} :
    pSpec₁.Message (i.cast hn.symm (cast_symm hSpec)) = pSpec₂.Message i

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

theorem liftContext_processRound
    {lens : Context.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut
                        OuterWitIn OuterWitOut InnerWitIn InnerWitOut}
    {i : Fin n}
    {P : Prover oSpec InnerStmtIn InnerWitIn InnerStmtOut InnerWitOut pSpec}
    {resultRound : OracleComp (oSpec ++ₒ [pSpec.Challenge]ₒ)
      (pSpec.Transcript i.castSucc × (P.liftContext lens).PrvState i.castSucc)} :
      (P.liftContext lens).processRound i resultRound
      = do
        let ⟨transcript, prvState, outerStmtIn, outerWitIn⟩ ← resultRound
        let ⟨newTranscript, newPrvState⟩ ← P.processRound i (do return ⟨transcript, prvState⟩)
        return ⟨newTranscript, ⟨newPrvState, outerStmtIn, outerWitIn⟩⟩

@[simp]
lemma liftF_zero_eq_zero
  : liftF (fun (_ : Fin n) ↦ (0 : α)) = (fun _ ↦ (0 : α))

theorem mobius_apply_zeta_apply_eq_id (n : ℕ) [NeZero n] (r : Fin n) (l : Fin (r.val + 1))
    (v : Vector R (2 ^ n)) : lagrangeToMono_segment n r l (monoToLagrange_segment n r l v) = v

theorem johnson_bound [Field F]
  (h_condition : JohnsonConditionStrong B v)
  :
  let d := d B
  let q : ℚ := Fintype.card F
  let frac := q / (q - 1)
  B.card ≤ (frac * d/n) / JohnsonDenominator B v
</all_available_lemmas>

<local_ctx>
import ArkLib.Data.CodingTheory.BerlekampWelch.BerlekampWelch

import ArkLib.Data.CodingTheory.ReedSolomon

import ArkLib.Data.FieldTheory.AdditiveNTT.AdditiveNTT

import ArkLib.Data.MvPolynomial.Multilinear

import ArkLib.Data.Vector.Basic

import ArkLib.ProofSystem.Sumcheck.Spec.SingleRound

namespace Binius.BinaryBasefold

open OracleSpec OracleComp ProtocolSpec Finset AdditiveNTT Polynomial MvPolynomial
  Binius.BinaryBasefold

open scoped NNReal

open ReedSolomon Code BerlekampWelch

open Finset AdditiveNTT Polynomial MvPolynomial Nat Matrix

section Preliminaries

variable {L : Type} [CommRing L] (ℓ : ℕ) [NeZero ℓ]

variable (𝓑 : Fin 2 ↪ L)

end Preliminaries

noncomputable section       -- expands with 𝔽q in front

variable {r : ℕ} [NeZero r]

variable {L : Type} [Field L] [Fintype L] [DecidableEq L] [CharP L 2]

variable (𝔽q : Type) [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 {ℓ 𝓡 ϑ : ℕ} (γ_repetitions : ℕ) [NeZero ℓ] [NeZero 𝓡] [NeZero ϑ] -- Should we allow ℓ = 0?

variable {h_ℓ_add_R_rate : ℓ + 𝓡 < r} -- ℓ ∈ {1, ..., r-1}

variable {𝓑 : Fin 2 ↪ L}

section Essentials

noncomputable def fiber_coeff
    (i : Fin r) (steps : ℕ)
    (j : Fin (ℓ + 𝓡 - i)) (elementIdx : Fin (2 ^ steps))
    (y_coeffs : Fin (ℓ + 𝓡 - (i + steps)) →₀ 𝔽q) : 𝔽q :=
  if hj : j.val < steps then
    if Nat.getBit (k := j) (n := elementIdx) = 0 then 0 else 1
  else y_coeffs ⟨j.val - steps, by admit /- proof elided -/
    ⟩

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

    let basis_x := sDomain_basis 𝔽q β h_ℓ_add_R_rate ⟨i, by admit /- proof elided -/
    ⟩ (by admit /- proof elided -/
    )
    exact fun elementIdx => by admit /- proof elided -/

def pointToIterateQuotientIndex (i : Fin (ℓ + 1)) (steps : ℕ) (h_i_add_steps : i.val + steps ≤ ℓ)
    (x : sDomain 𝔽q β h_ℓ_add_R_rate (i := ⟨i, by omega⟩)) : Fin (2 ^ steps) :=
</local_ctx>

<target_theorem>
theorem qMap_total_fiber_disjoint
  (i : Fin ℓ) (steps : ℕ) (h_i_add_steps : i + steps ≤ ℓ)
  {y₁ y₂ : sDomain 𝔽q β h_ℓ_add_R_rate ⟨i.val + steps, by omega⟩}
  (hy_ne : y₁ ≠ y₂) :
  Disjoint
    ((qMap_total_fiber 𝔽q β (i := ⟨i, by omega⟩) (steps := steps)
      (h_i_add_steps := fin_ℓ_steps_lt_ℓ_add_R i steps h_i_add_steps) y₁ '' Set.univ).toFinset)
    ((qMap_total_fiber 𝔽q β (i := ⟨i, by omega⟩) (steps := steps)
      (h_i_add_steps := fin_ℓ_steps_lt_ℓ_add_R i steps h_i_add_steps) y₂ '' Set.univ).toFinset) :=
</target_theorem>

