Flag basis at `h = 23` (round six, `flagBasis`)

Proved

IntMul.Kappa.R6.Bit.NB.flagBasis

by xuanji · Oct 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

Flag basis at h = 23 (n = 23, m = 529), with the kernel-certified data corner.

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

theorem IntMul.Kappa.R6.Bit.NB.flagBasis (Lab : Finset ((Fin (19 + 4) → ℚ) × (Fin (19 + 4) → ℚ)))
    (hLab : ∀ p ∈ Lab, p.2 ⬝ᵥ p.1 = 1)
    (Pis : Finset (Matrix (Fin (19 + 4)) (Fin (19 + 4)) ℚ)) (hPis : ∀ A ∈ Pis, A * A = A) :
    ∃ (S : Matrix (Fin ((19 + 4) * (19 + 4))) (Pr (19 + 4)) ℚ)
      (Sinv : Matrix (Pr (19 + 4)) (Fin ((19 + 4) * (19 + 4))) ℚ),
      S * Sinv = 1 ∧ Sinv * S = 1 ∧
      (∀ p ∈ Lab, AuxE (h := 19) (S * ((1 : Matrix (Fin (19 + 4)) (Fin (19 + 4)) ℚ) ⊗ₖ
          (1 - vecMulVec p.1 p.2)) * Sinv) ∧
        AuxE (h := 19) (S * ((1 - vecMulVec p.1 p.2) ⊗ₖ (1 : Matrix (Fin (19 + 4)) (Fin (19 + 4)) ℚ)) *
          Sinv)) ∧
      (∀ p ∈ Lab, ∀ A ∈ Pis, SideE (h := 19) (S * (A ⊗ₖ vecMulVec p.1 p.2) * Sinv) A.rank ∧
        SideE (h := 19) (S * (vecMulVec p.1 p.2 ⊗ₖ A) * Sinv) A.rank) ∧
      (∀ p₁ ∈ Lab, ∀ p₂ ∈ Lab,
        DataE (h := 19) (S * ((1 - vecMulVec p₁.1 p₁.2) ⊗ₖ (1 - vecMulVec p₂.1 p₂.2)) * Sinv))

Context. Round six, bit network: the flag basis (main theorem of part (c))

flagBasis: for any finite set of labels (x, y) (y ⬝ x = 1) and any finite set of idempotents, at h = 23 (n = 23, m = 529) there is one rational basis change S (S * Sinv = 1 = Sinv * S) in which every edge of every class has the claimed Bruhat runs:

aux 1 ⊗ (1 - x yᵀ), (1 - x yᵀ) ⊗ 1: exactly [(0, m-n, n), (n, n, m-2n)];
side A ⊗ x yᵀ, x yᵀ ⊗ A: sideRuns n m (rank A) plus singletons, total rank A pivots;
data (1 - x₁ y₁ᵀ) ⊗ (1 - x₂ y₂ᵀ): dataRuns n m plus n + 1 singletons.

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

Preamble

-- 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 MvPolynomial
open scoped Kronecker
variable {h : ℕ}

Formal statement

theorem IntMul.Kappa.R6.Bit.NB.flagBasis (Lab : Finset ((Fin (19 + 4) → ℚ) × (Fin (19 + 4) → ℚ)))
    (hLab : ∀ p ∈ Lab, p.2 ⬝ᵥ p.1 = 1)
    (Pis : Finset (Matrix (Fin (19 + 4)) (Fin (19 + 4)) ℚ)) (hPis : ∀ A ∈ Pis, A * A = A) :
    ∃ (S : Matrix (Fin ((19 + 4) * (19 + 4))) (Pr (19 + 4)) ℚ)
      (Sinv : Matrix (Pr (19 + 4)) (Fin ((19 + 4) * (19 + 4))) ℚ),
      S * Sinv = 1 ∧ Sinv * S = 1 ∧
      (∀ p ∈ Lab, AuxE (h := 19) (S * ((1 : Matrix (Fin (19 + 4)) (Fin (19 + 4)) ℚ) ⊗ₖ
          (1 - vecMulVec p.1 p.2)) * Sinv) ∧
        AuxE (h := 19) (S * ((1 - vecMulVec p.1 p.2) ⊗ₖ (1 : Matrix (Fin (19 + 4)) (Fin (19 + 4)) ℚ)) *
          Sinv)) ∧
      (∀ p ∈ Lab, ∀ A ∈ Pis, SideE (h := 19) (S * (A ⊗ₖ vecMulVec p.1 p.2) * Sinv) A.rank ∧
        SideE (h := 19) (S * (vecMulVec p.1 p.2 ⊗ₖ A) * Sinv) A.rank) ∧
      (∀ p₁ ∈ Lab, ∀ p₂ ∈ Lab,
        DataE (h := 19) (S * ((1 - vecMulVec p₁.1 p₁.2) ⊗ₖ (1 - vecMulVec p₂.1 p₂.2)) * Sinv)) := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `IntMul.Kappa.R6.Bit.NB.flagBasis`, Solutions/R6BitNBMain.lean (lines 317–332) of the round-six development.

View graph