Round-six lemma `bruhat_rank_nat`
ProvedIntMul.Kappa.R6.Bit.RunsLib.RunsAux.bruhat_rank_natAn 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.R6BitNBRunsLib):
theorem IntMul.Kappa.R6.Bit.RunsLib.RunsAux.bruhat_rank_nat {n : ℕ} [DecidableEq K] (E₁ P E₂ : Matrix (Fin n) (Fin n) K)
(hE₁ : ∀ i j, i < j → E₁ i j = 0) (hd₁ : ∀ i, E₁ i i ≠ 0)
(hE₂ : ∀ i j, i < j → E₂ i j = 0) (hd₂ : ∀ i, E₂ i i ≠ 0)
(h01 : ∀ i j, P i j = 0 ∨ P i j = 1)
(hrow : ∀ i j j', P i j = 1 → P i j' = 1 → j = j')
(hcol : ∀ i i' j, P i j = 1 → P i' j = 1 → i = i') (X Y : ℕ) :
((E₁ * P * E₂).submatrix (fun r : {r : Fin n // r.val < X} => r.1)
(fun c : {c : Fin n // Y ≤ c.val} => c.1)).rank =
(univ.filter fun x : Fin n × Fin n => x.1.val < X ∧ Y ≤ x.2.val ∧ P x.1 x.2 = 1).card
Context. Verbatim copy of Solutions/Runs.lean (OpenAI layer) inside a namespace, so that it can be
imported together with other root-level solution theorems.
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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6
open Matrix Finset
variable {K : Type*} [Field K]
theorem IntMul.Kappa.R6.Bit.RunsLib.RunsAux.bruhat_rank_nat {n : ℕ} [DecidableEq K] (E₁ P E₂ : Matrix (Fin n) (Fin n) K)
(hE₁ : ∀ i j, i < j → E₁ i j = 0) (hd₁ : ∀ i, E₁ i i ≠ 0)
(hE₂ : ∀ i j, i < j → E₂ i j = 0) (hd₂ : ∀ i, E₂ i i ≠ 0)
(h01 : ∀ i j, P i j = 0 ∨ P i j = 1)
(hrow : ∀ i j j', P i j = 1 → P i j' = 1 → j = j')
(hcol : ∀ i i' j, P i j = 1 → P i' j = 1 → i = i') (X Y : ℕ) :
((E₁ * P * E₂).submatrix (fun r : {r : Fin n // r.val < X} => r.1)
(fun c : {c : Fin n // Y ≤ c.val} => c.1)).rank =
(univ.filter fun x : Fin n × Fin n => x.1.val < X ∧ Y ≤ x.2.val ∧ P x.1 x.2 = 1).card := by sorry