Prove2Me

The single generator of a line `psp a b C` (`C` one bit `c`) is the vector of `2^a ||| 2^b ||| C` (`line_gen`)

Proved
IntMul.Kappa.R6.Cx.NetF2.line_gen

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

complexity-theoryinteger-multiplicationkappa-improvement

The single generator of a line psp a b C (C one bit c) is the vector of 2^a ||| 2^b ||| C.

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

theorem IntMul.Kappa.R6.Cx.NetF2.line_gen {a b C : ℕ} (hp : PspOK a b C) (h1 : pc24 C = 1) (c : Fin 24) (hc : C.testBit c = true) :
    ev a + ev b + ev c = bitv (2 ^ a ||| 2 ^ b ||| C)

Context. Labels of the h = 24 local program: codes over 𝔽₂^24 and a sound Boolean edge checker

A label code (Code) is one of

  • coord X: span {e_p : p ∈ X};
  • psp a b C: span {e_a + e_b + e_c : c ∈ C} (a "pair span"; a line ⟨t⟩ is psp p q {r});
  • perp t: ⟨t⟩^⊥ (a triple t);
  • ext k: boundary labels of stage two (decoded elsewhere).

Vectors are 24-bit naturals (bitv). edgeB new old = true implies NetComplexP8.EdgeOK (dec new) (dec old) (edgeB_sound), with finrank (dec c) = dimC c (finrank_dec). All functions are kernel-friendly (straight-line bit operations, SWAR popcount).

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_Defs24

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Cx IntMul.Kappa.R6.Cx.NetF2
open Matrix Finset Matrix.Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8
Formal statement
theorem IntMul.Kappa.R6.Cx.NetF2.line_gen {a b C : ℕ} (hp : PspOK a b C) (h1 : pc24 C = 1) (c : Fin 24) (hc : C.testBit c = true) :
    ev a + ev b + ev c = bitv (2 ^ a ||| 2 ^ b ||| C) := 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.Cx.NetF2.line_gen`, Solutions/R6CxNetF2.lean (lines 534–577) of the round-six development.

View graph