Round-six lemma `step`
ProvedIntMul.Kappa.R6.Bit.RunsLib.BruhatAux.stepAn 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.BruhatAux.step (B : Matrix (Fin m) (Fin m) K) (k : Fin m) (hB : Clean B k.val) :
∃ L R : Matrix (Fin m) (Fin m) K, LowerND L ∧ LowerND R ∧ Clean (L * B * R) (k.val + 1)
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_R6_Defs51
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.RunsLib IntMul.Kappa.R6.Bit.RunsLib.BruhatAux
open Matrix Finset
variable {K : Type*} [Field K] {m : ℕ}
theorem IntMul.Kappa.R6.Bit.RunsLib.BruhatAux.step (B : Matrix (Fin m) (Fin m) K) (k : Fin m) (hB : Clean B k.val) :
∃ L R : Matrix (Fin m) (Fin m) K, LowerND L ∧ LowerND R ∧ Clean (L * B * R) (k.val + 1) := by sorry