Common part (`aux_edge_of`)

Common part: an idempotent qM M of rank m - n whose n × n corner is lower triangular with nonzero diagonal has the aux runs.

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

theorem IntMul.Kappa.R6.Bit.NB.aux_edge_of (M : Matrix (Pr (h + 4)) (Pr (h + 4)) ℚ) (hM : M * M = M)
    (htr : M.trace = ((h + 4) * (h + 3) : ℕ))
    (hlow : ∀ β γ : ℕ, β < γ → γ < h + 4 → cor M β (h + 3 + γ) = 0)
    (hdiag : ∀ β : ℕ, β < h + 4 → cor M β (h + 3 + β) ≠ 0) :
    ∃ e : Edge ((h + 4) * (h + 4)), EdgeQ e (qM M) ∧
      e.runs = [(0, (h + 4) * (h + 4) - (h + 4), h + 4),
        (h + 4, h + 4, (h + 4) * (h + 4) - 2 * (h + 4))]

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