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
Finset in Mathlib.Data.Finset.Defs
Finset.univ in Mathlib.Data.Fintype.Defs
Ne in Init.Core
NeZero in Init.Data.NeZero
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
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
Polynomial.X in Mathlib.Algebra.Polynomial.Basic
Semiring in Mathlib.Algebra.Ring.Defs
Polynomial.degreeLT in Mathlib.RingTheory.Polynomial.Basic
Set.univ in Mathlib.Data.Set.Defs
hammingDist in Mathlib.InformationTheory.Hamming
Finset.max in Mathlib.Data.Finset.Max
Module in Mathlib.Algebra.Module.Defs
Module.finrank in Mathlib.LinearAlgebra.Dimension.Finrank
ENat in Mathlib.Data.ENat.Defs
ENat.toNat in Mathlib.Data.ENat.Basic
Eq in Init.Prelude
Finset.biUnion in Mathlib.Data.Finset.Union
Finset.filter in Mathlib.Data.Finset.Filter
Fintype.ofFinite in Mathlib.Data.Fintype.EquivFin
Function.onFun in Mathlib.Logic.Function.Defs
Nonempty in Init.Prelude
Polynomial.eval in Mathlib.Algebra.Polynomial.Eval.Defs
SetLike in Mathlib.Data.SetLike.Basic
WithTop in Mathlib.Order.TypeTags
id in Init.Prelude
Finsupp in Mathlib.Data.Finsupp.Defs
Finsupp.equivFunOnFinite in Mathlib.Data.Finsupp.Defs
CharP in Mathlib.Algebra.CharP.Defs
DecidableEq in Init.Prelude
Set.image in Mathlib.Data.Set.Defs
Decidable in Init.Prelude
reduceDIte in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
Inhabited in Init.Prelude
Repr in Init.Data.Repr
Fin.cast in Init.Data.Fin.Basic
Nat.succ in Init.Prelude

notation "Δ₀(" u ", " v ")" => hammingDist u v

notation "Δ₀(" u ", " C ")" => distFromCode u C

scoped macro_rules
  | `(ρ $t:term) => `(LinearCode.rate $t)

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
}

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

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

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 code (deg : ℕ) [Semiring F]: Submodule F (ι → F) :=
  (Polynomial.degreeLT F deg).map (evalOnPoints domain)

def evalOnPoints [Semiring F] : F[X] →ₗ[F] (ι → F) where
  toFun := fun p => fun x => p.eval (domain x)
  map_add' := fun x y => by admit /- proof elided -/

noncomputable def distFromCode (u : n → R) (C : Set (n → R)) : ℕ∞ :=
  sInf {d | ∃ v ∈ C, hammingDist u v ≤ d}

def toFinset (domain : ι ↪ F) (deg : ℕ) : Finset (ι → F) :=
  (RScodeSet domain deg).toFinset

abbrev RScodeSet (domain : ι ↪ F) (deg : ℕ) : Set (ι → F) := (ReedSolomon.code domain deg).carrier

noncomputable def minDist (C : Set (n → R)) : ℕ :=
  sInf {d | ∃ u ∈ C, ∃ v ∈ C, u ≠ v ∧ hammingDist u v = d}

noncomputable def rate [Semiring F] (LC : LinearCode ι F) : ℚ≥0 :=
  (dim LC : ℚ≥0) / length LC

noncomputable def dim [Semiring F] (LC : LinearCode ι F) : ℕ :=
  Module.finrank F LC

abbrev LinearCode.{u, v} (ι : Type u) [Fintype ι] (F : Type v) [Semiring F] : Type (max u v) :=
  Submodule F (ι → F)

def length [Semiring F] (_ : LinearCode ι F) : ℕ := Fintype.card ι

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

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

notation "Δ" IC => minDist IC

notation "Δ₀(" u ", " C ")" => distFromCode u C

List in Init.Prelude

EquivLike in Mathlib.Data.FunLike.Equiv

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

def deriveTranscriptDSFS {ι : Type} {oSpec : OracleSpec ι} {StmtIn : Type}
    (stmtIn : StmtIn) (messages : pSpec.Messages) :
    OracleComp (oSpec ++ₒ duplexSpongeChallengeOracle StmtIn U)
      (CanonicalDuplexSponge U × pSpec.FullTranscript) := do
  let sponge ← liftM (DuplexSponge.start stmtIn)
  deriveTranscriptDSFSAux sponge messages (Fin.last n)

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

@[inline]
def nsmul [SMul ℕ R] (m : ℕ) (p : MlPoly R n) : MlPoly R n := p.map (fun a => m • a)

List.mapM' in Init.Data.List.Monadic

def hiding' (scheme : Scheme oSpec Data Randomness Commitment pSpec) : Prop := sorry

