Inner relation of verified

theorem inner_relation_of_verified {base : ZMod q} {βSq γ κ : Nat}    {pp : PublicParams 𝓜(q, α)      innerRows messageRows messageDigits outerRows blocks innerDigits}    {u : Commitment 𝓜(q, α) outerRows}    {opening₁ opening₂ :      Opening 𝓜(q, α) innerRows messageRows messageDigits blocks innerDigits}    (hv₁ : VerifiedOpening 𝓜(q, α) base βSq γ κ pp u opening₁)    (hv₂ : VerifiedOpening 𝓜(q, α) base βSq γ κ pp u opening₂)    (hflat : PolyVec.flattenBlocks opening₁.innerDecomp =      PolyVec.flattenBlocks opening₂.innerDecomp)    {i : Fin blocks} (hmsgNe : opening₁.message i ≠ opening₂.message i) :    ModuleSIS.relation 𝓜(q, α) (innerShort 𝓜(q, α) κ βSq)      pp.innerMatrix (scaledMessage 𝓜(q, α) opening₁ opening₂ i -        scaledMessage 𝓜(q, α) opening₂ opening₁ i)      = true := by  have hB₁ := hv₁.block i  have hB₂ := hv₂.block i  have hne : scaledMessage 𝓜(q, α) opening₁ opening₂ i -      scaledMessage 𝓜(q, α) opening₂ opening₁ i ≠ 0 :=    sub_ne_zero.mpr (scaledMessage_ne_of_message_ne 𝓜(q, α) hB₁ hB₂ hmsgNe)  have hshort : ‖scaledMessage 𝓜(q, α) opening₁ opening₂ i -        scaledMessage 𝓜(q, α) opening₂ opening₁ i‖₂² ≤        subL2NormSqBound (scalarVecMulMulL2NormSqBound κ βSq) :=    sub_l2NormSq_le 𝓜(q, α) _ _ (scaledMessage_l2NormSq_le α hB₁ hB₂)      (scaledMessage_l2NormSq_le α hB₂ hB₁)  have hinnerEq := inner_commit_eq_of_flatten_eq 𝓜(q, α) hv₁ hv₂ hflat i  have heq : pp.innerMatrix *ᵥ scaledMessage 𝓜(q, α) opening₁ opening₂ i =      pp.innerMatrix *ᵥ scaledMessage 𝓜(q, α) opening₂ opening₁ i := by    simpa [scaledMessage, Simple.commit] using      matVecMul_scalarVecMul_mul_eq_of_eq pp.innerMatrix (opening₁.challenge i)        (opening₂.challenge i) (by simpa [Simple.commit] using hinnerEq)  have hker : pp.innerMatrix *ᵥ      (scaledMessage 𝓜(q, α) opening₁ opening₂ i -        scaledMessage 𝓜(q, α) opening₂ opening₁ i) = 0 := by    rw [matVecMul_sub]; exact sub_eq_zero.mpr heq  simp [ModuleSIS.relation, innerShort, hne, hshort, hker]