Round-six lemma `isPiv_mid`

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

theorem IntMul.Kappa.R6.Bit.NB.isPiv_mid {m k : ℕ} (hk : 2 * k ≤ m) (p : Matrix (Fin m) (Fin m) K) (hp : p * p = p)
    (hrank : p.rank = m - k)
    (hC : (p.submatrix (fun l : Fin k => (⟨l.val, by omega⟩ : Fin m))
        (fun r : Fin k => (⟨m - k + r.val, by omega⟩ : Fin m))).det ≠ 0)
    {i : ℕ} (hi1 : k ≤ i) (hi2 : i < m - k) : IsPiv p i i

Context. Round six, bit network: pivot lemmas

• isPiv_block: pivots of a block in the top-right part pass to the whole matrix.
• isPiv_diag_of_lower: a lower triangular matrix with nonzero diagonal pivots on its diagonal.
• isPiv_mid: an idempotent of rank m - k with invertible k × k corner pivots on the middle diagonal (CornerLib.solution).
• isPiv_rank1_lower: a matrix that is rank one strictly above the diagonal pivots at (l, l).
• rk_mul_lower, isPiv_side: lower triangular factors keep the rank profile; the pivots of B M A (B with lower triangular top, A with lower triangular right end) are those of M, moved to the top-right corner.

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