instance [inst : ∀ i, DecidableEq (pSpec.Message i)] {k : Fin (n + 1)} :
    DecidableEq (MessagesUpTo k pSpec) :=
  @Fintype.decidablePiFintype _ _ (fun i => inst ⟨i.1.castLE (by admit /- proof elided -/
  ), i.property⟩) _

GaloisField.equivZmodP in Mathlib.FieldTheory.Finite.GaloisField

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⟩

noncomputable def finalFoldProver :
  OracleProver []ₒ
    (Statement F (Fin.last k)) (OracleStatement D x s (Fin.last k))
      (Witness F s d (Fin.last k).castSucc)
    (FinalStatement F k) (FinalOracleStatement D x s)
      (Witness F s d (Fin.last (k + 1)))
    (pSpec F) where
  PrvState
  | 0 =>
    (Statement F (Fin.last k) × ((j : Fin (k + 1)) → OracleStatement D x s (Fin.last k) j)) ×
      Witness F s d (Fin.last k).castSucc
  | _ =>
    (FinalStatement F k × ((j : Fin (k + 1)) → OracleStatement D x s (Fin.last k) j)) ×
      Witness F s d (Fin.last (k + 1))

HomogeneousPow in Init.Prelude

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

def closePtsOnAffineLine {ι : Type*} [Fintype ι]
                         (u v : ι → F) (deg : ℕ) (α : ι ↪ F) (e : ℕ) : Set (ι → F) :=
  {x : ι → F | x ∈ Affine.line u v ∧ distFromCode x (ReedSolomon.code α deg) ≤ e}

instance instDCastSigma {α : Type*} {β : α → Type*} {γ : (a : α) → β a → Type*}
    [DCast α β] [DCast₂ α β γ] : DCast ((a : α) × β a) (fun a => γ a.1 a.2) where
  dcast hab c := dcast₂ (by admit /- proof elided -/
  ) (by admit /- proof elided -/
  ) c
  dcast_id := by admit /- proof elided -/

Or.inl in Init.Prelude

instance {k : Fin 1} : Unique (Transcript k (default : ProtocolSpec 0)) where
  default := fun i => ()
  uniq := by admit /- proof elided -/

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

output := fun ⟨⟨chals, o⟩, p⟩ => pure <|
    ⟨
      ⟨
        chals,
        fun j =>
          if h : j.1 < i.1
          then by admit /- proof elided -/
      ⟩,
      p
    ⟩

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

abbrev SEP_CHAR : Char := Char.ofNat 0

first_inputState_eq_state : inputState[0]? = state

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

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

Polynomial.degreeLTEquiv in Mathlib.RingTheory.Polynomial.Basic

noncomputable def liftBivariate {H : F[X][Y]} : F[X][Y] →+* 𝕃 H :=
  RingHom.comp (Ideal.Quotient.mk (Ideal.span {H_tilde H})) bivPolyHom

zsmulRec in Mathlib.Algebra.Group.Defs

Fin.mk in Init.Prelude

instance Vector.instFintype {α : Type*} {n : ℕ} [VCVCompatible α] : Fintype (Vector α n) :=
  Fintype.ofEquiv _ (Equiv.rootVectorEquivFin).symm

def Cache (n : ℕ) := (layer : Fin (n + 1)) → List.Vector α (2 ^ layer.val)

Polynomial.reverse in Mathlib.Algebra.Polynomial.Reverse

def SkeletonLeafIndex.depth {s : Skeleton} : SkeletonLeafIndex s → Nat
  | SkeletonLeafIndex.ofLeaf => 0
  | SkeletonLeafIndex.ofLeft idxLeft => idxLeft.depth + 1
  | SkeletonLeafIndex.ofRight idxRight => idxRight.depth + 1

instance :
    ∀ i, OracleInterface
          ((pSpecFold D x k s ++ₚ FinalFoldPhase.pSpec F ++ₚ QueryRound.pSpec D x l).Message i) :=
  instOracleInterfaceMessageAppend

input := id

instance {α : Type*} {n : ℕ} [VCVCompatible α] : VCVCompatible (Vector α n) where

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

noncomputable def toMvPolynomialAlgHom : P →ₐ[R] MvPolynomial σ R := aeval MvPolynomial.X

noncomputable def finalSumcheckVerifier :
  OracleVerifier
    (oSpec := []ₒ)
    (StmtIn := Statement (L := L) (SumcheckBaseContext L ℓ) (Fin.last ℓ))
    (OStmtIn := OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ (Fin.last ℓ))
    (StmtOut := FinalSumcheckStatementOut (L := L) (ℓ := ℓ))
    (OStmtOut := OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ (Fin.last ℓ))
    (pSpec := pSpecFinalSumcheckStep (L := L)) where
  verify := fun stmtIn _ => do
    
    let c : L ← query (spec := [(pSpecFinalSumcheckStep (L := L)).Message]ₒ) ⟨0, rfl⟩ ()

