Round-six lemma `data_edge`

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

The following holds (Lean statement, in the scope of module Solutions.R6BitNBEdges):

theorem IntMul.Kappa.R6.Bit.NB.data_edge (x₁ y₁ x₂ y₂ : Fin (h + 4) → ℚ) (h₁ : y₁ ⬝ᵥ x₁ = 1) (h₂ : y₂ ⬝ᵥ x₂ = 1)
    (hu : x₁ ⟨0, by omega⟩ * x₂ ⟨0, by omega⟩ ≠ 0)
    (hv : y₁ ⟨h + 3, by omega⟩ * y₂ ⟨h + 3, by omega⟩ ≠ 0)
    (hT : ∀ l (hl1 : 1 ≤ l) (hl2 : l ≤ h + 2),
      x₁ ⟨l, by omega⟩ * y₁ ⟨h + 3, by omega⟩ + x₂ ⟨l, by omega⟩ * y₂ ⟨h + 3, by omega⟩ ≠ 0)
    (hdet : (Matrix.of fun i j : Fin (2 * h + 7) =>
      cor ((1 - vecMulVec x₁ y₁) ⊗ₖ (1 - vecMulVec x₂ y₂)) i.val j.val).det ≠ 0) :
    ∃ e : Edge ((h + 4) * (h + 4)),
      EdgeQ e (qM ((1 - vecMulVec x₁ y₁) ⊗ₖ (1 - vecMulVec x₂ y₂))) ∧ ∃ rs',
      e.runs = dataRuns (h + 4) ((h + 4) * (h + 4)) ++ rs' ∧ (∀ ρ ∈ rs', ρ.2.2 = 1) ∧
      rs'.length = h + 5

Context. Round six, bit network: edges of the classes (over ℚ)

EdgeQ e q: valid runs, lower triangular E₁, E₂ with nonzero diagonals, and frame E₁ σ E₂ = pswQ q. For each class, under the genericity conditions on the transformed labels, an edge with the claimed runs exists.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).