Round-six lemma `side_edge_of`
ProvedIntMul.Kappa.R6.Bit.NB.side_edge_ofAn 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.side_edge_of (C : Matrix (Pr (h + 4)) (Fin (h + 4)) ℚ)
(A : Matrix (Fin (h + 4)) (Fin (h + 4)) ℚ) (R : Matrix (Fin (h + 4)) (Pr (h + 4)) ℚ)
(hB : ∀ i j : Fin (h + 4), i < j → (Te (h := h) * C) ⟨i.val, by have := two_k_le (h := h); omega⟩ j = 0)
(hBd : ∀ i : Fin (h + 4), (Te (h := h) * C) ⟨i.val, by have := two_k_le (h := h); omega⟩ i ≠ 0)
(hA : ∀ i j : Fin (h + 4), i < j → (R * Te' (h := h)) i
⟨(h + 4) * (h + 4) - (h + 4) + j.val, by have := two_k_le (h := h); omega⟩ = 0)
(hAd : ∀ i : Fin (h + 4), (R * Te' (h := h)) i
⟨(h + 4) * (h + 4) - (h + 4) + i.val, by have := two_k_le (h := h); omega⟩ ≠ 0)
(hM : C * A * R * (C * A * R) = C * A * R) (hAA : A * A = A) (r : ℕ) (hr : A.rank = r)
(hrM : (qM (C * A * R)).rank = r)
(hcor : h + 4 < 2 * r → (A.submatrix (fun l : Fin (h + 4 - r) => (⟨l.val, by omega⟩ : Fin (h + 4)))
(fun c : Fin (h + 4 - r) => (⟨h + 4 - (h + 4 - r) + c.val, by omega⟩ : Fin (h + 4)))).det ≠ 0) :
∃ e : Edge ((h + 4) * (h + 4)), EdgeQ e (qM (C * A * R)) ∧ ∃ rs',
e.runs = sideRuns (h + 4) ((h + 4) * (h + 4)) r ++ rs' ∧ (∀ ρ ∈ rs', ρ.2.2 = 1) ∧
(runPairs (sideRuns (h + 4) ((h + 4) * (h + 4)) r)).length + rs'.length = r
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_R6_Defs4
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Bit IntMul.Kappa.R6.Bit.NB
open Matrix Finset
open scoped Kronecker
variable {h : ℕ}
theorem IntMul.Kappa.R6.Bit.NB.side_edge_of (C : Matrix (Pr (h + 4)) (Fin (h + 4)) ℚ)
(A : Matrix (Fin (h + 4)) (Fin (h + 4)) ℚ) (R : Matrix (Fin (h + 4)) (Pr (h + 4)) ℚ)
(hB : ∀ i j : Fin (h + 4), i < j → (Te (h := h) * C) ⟨i.val, by have := two_k_le (h := h); omega⟩ j = 0)
(hBd : ∀ i : Fin (h + 4), (Te (h := h) * C) ⟨i.val, by have := two_k_le (h := h); omega⟩ i ≠ 0)
(hA : ∀ i j : Fin (h + 4), i < j → (R * Te' (h := h)) i
⟨(h + 4) * (h + 4) - (h + 4) + j.val, by have := two_k_le (h := h); omega⟩ = 0)
(hAd : ∀ i : Fin (h + 4), (R * Te' (h := h)) i
⟨(h + 4) * (h + 4) - (h + 4) + i.val, by have := two_k_le (h := h); omega⟩ ≠ 0)
(hM : C * A * R * (C * A * R) = C * A * R) (hAA : A * A = A) (r : ℕ) (hr : A.rank = r)
(hrM : (qM (C * A * R)).rank = r)
(hcor : h + 4 < 2 * r → (A.submatrix (fun l : Fin (h + 4 - r) => (⟨l.val, by omega⟩ : Fin (h + 4)))
(fun c : Fin (h + 4 - r) => (⟨h + 4 - (h + 4 - r) + c.val, by omega⟩ : Fin (h + 4)))).det ≠ 0) :
∃ e : Edge ((h + 4) * (h + 4)), EdgeQ e (qM (C * A * R)) ∧ ∃ rs',
e.runs = sideRuns (h + 4) ((h + 4) * (h + 4)) r ++ rs' ∧ (∀ ρ ∈ rs', ρ.2.2 = 1) ∧
(runPairs (sideRuns (h + 4) ((h + 4) * (h + 4)) r)).length + rs'.length = r := by sorry