@[reducible]
def FinalOracleStatement : Fin (k + 2) → Type :=
  fun j =>
    if j.1 = k + 1
    then (Unit → F[X])
    else (evalDomain D x (∑ j' ∈ finRangeTo j.1, s j') → F)

def challengeTensorProduct (steps : ℕ) (r_challenges : Fin steps → L) : Vector L (2 ^ steps) :=
  if h_steps_zero : steps = 0 then
    
    by
      rw [h_steps_zero, pow_zero]
      exact ⟨#[1], rfl⟩
  else
    
    Nat.rec
      (motive := fun k => k ≤ steps → Vector L (2^k))
      (fun _ => ⟨#[1], rfl⟩)  
      (fun k ih h_k_le =>
        
        let prev_vec := ih (Nat.le_trans (Nat.le_succ k) h_k_le)
        let r_k := r_challenges ⟨k, by admit /- proof elided -/
        ⟩
        
        Vector.ofFn (fun idx : Fin (2^k.succ) =>
          let prev_idx : Fin (2^k) := ⟨idx.val / 2, by admit /- proof elided -/
            ⟩
          let bit := idx.val % 2
          let prev_val := prev_vec.get prev_idx
          if bit = 0 then (1 - r_k) * prev_val else r_k * prev_val))
      steps (le_refl steps)

def combined : Prop :=
  capacitySegmentDup trace ∨ notFunction trace

ratchetUnchecked : α → α

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

structure OracleContext.Lens (OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut : Type)
    {Outer_ιₛᵢ : Type} (OuterOStmtIn : Outer_ιₛᵢ → Type) [∀ i, OracleInterface (OuterOStmtIn i)]
    {Outer_ιₛₒ : Type} (OuterOStmtOut : Outer_ιₛₒ → Type) [∀ i, OracleInterface (OuterOStmtOut i)]
    {Inner_ιₛᵢ : Type} (InnerOStmtIn : Inner_ιₛᵢ → Type) [∀ i, OracleInterface (InnerOStmtIn i)]
    {Inner_ιₛₒ : Type} (InnerOStmtOut : Inner_ιₛₒ → Type) [∀ i, OracleInterface (InnerOStmtOut i)]
    (OuterWitIn OuterWitOut InnerWitIn InnerWitOut : Type) where
  stmt : OracleStatement.Lens OuterStmtIn OuterStmtOut InnerStmtIn InnerStmtOut
                                  OuterOStmtIn OuterOStmtOut InnerOStmtIn InnerOStmtOut
  wit : Witness.Lens (OuterStmtIn × ∀ i, OuterOStmtIn i) (InnerStmtOut × ∀ i, InnerOStmtOut i)
                          OuterWitIn OuterWitOut InnerWitIn InnerWitOut

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)

inputState_length_eq_outputState_length : inputState.length = outputState.length

Infinite in Mathlib.Data.Finite.Defs

def duplexSpongeToBasicFSQueryImpl :
    QueryImpl (duplexSpongeChallengeOracle StmtIn U)
      (OracleComp (fsChallengeOracle StmtIn pSpec)) :=
  sorry

@[inline, specialize]
def oracleReduction :
  OracleReduction oSpec Unit (fun _ : Fin 2 => OStatement) Unit
    (Query OStatement) (fun _ : Fin 2 => OStatement) Unit (pSpec OStatement) where
  prover := oracleProver oSpec OStatement
  verifier := oracleVerifier oSpec OStatement

instance : HListRepr (HList []) where
  repr := fun _ => ""

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

def MLE (evals : (σ → Fin 2) → R) : MvPolynomial σ R :=
    ∑ x : σ → Fin 2, (eqPolynomial (x : σ → R)) * C (evals x)

instance : OracleInterfaces (vPSpec.toProtocolSpec A) where
  oracleInterfaces := fun _ => some OracleInterface.instVector

def rightpad {m : ℕ} {α : Sort*} (n : ℕ) (a : α) (v : Fin m → α) : Fin n → α :=
  fun i => if h : i < m then v ⟨i, h⟩ else a

tail in ToMathlib.Control.Comonad.Instances

noncomputable def disagreementSet (f : ι → F) (S : Finset F) (Ans : S → F) : Finset F :=
  Set.toFinset ({x : ι | x.val ∈ S ∧ (ansPoly S Ans).eval x.val ≠ f x}.image Subtype.val)

Finset.image in Mathlib.Data.Finset.Image

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

noncomputable def ofPolynomialAlgHom : R[X] →ₐ[R] P := Polynomial.aeval PolynomialLike.X

def degCor
  (φ : ι ↪ F) (dstar degree : ℕ) (r : F) (f : ι → F) (x : ι) : F :=
    f x * ∑ l ∈ range (dstar - degree + 1), ((φ x) * r) ^ l

