Round-six lemma `edge_of_pivs`

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.R6BitNBPiv):

theorem IntMul.Kappa.R6.Bit.NB.edge_of_pivs (hm : 1 < m) (q : Matrix (Fin m) (Fin m) ℚ) (hq : q * q = q)
    (rs : List (ℕ × ℕ × ℕ)) (hok : ∀ ρ ∈ rs, RunOK m ρ) (hnd : (runPairs rs).Nodup)
    (hp : ∀ x ∈ runPairs rs, IsPiv q x.1 x.2) :
    ∃ e : Edge m, (∃ rs', e.runs = rs ++ rs' ∧ (∀ ρ ∈ rs', ρ.2.2 = 1) ∧
        (runPairs rs).length + rs'.length = q.rank) ∧
      (∀ ρ ∈ e.runs, RunOK m ρ) ∧
      (∀ i j, i < j → e.E₁ i j = 0) ∧ (∀ i, e.E₁ i i ≠ 0) ∧
      (∀ i j, i < j → e.E₂ i j = 0) ∧ (∀ i, e.E₂ i i ≠ 0) ∧
      e.E₁ * ((e.runs.flatMap (runPiv m)).map fun p => Equiv.swap p.1 p.2).prod.permMatrix ℚ *
        e.E₂ = pswQ q

Context. Round six, bit network: pivots from ranks, and edges from pivots

• rk q X Y: rank of the rows < X, columns ≥ Y of q; IsPiv q i j: the inclusion–exclusion of rk at (i, j) is one.
• isPiv_iff: for a Bruhat factorization E₁ P E₂, IsPiv is exactly P i j = 1.
• edge_of_pivs: for an idempotent q over ℚ and runs whose positions are pivots of q, there is an edge (lower triangular E₁, E₂, nonzero diagonals) with runs rs ++ rs', rs' singletons, |rs| + |rs'| = rank q, and frame E₁ σ E₂ = pswQ q (the partial swap of q).

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