Build Witness mem rel In

theorem buildWitness_mem_relIn (hq5 : q % 8 = 5) {b ω γ : ℕ} (hκ : (2 * ω) ^ 2 < q)    (hτ : 0 < zDigits)    (stmt : QuadEvalStatement 𝓜(q, α) innerRows (2 ^ m) messageDigits outerRows (2 ^ r) innerDigits      dRows)    (v : CarrierCom 𝓜(q, α) dRows)    (fam : Fin (2 ^ r + 1) → (Fin (2 ^ r) → ShortChallenge 𝓜(q, α) ω))    (resp : Fin (2 ^ r + 1) →      QuadEvalResponse 𝓜(q, α) innerRows (2 ^ m) messageDigits (2 ^ r) innerDigits zDigits)    (hrel : ∀ j, ((stmt, v, fam j), resp j) ∈ relOut 𝓜(q, α) (b : ZMod q) ω γ)    (hstar : ∃ e, StarAt fam e) :    (stmt, buildWitness 𝓜(q, α) (b : ZMod q) stmt v fam resp) ∈      relIn 𝓜(q, α) (b : ZMod q)        (quadEvalBetaSq γ b zDigits ((𝓜(q, α)).φ.natDegree) m messageDigits) γ (2 * ω) := by  unfold buildWitness  by_cases hB : ∃ j, PolyVec.flattenBlocks (resp j).innerDec      ≠ PolyVec.flattenBlocks (resp (central fam)).innerDec  · -- Case (A): some branch's inner decomposition differs → `B`-kernel MSIS solution    -- (both branches' c2 commit to the shared `stmt.u`).    rw [dif_pos hB]    obtain ⟨-, hu₁, -, -, -, -, hγ₁, -⟩ := hrel hB.choose    obtain ⟨-, hu₂, -, -, -, -, hγ₂, -⟩ := hrel (central fam)    exact msis_of_commit_eq 𝓜(q, α) stmt.pp.outerMatrix hu₁ hu₂ hγ₁ hγ₂ hB.choose_spec  · by_cases hD : ∃ j, (resp j).carrierDec ≠ (resp (central fam)).carrierDec    · -- Case (B): shared `t̂` but some carrier decomposition differs → `D`-kernel MSIS solution      -- (the shared round-0 message `v` is what makes both branches commit to the same `v`).      rw [dif_neg hB, dif_pos hD]      obtain ⟨hv₁, -, -, -, -, hγ₁, -, -⟩ := hrel hD.choose      obtain ⟨hv₂, -, -, -, -, hγ₂, -, -⟩ := hrel (central fam)      exact msis_of_commit_eq 𝓜(q, α) stmt.pp.dMatrix hv₁ hv₂ hγ₁ hγ₂ hD.choose_spec    · -- Case (C): shared `t̂` and `ŵ` → the subtract-and-divide weak opening.      rw [dif_neg hB, dif_neg hD]      push Not at hB hD      have ht : ∀ j, (resp j).innerDec = (resp (central fam)).innerDec :=        fun j => funext fun i => PolyVec.block_eq_of_flattenBlocks_eq (hB j) i      exact ⟨verifiedOpening_of_star hq5 hκ hτ stmt v fam resp hrel hstar ht hD,        evalConsistency_of_relOut_star hq5 hκ stmt v fam resp hrel hstar hD⟩