def proverOutput (i : Fin n) : ProverOutput oSpec
    ((StatementRound R n i.succ × (∀ i, OracleStatement R n deg i)) × Unit)
    ((proverState R n deg i).PrvState (Fin.last 2)) where
  output := fun x => pure (x, ())

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

LT.lt in Init.Prelude

noncomputable def H
  (δ : ℚ) (x₀ : F)
  (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁)
  : F[Z][X] := (exists_factors_with_large_common_root_set k δ x₀ h_gs).choose_spec.choose

Polynomial.degreeLT in Mathlib.RingTheory.Polynomial.Basic

instance (k : ℕ) : Preorder (ConcreteBTField k) where
  le_refl := fun x => BitVec.le_refl x
  le_trans := fun x y z hxy hyz => BitVec.le_trans hxy hyz
  lt := fun x y => x < y
  lt_iff_le_not_ge := fun x y => by admit /- proof elided -/
| intro h_le_xy h_not_le_yx =>
      have x_lt_y:= mt bitvec_statement.mp h_not_le_yx
      push_neg at x_lt_y
      exact x_lt_y

instance : SMul ℕ (UniPoly R) := ⟨nsmul⟩

def baseFoldMatrix (i : Fin r) (h_i : i + 1 < ℓ + 𝓡)
    (y : ↥(sDomain 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, by admit /- proof elided -/
    ⟩)) : Matrix (Fin 2) (Fin 2) L :=
  let fiberMap := qMap_total_fiber 𝔽q β (i := i) (steps := 1)
      (h_i_add_steps := h_i) (y := y)
  let x₀ := fiberMap 0
  let x₁ := fiberMap 1
  fun i j => match i, j with
  | 0, 0 => x₁
  | 0, 1 => -x₀
  | 1, 0 => -1
  | 1, 1 => 1

Finset.map in Mathlib.Data.Finset.Image

@[inline] def zero : Cayley T :=
  ⟨id, by admit /- proof elided -/
  ⟩

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

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

@[reducible, simp]
def mapOStmt (oStmtIn : ∀ i, OStmtIn i) : ∀ i, OStmtOut i := fun i => (hEq i) ▸ oStmtIn (embedIdx i)

Set.Ico in Mathlib.Order.Interval.Set.Defs

Function.update in Mathlib.Logic.Function.Basic

def oracleReduction.firstMessage :
    OracleReduction oSpec
      (Statement R pp) (OracleStatement R pp) (Witness R pp)
      (Statement.AfterFirstMessage R pp) (OracleStatement.AfterFirstMessage R pp) Unit
      ⟨!v[.P_to_V], !v[Witness R pp]⟩ :=
  SendSingleWitness.oracleReduction oSpec
    (Statement R pp) (OracleStatement R pp) (Witness R pp)

@[reducible, simp] def StmtIn : Type := R

@[reducible] def NonInteractiveProver (Message : Type) {ι : Type} (oSpec : OracleSpec ι)
    (StmtIn WitIn StmtOut WitOut : Type) :=
  Prover oSpec StmtIn WitIn StmtOut WitOut ⟨!v[.P_to_V], !v[Message]⟩

instance [inst : ∀ i, OracleInterface (pSpec₁.Message i)] :
    ∀ i, OracleInterface ((pSpec₁.cast hn).Message i) :=
  fun i => inst (dcast₂ hn.symm (by admit /- proof elided -/
  ) i)

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

def ratchetUnchecked [Permute C] (sponge : DuplexSponge U C) : DuplexSponge U C :=
  simulateQ' forwardPermutationOracleImpl (ratchet sponge) (by admit /- proof elided -/
  )

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

none
</all_available_defs>

