Round-six κ development, definitions part 50

Definition

IntMul_Kappa_R6_Defs50

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

complexity-theoryinteger-multiplicationkappa-improvement

Definition bundle IntMul_Kappa_R6_Defs50 of the round-six κ-improvement development. It collects the definitions (data types, parameter maps, network and program structures, and the few lemmas that these definitions need) of the Lean modules Solutions.R6ChkBitBase, extracted by skeleton subtraction from the source files with their namespaces, variable declarations and opens unchanged.

The theorems about these objects are published as separate platform nodes that import this bundle.

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

Definition code

-- 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

section
-- Source module: Solutions.R6ChkBitBase
/-!
# Bit round six (h = 23): support trees and triple tables

* `BT`: a binary tree of numbers; `btGet t d i` follows the low `d` bits of `i` (most significant
  first). Node supports (bitmasks over the 1771 triples of `Fin 23`) are stored 16 per leaf in
  1792-bit fields (`R6BitDataSup*`), read by `fieldOf`.
* `TRIPL`: row `i` (32-bit field) is the bitmask of the `i`-th triple (lexicographic order);
  `STARL`: field `c` (1792 bits) is `star c`, the set of triples containing `c`;
  `UMT0..3`: field `b` of `UMTj` is the set of triples meeting the 6-bit chunk `b` of points
  `6j, …, 6j+5` (so `um P` = triples meeting `P` is four lookups).
* Table facts are proved by one kernel evaluation each (`star_spec`, `umt_spec`).
-/

namespace R6Chk.Bit

open R6Chk

/-- Binary trees of numbers. -/
inductive BT where
  | leaf (x : ℕ)
  | node (l r : BT)

end R6Chk.Bit

end

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 modules Solutions/R6ChkBitBase.lean.

View graph