Round-six κ development, definitions part 52

Definition
IntMul_Kappa_R6_Defs52
by xuanji · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)
complexity-theoryinteger-multiplicationkappa-improvement
Definition bundle IntMul_Kappa_R6_Defs52 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.R6BitNBNetA, Solutions.R6BitNBNetB, Solutions.R6BitNBNetC, R6Pk.R6BitNBNetD, Solutions.R6BitNBStmt, R6Pk.R6BitNBNetE, 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_R6_Defs51
import Mathlib
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_KappaJainData
import Definitions.Def_IntMul_Kappa_R6_Defs4
import Definitions.Def_IntMul_Kappa_R6_Data_BitNBGenData_0
import Definitions.Def_IntMul_Kappa_R6_Data_BitNBGenData_2
import Definitions.Def_IntMul_Kappa_K_Defs1
import Definitions.Def_IntMul_Kappa_R6_Data_BitNBGenData_3

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.R6BitNBNetA
/-!
# Round six, bit network: the network (definitions, wires, generic fold lemmas)

Global roles (`v = 1771`, `N = v² = 3136441`, `R = 40077`): `X(a₁, a₂) = a₁ v + a₂`,
`Y(a₁, a₂) = N + a₁ v + a₂`, `A₁(b, q) = 2N + b R + q`, `A₂(a, q) = 2N + v R + a R + q`
(`W = 2N + 2vR = 148225616`). Temporaries: `tmp₁(b, c) = 23 b + c`, `tmp₂(a, c) = 23 v + 23 a + c`,
`τ(a₁, a₂) = 46 v + a₁ v + a₂` (`T = 46 v + N = 3217907`).

Stage-one invocation `b` maps the local wires `x_t ↦ X(t, b)`, `y_T ↦ Y(T, b)`, `s_q ↦ A₁(b, q)`,
`tmp_c ↦ tmp₁(b, c)`; stage-two invocation `a` maps `x_t ↦ Y(a, t)`, `y_S ↦ X(a, S)`,
`s_q ↦ A₂(a, q)`, `tmp_c ↦ tmp₂(a, c)`, `u_S ↦ τ(a, S)` (local `u_S = 43642 + S`).

Program: for each `b`, the stage-one chunks then the aux exits on its slots; then for each `a`, the
entrance edges on its `x`, `y` and slot wires, the stage-two chunks and the copy corrections.
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Bit.NB

open Matrix R6Chk R6Chk.Bit R6Chk.Bit.Loc AModel AModelFac

/-! ## Generic fold lemmas -/

/-! ## Wires -/

abbrev Wr := Fin 148225616 ⊕ Fin 3217907

def gw (g : ℕ) : Wr :=
  if h : g < 148225616 then .inl ⟨g, h⟩ else .inr ⟨(g - 148225616) % 3217907, Nat.mod_lt _ (by norm_num)⟩

/-- Stage-one local-to-global map. -/
def g1 (b w : ℕ) : ℕ :=
  if w < 1771 then w * 1771 + b
  else if w < 3542 then 3136441 + (w - 1771) * 1771 + b
  else if w < 43619 then 6272882 + b * 40077 + (w - 3542)
  else 148225616 + 23 * b + (w - 43619)

/-- Stage-two local-to-global map. -/
def g2 (a w : ℕ) : ℕ :=
  if w < 1771 then 3136441 + a * 1771 + w
  else if w < 3542 then a * 1771 + (w - 1771)
  else if w < 43619 then 77249249 + a * 40077 + (w - 3542)
  else if w < 43642 then 148225616 + 40733 + 23 * a + (w - 43619)
  else 148225616 + 81466 + a * 1771 + (w - 43642)

def ι1 (b w : ℕ) : Wr := gw (g1 b w)
def ι2 (a w : ℕ) : Wr := gw (g2 a w)

/-- Local `u` wires (correction temporaries). -/
def wU (s : ℕ) : ℕ := 43642 + s

/-! ## The network -/

/-- The stage chunk lists. -/
@[irreducible] def cs1 : List LChunk := (genF (codeOf SG1_0) W1F).2
@[irreducible] def cs2 : List LChunk := (genF (codeOf SG2_0) W2F).2