<all_available_lemmas>
Fin.is_le in Init.Data.Fin.Lemmas
Nat.lt_of_add_right_lt in Init.Data.Nat.Basic
Nat.lt_of_le_of_lt in Init.Prelude
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
Decidable.not_not in Init.PropLemmas
Fin.eq_of_val_eq in Init.Prelude
Fin.is_lt in Init.Data.Fin.Lemmas
Fintype.card_fin in Mathlib.Data.Fintype.Card
Fintype.card_setUniv in Mathlib.Data.Fintype.Card
Set.card_image_of_injective in Mathlib.Data.Set.Finite.Basic
false_or in Init.SimpLemmas
imp_false in Init.Core
left_eq_ite_iff in Init.PropLemmas
one_ne_zero in Mathlib.Algebra.NeZero
right_eq_ite_iff in Init.PropLemmas
zero_ne_one in Mathlib.Algebra.NeZero
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
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
forall_const in Init.PropLemmas
ite_eq_left_iff in Init.PropLemmas
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
ENat.coe_le_coe in Mathlib.Data.ENat.Basic
ENat.coe_lt_coe in Mathlib.Data.ENat.Basic
ENat.coe_mul in Mathlib.Data.ENat.Basic
ENat.coe_toNat in Mathlib.Data.ENat.Basic
Finset.card_biUnion in Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.card_le_card in Mathlib.Data.Finset.Card
Finset.coe_univ in Mathlib.Data.Fintype.Defs
Finset.mem_biUnion in Mathlib.Data.Finset.Union
Finset.mem_filter in Mathlib.Data.Finset.Filter
Finset.mem_image in Mathlib.Data.Finset.Image
Finset.mem_univ in Mathlib.Data.Fintype.Defs
Finset.sum_congr in Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_const in Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.card_ofFinset in Mathlib.Data.Fintype.Card
Nat.add_sub_cancel in Init.Data.Nat.Basic
Nat.card_coe_set_eq in Mathlib.Data.Set.Card
Nat.card_eq_fintype_card in Mathlib.SetTheory.Cardinal.Finite
Nat.le_of_lt_succ in Init.Prelude
Nat.lt_add_of_pos_right in Init.Data.Nat.Basic
Nat.lt_of_le_pred in Init.Data.Nat.Basic
Nat.ofNat_pos in Mathlib.Data.Nat.Cast.Order.Ring
Nat.pos_of_neZero in Init.Data.Nat.Basic
Nat.pow_add in Init.Data.Nat.Lemmas
Nat.pow_lt_pow_right in Init.Data.Nat.Lemmas
Nat.sInf_mem in Mathlib.Data.Nat.Lattice
Nat.sub_mul in Init.Data.Nat.Basic
Set.image_nonempty in Mathlib.Data.Set.Image
Set.image_univ in Mathlib.Data.Set.Image
Set.nonempty_iff_ne_empty' in Mathlib.Data.Set.Basic
Set.toFinset_card in Mathlib.Data.Fintype.Card
Set.toFinset_range in Mathlib.Data.Fintype.Sets
Set.toFinset_setOf in Mathlib.Data.Fintype.Sets
Set.univ_nonempty in Mathlib.Data.Set.Basic
SetLike.mem_coe in Mathlib.Data.SetLike.Basic
Submodule.coe_mem in Mathlib.Algebra.Module.Submodule.Defs
Submodule.nonempty in Mathlib.Algebra.Module.Submodule.Defs
Subtype.coe_eta in Mathlib.Data.Subtype
WithTop.coe_lt_coe in Mathlib.Order.WithBot
and_self in Init.SimpLemmas
ge_iff_le in Init.Core
le_of_eq_of_le in Init.Core
le_refl in Mathlib.Order.Defs.PartialOrder
le_trans in Mathlib.Order.Defs.PartialOrder
mul_assoc in Mathlib.Algebra.Group.Defs
mul_le_mul_right in Mathlib.Algebra.Order.Monoid.Unbundled.Basic
ne_eq in Init.SimpLemmas
nonempty_subtype in Mathlib.Logic.Nonempty
not_false_eq_true in Init.SimpLemmas
pow_pos in Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic
sInf_le in Mathlib.Order.CompleteLattice.Defs
smul_eq_mul in Mathlib.Algebra.Group.Action.Defs
true_and in Init.SimpLemmas

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

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

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_eq_zero_or_one {k n : Nat} :
  getBit k n = 0 ∨ getBit k n = 1

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

theorem distFromCode_eq_top_iff_empty (u : n → R) (C : Set (n → R)) : Δ₀(u, C) = ⊤ ↔ C = ∅

theorem sub_add_eq_sub_sub_rev (a b c : Nat) (h1 : c ≤ b) (h2 : b ≤ a) :
  a - b + c = a - (b - c)

theorem ConcreteBTFieldAlgebra_apply_assoc (l mid r : ℕ)
    (h_l_le_mid : l ≤ mid) (h_mid_le_r : mid ≤ r) :
    ∀ x : ConcreteBTField l,
    (@ConcreteBTFieldAlgebra (l:=l) (r:=r) (h_le:=by
      exact Nat.le_trans h_l_le_mid h_mid_le_r)).algebraMap x =
    (@ConcreteBTFieldAlgebra (l:=mid) (r:=r) (h_le:=h_mid_le_r)).algebraMap
      ((@ConcreteBTFieldAlgebra (l:=l) (r:=mid) (h_le:=h_l_le_mid)).algebraMap x)

theorem heq_of_dcast (ha : a = a') (hb : dcast ha b = b') : HEq b b'

lemma βᵢ_not_in_Uᵢ (i : Fin r) :
    β i ∉ U 𝔽q β i

lemma quotienting [DecidableEq F] {degree : ℕ} {domain : ι ↪ F} [Nonempty ι]
  (S : Finset F) (hS_lt : S.card < degree) (r : F)
  (f : ι → F) (Ans Fill : S → F) (δ : ℝ) (hδPos : δ > 0) (hδLt : δ < 1)
  (h : ∀ u : code domain degree, u.val ∈ (relHammingBall ↑(code domain degree) f δ) →
    ∃ (x : S) (hx : x.val ∈ S), ((decodeLT u) : F[X]).eval x.val ≠ Ans ⟨x.val, hx⟩) :
    δᵣ((funcQuotient f S Ans Fill), (code domain (degree - S.card))) +
      ((disagreementSet f S Ans).card : ℝ) / (ι.card : ℝ) > δ

theorem join_eq_iff_dcast_extractLsb {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField k)
  (hi_btf lo_btf : ConcreteBTField (k - 1)) :
  x = 《 hi_btf, lo_btf 》 ↔
  (hi_btf = dcast (h_sub_middle h_pos) (BitVec.extractLsb (hi := 2 ^ k - 1) (lo := 2 ^ (k - 1)) x) ∧
  lo_btf = dcast (h_middle_sub) (BitVec.extractLsb (hi := 2 ^ (k - 1) - 1) (lo := 0) x))

theorem join_of_split {k : ℕ} (h_pos : k > 0) (x : ConcreteBTField k)
    (hi_btf lo_btf : ConcreteBTField (k - 1))
    (h_split_eq : split h_pos x = (hi_btf, lo_btf)) :
    x = 《 hi_btf, lo_btf 》

lemma norm_of_ne_zero_is_ne_zero {k : ℕ}
  {h_k_gt_0 : k > 0} (prevBTFieldResult : ConcreteBTFStepResult (k := k - 1))
  (a : ConcreteBTField k) (h_a_ne_zero : a ≠ 0) :
  let a₁ := (split h_k_gt_0 a).1
  let a₀ := (split h_k_gt_0 a).2
  concrete_mul a₀ (a₀ + concrete_mul a₁ (Z (k - 1))) + concrete_mul a₁ a₁ ≠ 0

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

@[simp]
theorem drop_zero (v : (i : Fin n) → α i) : drop 0 n.zero_le v = v

@[simp]
theorem hcons_zero {β : Fin n → Sort u} (a : α) (b : (i : Fin n) → β i) :
    hcons a b 0 = cast (vcons_zero α β).symm a

theorem zero_mul {a : AssocNat} : 0 * a = 0

@[simp]
lemma Transcript.def_eq {k : Fin (n + 1)} {pSpec : ProtocolSpec n} :
    (pSpec.take k k.is_le).FullTranscript =
      ((i : Fin k) → pSpec.«Type» (Fin.castLE (by omega) i))

congrArg in Init.Prelude

@[simp]
theorem rdrop_eq_take (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) :
    rdrop m h v = take (n - m) (by omega) v

lemma powerBasisSucc_dim (k : ℕ) :
  powerBasisSucc (k:=k).dim = 2

@[simp]
theorem insertNth_last : insertNth (Fin.last n) y s = snoc s y

@[simp, grind] lemma R_pos : 0 < sz.R

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

theorem neg_add_cancel : -p + p = 0

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

theorem LeafData.composeBuild_internal {α} {s_left s_right : Skeleton}
    (left : LeafData α s_left) (right : LeafData α s_right)
    (compose : α → α → α) :
    (LeafData.internal left right).composeBuild compose =
      FullData.internal
        (compose (left.composeBuild compose).getRootValue (right.composeBuild compose).getRootValue)
        (left.composeBuild compose)
        (right.composeBuild compose)

theorem add_zero : @add α zero = @id (ChurchNat α)

lemma algebraMap_adjacent_tower_def (l : ℕ) :
    (algebraMap (ConcreteBTField l) (ConcreteBTField (l + 1))) =
    canonicalAlgMap l

@[simp]
theorem Verifier.id_soundness {lang : Set StmtIn} :
    (Verifier.id : Verifier oSpec _ _ _).soundness init impl lang lang 0

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

private lemma leadingCoeff_E'
  (h_dist : (Δ₀(f, p.eval ∘ ωs) : ℕ) ≤ e)
  : (E ωs f p e).coeff e = 1

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

@[simp]
lemma numFullRounds_pos : 0 < params.numFullRounds

theorem linear_form_of_elements_in_adjoined_commring
    {R : Type*} [CommRing R] (f : R[X]) (hf_deg : f.natDegree = 2)
    (hf_monic : Monic f) (c1 : AdjoinRoot f) :
    ∃ a b : R, c1 = (AdjoinRoot.of f) a * root f + (AdjoinRoot.of f) b