/-- The chosen edges and the flag basis. -/
structure Ch where
  S : Matrix (Fin 529) (Pr 23) ℚ
  Si : Matrix (Pr 23) (Fin 529) ℚ
  e1 : ℕ → ℕ → ℕ → Edge 529
  e2 : ℕ → ℕ → ℕ → Edge 529
  ex : ℕ → Edge 529
  en : ℕ → ℕ → Edge 529
  ei : ℕ → Edge 529
  ec : ℕ → ℕ → Edge 529

abbrev NI := Instr Wr (ZMod 2) 529

/-- Entrance edges of stage-two invocation `a` on its local wire `w < 43619`. -/
def entE (ch : Ch) (a w : ℕ) : Edge 529 :=
  if w < 1771 then ch.en a w else if w < 3542 then ch.en a (w - 1771) else ch.ei a

def blk1 (ch : Ch) (b : ℕ) : List NI :=
  chunkProg (ι1 b) (ch.e1 b) cs1 ++ (List.range' 3542 40077).map fun w => Instr.edge (ι1 b w) (ch.ex b)

def corrI (ch : Ch) (a s : ℕ) : List NI :=
  [xorG (ι2 a (wU s)) (ι2 a (wY s)), Instr.edge (ι2 a (wU s)) (ch.ec a s), xorG (ι2 a (wX s)) (ι2 a (wU s))]

def entI (ch : Ch) (a : ℕ) : List NI := (List.range 43619).map fun w => Instr.edge (ι2 a w) (entE ch a w)

def blk2 (ch : Ch) (a : ℕ) : List NI :=
  entI ch a ++ (chunkProg (ι2 a) (ch.e2 a) cs2 ++ (List.range 1771).flatMap (corrI ch a))

def prog (ch : Ch) : List NI := (List.range 1771).flatMap (blk1 ch) ++ (List.range 1771).flatMap (blk2 ch)

def ρn (g : ℕ) : ℕ := if g < 3136441 then g + 3136441 else if g < 6272882 then g - 3136441 else g

def ρ (w : Fin 148225616) : Fin 148225616 := ⟨ρn w.val, by unfold ρn; split_ifs <;> omega⟩

/-- **The round-six bit network.** -/
def net (ch : Ch) : QHNet (ZMod 2) 148225616 3217907 529 := ⟨prog ch, ρ⟩

end IntMul.Kappa.R6.Bit.NB

end

section
-- Source module: Solutions.R6BitNBNetB
/-!
# Round six, bit network: frame labels (`LabGates` for the whole program)

At field size `N`, under `EOK ch N` (flag basis, good denominators and the frame matrices of the
chosen edges), the whole program is label consistent from the initial labels `L0`, and the final
labels are: `swapMat` on `X(a, s)`, `A₁`, `A₂`, and `Φ₂(a, ND(s + 1))` on `Y(a, s)`.
-/

set_option linter.unusedSectionVars false
set_option maxRecDepth 10000
set_option linter.constructorNameAsVariable false

namespace IntMul.Kappa.R6.Bit.NB

open Matrix R6Chk R6Chk.Bit R6Chk.Bit.Loc AModel AModelFac

/-- Hypotheses at field size `N`. -/
structure EOK (ch : Ch) (N : ℕ) : Prop where
  hS : ch.S * ch.Si = 1
  hSi : ch.Si * ch.S = 1
  gS : GoodM N ch.S
  gSi : GoodM N ch.Si
  gPc : ∀ c < 38286, GoodM N (Pc c)
  gPl : ∀ b < 1771, GoodM N (Pl b)
  m1 : ∀ b < 1771, ∀ o < 38286, ∀ c < 38286, nestOK o c = true →
    edgeMat N (ch.e1 b o c) = redM N (pswQ (K ch.S ch.Si (Dm o c) (Pl b)))
  m2 : ∀ a < 1771, ∀ o < 38286, ∀ c < 38286, nestOK o c = true →
    edgeMat N (ch.e2 a o c) = redM N (pswQ (K ch.S ch.Si (Pl a) (Dm o c)))
  mx : ∀ b < 1771, edgeMat N (ch.ex b) = redM N (pswQ (K ch.S ch.Si 1 (1 - Pl b)))
  mn : ∀ a < 1771, ∀ t < 1771, edgeMat N (ch.en a t) = redM N (pswQ (K ch.S ch.Si (1 - Pl a) (1 - Pl t)))
  mi : ∀ a < 1771, edgeMat N (ch.ei a) = redM N (pswQ (K ch.S ch.Si (1 - Pl a) 1))
  mc : ∀ a < 1771, ∀ s < 1771, edgeMat N (ch.ec a s) = redM N (pswQ (K ch.S ch.Si (Pl a) (Pl s)))

noncomputable def lab1 (ch : Ch) (N b c : ℕ) : FMat 529 N := redM N (Φ₁ ch.S ch.Si b c)
noncomputable def lab2 (ch : Ch) (N a c : ℕ) : FMat 529 N := redM N (Φ₂ ch.S ch.Si a c)

/-! ## Stage facts -/

section Lab

variable {ch : Ch} {N : ℕ} (h : EOK ch N)
include h

/-- Final labels of stage one. -/
noncomputable def fin1 (ch : Ch) (N b w : ℕ) : FMat 529 N :=
  if 3542 ≤ w ∧ w < 43619 then swapMat else lab1 ch N b (codeOf SG1_11 w)

/-! ## Block two -/

noncomputable def pre2 (ch : Ch) (N a w : ℕ) : FMat 529 N :=
  if w < 1771 then lab1 ch N w (cPT a) else if w < 3542 then lab1 ch N (w - 1771) cHIGH
  else if w < 43619 then 1 else if w < 43642 then lab2 ch N a (codeOf SG2_0 w) else swapMat

noncomputable def fin2 (ch : Ch) (N a w : ℕ) : FMat 529 N :=
  if w < 43642 then lab2 ch N a (codeOf SG2_10 w) else lab2 ch N a (cND (w - 43642 + 1))

/-- Correction wires. -/
def cw (s j : ℕ) : ℕ := if j = 0 then wU s else if j = 1 then wY s else wX s

/-- Correction pre/post labels. -/
noncomputable def cf (ch : Ch) (N a s j : ℕ) : FMat 529 N :=
  if j = 0 then swapMat else if j = 1 then swapMat else lab2 ch N a (cND (s + 1))
noncomputable def cg (ch : Ch) (N a s j : ℕ) : FMat 529 N :=
  if j = 1 then swapMat else lab2 ch N a (cND (s + 1))

attribute [local irreducible] LabGates

end Lab

/-! ## The whole program -/

/-- Initial labels. -/
noncomputable def L0 (ch : Ch) (N : ℕ) : Wr → FMat 529 N
  | .inl g => if g.val < 3136441 then lab1 ch N (g.val % 1771) (cND (g.val / 1771 + 1)) else 1
  | .inr t => if t.val < 40733 then lab1 ch N (t.val / 23) (codeOf SG1_0 (43619 + t.val % 23))
      else if t.val < 81466 then lab2 ch N ((t.val - 40733) / 23) (codeOf SG2_0 (43619 + (t.val - 40733) % 23))
      else swapMat

end IntMul.Kappa.R6.Bit.NB

end

section
-- Source module: Solutions.R6BitNBNetC
/-!
# Round six, bit network: the scalar circuit and formal correctness (`FormalOK`)

The module-valued scalar circuit (formal values over `ZMod 2`) of the whole program: stage one
adds `X(T, b)` into `Y(T, b)`, stage two adds `Y(a, S)` into `X(a, S)`, the correction adds
`X` into `τ` and `τ` into `Y`. With the labels of `R6BitNBNetB` and `formal_labels`, every role
`ρ w` ends with `(swapMat, w)`.
-/

set_option linter.unusedSectionVars false
set_option maxRecDepth 10000
set_option linter.constructorNameAsVariable false

namespace IntMul.Kappa.R6.Bit.NB

open Matrix R6Chk R6Chk.Bit R6Chk.Bit.Loc AModel AModelFac

section Scalar

variable {N : ℕ}

abbrev FVN (N : ℕ) := FV (ZMod 2) (Fin 148225616) 529 N

/-- Initial scalar values. -/
noncomputable def φ0 (ch : Ch) (N : ℕ) : Wr → FVN N
  | .inl g => if g.val < 3136441 then Finsupp.single (L0 ch N (.inl g), g) 1 else Finsupp.single (1, g) 1
  | .inr _ => 0

variable (ch : Ch)

noncomputable def u1 (ch : Ch) (N b w : ℕ) : FVN N := φ0 ch N (ι1 b w)

/-- Stage-two initial local values. -/
noncomputable def u2 (ch : Ch) (N a w : ℕ) : FVN N :=
  if w < 1771 then φ0 ch N (ι1 w (wY a)) + φ0 ch N (ι1 w (wX a)) else φ0 ch N (ι2 a w)

/-- The correction block on scalars. -/
noncomputable def cfS (ch : Ch) (N a s j : ℕ) : FVN N :=
  if j = 0 then 0 else if j = 1 then xrL G2 (u2 ch N a) (wY s) else xrL G2 (u2 ch N a) (wX s)
noncomputable def cgS (ch : Ch) (N a s j : ℕ) : FVN N :=
  if j = 0 then xrL G2 (u2 ch N a) (wY s) else if j = 1 then xrL G2 (u2 ch N a) (wY s)
  else xrL G2 (u2 ch N a) (wX s) + xrL G2 (u2 ch N a) (wY s)

noncomputable def fin2S (ch : Ch) (N a w : ℕ) : FVN N :=
  if w < 1771 then xrL G2 (u2 ch N a) w + xrL G2 (u2 ch N a) (wY w)
  else if w < 43642 then xrL G2 (u2 ch N a) w else xrL G2 (u2 ch N a) (wY (w - 43642))

end Scalar

/-! ## Formal correctness -/

end IntMul.Kappa.R6.Bit.NB

end

section
-- Source module: R6Pk.R6BitNBNetD
/-!
# Round six, bit network: the edges (flag basis) and good primes

The frame basis `S`, `S⁻¹` and every edge come from `flagBasis` (labels `(xv T, yv T)`, idempotents
`Dm o c` for nested moves and `Pl b`). Out-of-range parameters give the trivial edge, so all edges
of the network lie in one finite set `E0`; `good_edges` / `good_mats` give a prime bound `q₀`
above which `EOK`, `EdgesOK` and `FormalOK` hold mod every prime power.
-/

set_option linter.unusedSectionVars false
set_option maxRecDepth 10000
set_option linter.constructorNameAsVariable false

namespace IntMul.Kappa.R6.Bit.NB

open Matrix R6Chk R6Chk.Bit R6Chk.Bit.Loc AModel AModelFac
open scoped Kronecker

/-! ## Choosing edges -/

def dfltE : Edge 529 := ⟨1, [], 1⟩

open Classical in
noncomputable def pickE (P : Edge 529 → Prop) : Edge 529 :=
  if h : ∃ e, P e then Classical.choose h else dfltE

def SideR (r : ℕ) (rs : List (ℕ × ℕ × ℕ)) : Prop :=
  ∃ rs', rs = sideRuns 23 529 r ++ rs' ∧ (∀ ρ ∈ rs', ρ.2.2 = 1) ∧
    (runPairs (sideRuns 23 529 r)).length + rs'.length = r

def DataR (rs : List (ℕ × ℕ × ℕ)) : Prop :=
  ∃ rs', rs = dataRuns 23 529 ++ rs' ∧ (∀ ρ ∈ rs', ρ.2.2 = 1) ∧ rs'.length = 24

def AuxR (rs : List (ℕ × ℕ × ℕ)) : Prop := rs = auxRuns 19

def PE (q : Matrix (Fin 529) (Fin 529) ℚ) (R : List (ℕ × ℕ × ℕ) → Prop) (e : Edge 529) : Prop :=
  EdgeQ e q ∧ R e.runs

/-! ## The flag basis -/

noncomputable def Lab0 : Finset (V23 × V23) := (Finset.range 1771).image fun T => (xv T, yv T)

/-- Nested move index pairs (irreducible: products of big ranges make the elaborator unfold
`List.range`). -/
noncomputable def idxD : Finset (ℕ × ℕ) :=
  ((Finset.range 38286) ×ˢ (Finset.range 38286)).filter (fun p => nestOK p.1 p.2 = true)

def I3 : Finset (ℕ × ℕ × ℕ) := Finset.range 1771 ×ˢ (Finset.range 38286 ×ˢ Finset.range 38286)

def I2 : Finset (ℕ × ℕ) := Finset.range 1771 ×ˢ Finset.range 1771

attribute [irreducible] idxD I3 I2

noncomputable def Pis0 : Finset M23 := idxD.image (fun p => Dm p.1 p.2) ∪ (Finset.range 1771).image Pl

attribute [irreducible] Pis0

/-- The flag-basis property (the statement of `flagBasis` for `Lab0`, `Pis0`). -/
abbrev FB0 (S : Matrix (Fin ((19 + 4) * (19 + 4))) (Pr (19 + 4)) ℚ)
    (Sinv : Matrix (Pr (19 + 4)) (Fin ((19 + 4) * (19 + 4))) ℚ) : Prop :=
  S * Sinv = 1 ∧ Sinv * S = 1 ∧
      (∀ p ∈ Lab0, 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 ∈ Lab0, ∀ A ∈ Pis0, 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₁ ∈ Lab0, ∀ p₂ ∈ Lab0,
        DataE (h := 19) (S * ((1 - vecMulVec p₁.1 p₁.2) ⊗ₖ (1 - vecMulVec p₂.1 p₂.2)) * Sinv))

/-- The flag basis (chosen by `Classical.epsilon`, so the definition carries no proof). -/
noncomputable def S0 : Matrix (Fin 529) (Pr 23) ℚ := Classical.epsilon (fun S => ∃ Sinv, FB0 S Sinv)
noncomputable def Si0 : Matrix (Pr 23) (Fin 529) ℚ := Classical.epsilon (fun Sinv => FB0 S0 Sinv)

/-! ## The network's edges -/

noncomputable def ch0 : Ch where
  S := S0
  Si := Si0
  e1 b o c := if b < 1771 ∧ o < 38286 ∧ c < 38286 then
    pickE (PE (K S0 Si0 (Dm o c) (Pl b)) (SideR (rkC o c))) else dfltE
  e2 a o c := if a < 1771 ∧ o < 38286 ∧ c < 38286 then
    pickE (PE (K S0 Si0 (Pl a) (Dm o c)) (SideR (rkC o c))) else dfltE
  ex b := if b < 1771 then pickE (PE (K S0 Si0 1 (1 - Pl b)) AuxR) else dfltE
  en a t := if a < 1771 ∧ t < 1771 then pickE (PE (K S0 Si0 (1 - Pl a) (1 - Pl t)) DataR) else dfltE
  ei a := if a < 1771 then pickE (PE (K S0 Si0 (1 - Pl a) 1) AuxR) else dfltE
  ec a s := if a < 1771 ∧ s < 1771 then pickE (PE (K S0 Si0 (Pl a) (Pl s)) (SideR 1)) else dfltE

noncomputable instance instDecEqEdge : DecidableEq (Edge 529) := Classical.decEq _

noncomputable def E0 : Finset (Edge 529) :=
  (I3.image fun p => ch0.e1 p.1 p.2.1 p.2.2) ∪ (I3.image fun p => ch0.e2 p.1 p.2.1 p.2.2) ∪
    ((Finset.range 1771).image ch0.ex) ∪ (I2.image fun p => ch0.en p.1 p.2) ∪
    ((Finset.range 1771).image ch0.ei) ∪ (I2.image fun p => ch0.ec p.1 p.2) ∪ {dfltE}

attribute [irreducible] E0

/-! ## Every edge of the program is one of the chosen families -/

def Fam (ch : Ch) (e : Edge 529) : Prop :=
  (∃ b o c, e = ch.e1 b o c) ∨ (∃ a o c, e = ch.e2 a o c) ∨ (∃ b, e = ch.ex b) ∨
    (∃ a t, e = ch.en a t) ∨ (∃ a, e = ch.ei a) ∨ (∃ a s, e = ch.ec a s)

/-! ## Good primes -/

noncomputable def M0 : Finset M23 := (Finset.range 38286).image Pc ∪ (Finset.range 1771).image Pl

noncomputable def EM0 : Finset (QMat2 529) := E0.image Edge.E₁ ∪ E0.image Edge.E₂

end IntMul.Kappa.R6.Bit.NB

-- #print axioms IntMul.Kappa.R6.Bit.NB.net0_ok

end

section
-- Source module: Solutions.R6BitNBStmt
/-!
# Round six, bit side: the statement `bitNetR6` (interface)

Accepted restatement (coordinator, 2026-10-19): the round-six bit network as a `QHNet` over
`ZMod 2` with `W = 148225616` roles and `m = 529`, valid runs, admissible Bruhat data and formal
frame correctness at every power of every large prime, and Jain's histogram. Consumed through
`prop11H_formal`.

`bitNetR6_mom` is the moment-dominance variant (all that `prop11H_formal` / `costH_bound` use):
it follows from `bitNetR6` (`bitNetR6_mom_of`).

This file holds the statements only (sorry-free). The pending `bitNetR6` lives in
`R6BitNBStmtX`; `bitNetR6_mom` is proved in `R6BitNBNetE`.
-/

namespace IntMul.Kappa.R6.Bit

/-- **Moment-dominance variant.** -/
def BitNetR6MomStmt : Prop :=
  ∃ (T : ℕ) (C : QHNet (ZMod 2) 148225616 T 529) (q₀ : ℕ), C.RunsOK ∧
    (∀ q, q.Prime → q₀ < q → ∀ f, C.EdgesOK (q ^ f) ∧ C.FormalOK (q ^ f)) ∧
    ∀ τ : ℝ, 0 < τ → τ ≤ 1 → histMoment C.hist 529 τ ≤ histMoment Jain.bitR6 529 τ

end IntMul.Kappa.R6.Bit

end

section
-- Source module: R6Pk.R6BitNBNetE
/-!
# Round six, bit network: the child-width histogram and `BitNetR6MomStmt`

Every edge of the network contributes the moment of its runs: side edges of rank `r` give
`f (2r - 23) + (23 - r) f 1` (`2r > 23`) or `r f 1`, aux edges `f 23 + f 483`, data edges
`f 439 + f 21 + 24 f 1`. The per-rank move counts of the two stage words are the base-`2³²` digits
of the kernel-checked packed counts `CNs1`, `CNs2` (no overflow: `touch1`, `touch2`). The total
moment equals Jain's `bitR6` moment.
-/

set_option linter.unusedSectionVars false
set_option maxRecDepth 10000
set_option linter.constructorNameAsVariable false

namespace IntMul.Kappa.R6.Bit.NB

open Matrix R6Chk R6Chk.Bit R6Chk.Bit.Loc AModel AModelFac

/-! ## Generic list facts -/

/-! ## Edge moments -/

section Mom

variable (τ : ℝ)

noncomputable def fw (w : ℕ) : ℝ := ((w : ℝ) / 529) ^ τ

noncomputable def EM (e : Edge 529) : ℝ := (e.runs.map fun ρ => fw τ ρ.2.2).sum

noncomputable def sideV (r : ℕ) : ℝ :=
  if 23 < 2 * r then fw τ (2 * r - 23) + ((23 - r : ℕ) : ℝ) * fw τ 1 else (r : ℝ) * fw τ 1

noncomputable def auxV : ℝ := fw τ 23 + fw τ 483

noncomputable def dataV : ℝ := fw τ 439 + fw τ 21 + 24 * fw τ 1

end Mom

/-! ## The moment of the network -/

section Net

variable (τ : ℝ)

noncomputable def RS (cs : List LChunk) : ℝ := ((mvRanks cs).map (sideV τ)).sum

end Net

/-! ## Rank counts from the packed counts -/

/-- The per-rank move counts (both stages). -/
def DC (i : ℕ) : ℕ := CNs1 / 2 ^ (32 * i) % 2 ^ 32

/-! ## The statement -/

end IntMul.Kappa.R6.Bit.NB

-- #print axioms IntMul.Kappa.R6.Bit.NB.bitNetR6_mom

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/R6BitNBNetA.lean, Solutions/R6BitNBNetB.lean, Solutions/R6BitNBNetC.lean, Solutions/R6BitNBNetD.lean, Solutions/R6BitNBStmt.lean, Solutions/R6BitNBNetE.lean.
View graph