omit [NeZero ℓ] [NeZero r] [NeZero 𝓡] in
lemma fin_r_succ_bound {h_ℓ_add_R_rate : ℓ + 𝓡 < r} (i : Fin r) (h_i : i + 1 < ℓ + 𝓡)
    : i + 1 < r

lemma twoAdicity_maximal : ¬ (2 ^ (twoAdicity + 1)) ∣ (fieldSize - 1)

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

@[simp]
theorem dappend_right {motive : Fin (m + n) → Sort u} (u : (i : Fin m) → motive (castAdd n i))
    (v : (i : Fin n) → motive (natAdd m i)) (i : Fin n) :
    dappend (motive := motive) u v (natAdd m i) = v i

lemma concrete_one_ne_zero {k : ℕ} : (one (k:=k)) ≠ (zero (k:=k))

lemma approximate_solution_is_exact_solution_coeffs
  (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁)
  : ∀ t ≥ k,
  α' 
    x₀ 
    (R k δ x₀ h_gs) 
    (irreducible_H k h_gs) 
    t 
  = 
  (0 : AppendixA.𝕃 (H k δ x₀ h_gs))

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

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

Fin.isLt in Init.Prelude

@[simp]
theorem vconcat_zero (a : α) : vconcat !v[] a = !v[a]

theorem vcons_eq_cons (a : α) (v : Fin n → α) : a ::ᵛ v = cons a v

theorem is_unit_iff_deg_0 {R : Type*} [Field R] {p : R[X]} : p.degree = 0 ↔ IsUnit p

theorem toPoly_toImpl {p : Q[X]} : p.toImpl.toPoly = p

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

omit [CharP L 2] [DecidableEq 𝔽q] h_β₀_eq_1 [NeZero 𝓡] in
lemma firstOracleWitnessConsistencyProp_relay_preserved (i : Fin ℓ)
    (hNCR : ¬ isCommitmentRound ℓ ϑ i) (wit : Witness (L := L) 𝔽q β
      (h_ℓ_add_R_rate := h_ℓ_add_R_rate) i.succ)
    (oStmt : ∀ j, OracleStatement 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ϑ i.castSucc j) :
    firstOracleWitnessConsistencyProp 𝔽q β wit.t (getFirstOracle 𝔽q β oStmt) =
    firstOracleWitnessConsistencyProp 𝔽q β wit.t
      (getFirstOracle 𝔽q β (mapOStmtOutRelayStep 𝔽q β i hNCR oStmt))

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

@[simp]
theorem hflatten_one {n : Fin 1 → ℕ} {α : (i : Fin 1) → (j : Fin (n i)) → Sort*}
    {v : (i : Fin 1) → (j : Fin (n i)) → α i j} : hflatten v = v 0

@[simp]
theorem vflatten_zero {n : Fin 0 → ℕ} {v : (i : Fin 0) → Fin (n i) → α} : vflatten v = !v[]

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 seqCompose_succ_dir {m : ℕ} {n : Fin (m + 1) → ℕ} {pSpec : ∀ i, ProtocolSpec (n i)} :
    (seqCompose pSpec).dir = Fin.vflatten (fun i => (pSpec i).dir)

@[simp]
theorem LeafData.get_internal_ofRight {α} {s_left s_right : Skeleton}
    (left : LeafData α s_left) (right : LeafData α s_right)
    (idxRight : SkeletonLeafIndex s_right) :
    (LeafData.internal left right).get (SkeletonLeafIndex.ofRight idxRight) =
      right.get idxRight

@[simp]
theorem dempty_happend {α : Fin 0 → Sort u} {β : Fin n → Sort u} (v : (i : Fin n) → β i) :
    happend !d⟨α⟩[] v =
      fun i : Fin (0 + n) => cast (by simp) (v <| i.cast (by omega))

theorem eq_zero_of_degreeOf_lt_card_of_eval_eq_zero_of_fin {n : ℕ} {p : R[X Fin n]}
    (S : Fin n → Finset R) (hDegree : ∀ i, p.degreeOf i < (S i).card)
    (hEval : ∀ x ∈ piFinset fun i ↦ S i, eval x p = 0) :
        p = 0

omit [Finite F] in
lemma pow_2_pow_i_mem_Di_of_mem_D :
  ∀ {x : Fˣ} (i : ℕ),
    x ∈ D → x ^ (2 ^ i) ∈ evalDomain D i

@[simp]
lemma natDegree_solutionToQ :
  (solutionToQ e k v).natDegree ≤ e + k - 1

@[simp]
lemma getTypes_hcons (x : Σ α : Type u, α) (xs : HList) :
    (x ::ₕ xs).getTypes = x.1 :: xs.getTypes

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

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

theorem insertNth_right_injective :
    Injective (Finsupp.insertNth p y : (Fin n →₀ M) → Fin (n + 1) →₀ M)

beq_iff_eq in Init.Core

@[simp]
lemma foldl'_succ {n : ℕ} {α : Type u} (f : (i : Fin (n + 1)) → α → α) (x : α) :
    foldl' (n + 1) f x = f (last n) (foldl' n (fun i => f i.castSucc) x)

lemma add_eq_one_iff (a b : ConcreteBTField 0) :
  a + b = 1 ↔ (a = 0 ∧ b = 1) ∨ (a = 1 ∧ b = 0)

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

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

theorem vcons_inj (a b : α) (v w : Fin n → α) : a ::ᵛ v = b ::ᵛ w ↔ a = b ∧ v = w

theorem unique_linear_sum_repr (R : Type*) [CommRing R] (S : Type*) [CommRing S] [Algebra R S]
    (pb : PowerBasis R S) (h_dim : pb.dim = 2) (s : S) :
    ∃! p : R × R, s = p.fst • pb.gen + algebraMap R S p.snd

omit [Finite F] in
lemma mul_root_of_unity {x : Fˣ} :
  ∀ {a b : Fˣ} {i j : ℕ},
    i ≤ j → a ∈ evalDomain D x i → b ∈ Domain.evalDomain D j →
      a * b ∈ evalDomain D x i

lemma definingPoly_coeffOf1 {F : Type*} [Field F] [Fintype F] (s : F) [NeZero s] :
    (definingPoly s).coeff 1 = s

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

theorem bitsToU_bijective (i : Fin r) :
  Function.Bijective (bitsToU (𝔽q := 𝔽q) (β := β) (ℓ := ℓ) (R_rate := R_rate) i)
</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

abbrev OracleFunction (i : Fin (ℓ + 1)) : Type _ := sDomain 𝔽q β h_ℓ_add_R_rate ⟨i, by admit /- proof elided -/
    ⟩ → L

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

end Essentials

section SoundnessTools

def BBF_Code (i : Fin (ℓ + 1)) : Submodule L ((sDomain 𝔽q β h_ℓ_add_R_rate)
    ⟨i, by admit /- proof elided -/
        ⟩ → L) :=
  let domain : (sDomain 𝔽q β h_ℓ_add_R_rate) ⟨i, by admit /- proof elided -/
  ⟩ ↪ L :=
    ⟨fun x => x.val, fun x y h => by admit /- proof elided -/
    ⟩
  ReedSolomon.code (domain := domain) (deg := 2^(ℓ - i.val))

def BBF_CodeDistance (ℓ 𝓡 : ℕ) (i : Fin (ℓ + 1)) : ℕ :=
  2^(ℓ + 𝓡 - i.val) - 2^(ℓ - i.val) + 1

def fiberwiseDisagreementSet (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, by admit /- proof elided -/
      ⟩) :
  Set ((sDomain 𝔽q β h_ℓ_add_R_rate) ⟨i.val + steps, by admit /- proof elided -/
  ⟩) :=
  
    
  {y | ∃ x, iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate (i := i)
    (k := steps) (h_bound := by admit /- proof elided -/
    ) x = y ∧ f x ≠ g x}

def fiberwiseDistance (i : Fin ℓ) (steps : ℕ) [NeZero steps] (h_i_add_steps : i.val + steps ≤ ℓ)
  (f : OracleFunction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ⟨i.val, by admit /- proof elided -/
  ⟩) : ℕ :=
  
  
  let C_i := BBF_Code 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ⟨i.val, by admit /- proof elided -/
  ⟩
  let disagreement_sizes := (fun (g : C_i) =>
    (fiberwiseDisagreementSet 𝔽q β i steps h_i_add_steps f g).ncard) '' Set.univ
  sInf disagreement_sizes

def fiberwiseClose (i : Fin ℓ) (steps : ℕ) [NeZero steps] (h_i_add_steps : i.val + steps ≤ ℓ)
    (f : OracleFunction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
      ⟨i, by admit /- proof elided -/
      ⟩) : Prop :=
  2 * fiberwiseDistance 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) (i := i) steps
    (h_i_add_steps := h_i_add_steps) (f := f) < (BBF_CodeDistance ℓ 𝓡 ⟨i + steps, by admit /- proof elided -/
    ⟩ : ℕ∞)

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

<target_theorem>
theorem fiberwise_dist_lt_imp_dist_lt_unique_decoding_radius (i : Fin ℓ) (steps : ℕ)
    [NeZero steps] (h_i_add_steps : i.val + steps ≤ ℓ)
    (f : OracleFunction 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ⟨i, by omega⟩)
  (h_fw_dist_lt : fiberwiseClose 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate)
    (i := i) (steps := steps) (h_i_add_steps := h_i_add_steps) (f := f)) :
  hammingClose 𝔽q β (h_ℓ_add_R_rate := h_ℓ_add_R_rate) ⟨i, by omega⟩ f :=
</target_theorem>

