Prove2Me

Round-six κ development, definitions part 25

Definition
IntMul_Kappa_R6_Defs25

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

complexity-theoryinteger-multiplicationkappa-improvement

Definition bundle IntMul_Kappa_R6_Defs25 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.R6CxNetChk2_0, Solutions.R6CxNetChk2_1, Solutions.R6CxNetChk2_2, Solutions.R6CxNetChk2_3, Solutions.R6CxNetChk2_4, Solutions.R6CxNetChk2_5, Solutions.R6CxNetChk2_6, Solutions.R6CxNetChk2_7, Solutions.R6CxNetChk2_8, Solutions.R6CxNetChk2_9, Solutions.R6CxNetChk2_10, Solutions.R6CxNetChk2_11, Solutions.R6CxNetChk2_12, Solutions.R6CxNetChk2_13, Solutions.R6CxNetOps, Solutions.R6CxNetSeg, Solutions.R6CxNetChkI, Solutions.R6CxNetInvoc, Solutions.R6CxNetGlobL, Solutions.R6CxNetGlobS, Solutions.R6CxNetHist, Solutions.R6CxNetFinal, R6Pk.R6CxNetG, 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_Defs24
import Mathlib
import Definitions.Def_IntMul_KappaJainData
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_Kappa_R6_Data_CxNetData_1
import Definitions.Def_IntMul_Kappa_R6_Data_CxNetDataS1_0
import Definitions.Def_IntMul_Kappa_R6_Data_CxNetDataS2_0
import Definitions.Def_IntMul_Kappa_K_Defs6
import Definitions.Def_IntMul_Kappa_R6_Data_CxNetDataS1_14
import Definitions.Def_IntMul_Kappa_R6_Data_CxNetDataS2_14
import Definitions.Def_IntMul_Kappa_R6_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs3
import Definitions.Def_IntMul_Kappa_K_Defs4
import Definitions.Def_IntMul_Kappa_K_Defs8
import Definitions.Def_IntMul_Kappa_K_Defs15
import Definitions.Def_IntMul_Kappa_R6_Defs21

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.R6CxNetChk2_0
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 0 of stage 2 (`{552: 49208, 529: 2024}`). -/
def H2_0 : ℕ := 0xc03800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000007e800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_1
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 1 of stage 2 (`{529: 2024, 1: 20263, 23: 2047, 24: 1}`). -/
def H2_1 : ℕ := 0x7e800000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001007ff00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000004f2700000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_2
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 2 of stage 2 (`{3: 4796, 4: 2442, 2: 242, 6: 66, 8: 66, 10: 66, 12: 66, 14: 66, 16: 66, 18: 1196, 20: 22, 22: 234}`). -/
def H2_2 : ℕ := 0xea000000001600000004ac000000004200000000420000000042000000004200000000420000000042000000098a012bc000f20000000000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_3
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 3 of stage 2 (`{3: 3486, 4: 2433, 18: 196, 22: 30, 2: 22, 6: 6, 8: 6, 10: 6, 12: 6, 14: 6, 16: 6, 20: 2, 1: 682, 5: 341}`). -/
def H2_3 : ℕ := 0x1e000000000200000000c4000000000600000000060000000006000000000600000000060000000006001550098100d9e00016002aa00000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_4
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 4 of stage 2 (`{3: 914, 4: 871, 1: 221, 5: 1039, 2: 2112, 6: 896, 8: 388, 10: 387, 12: 367, 14: 351, 16: 277, 18: 135, 20: 131, 22: 465}`). -/
def H2_4 : ℕ := 0x1d1000000008300000000870000000115000000015f000000016f0000000183000000018400000003800040f003670039200840000dd00000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_5
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 5 of stage 2 (`{2: 3516, 10: 415, 4: 376, 12: 443, 6: 1234, 14: 475, 8: 414, 16: 396, 18: 198, 20: 198, 22: 343, 5: 680, 3: 198}`). -/
def H2_5 : ℕ := 0x15700000000c600000000c6000000018c00000001db00000001bb000000019f000000019e00000004d2002a800178000c600dbc0000000000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_6
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 6 of stage 2 (`{2: 3790, 6: 1204, 8: 412, 10: 414, 4: 378, 12: 400, 14: 398, 16: 271, 18: 199, 20: 199, 22: 72, 5: 240, 3: 198, 1: 100, 7: 78, 11: 14, 15: 10, 9: 19, 13: 10, 17: 30}`). -/
def H2_6 : ℕ := 0x4800000000c700000000c70001e0010f0000a0018e0000a001900000e0019e000130019c0004e004b4000f00017a000c600ece0006400000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_7
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 7 of stage 2 (`{9: 173, 2: 1534, 4: 1010, 13: 134, 1: 576, 5: 570, 11: 142, 10: 248, 8: 392, 6: 333, 7: 409, 17: 312, 15: 134, 19: 388, 12: 248, 18: 98, 3: 544, 22: 544, 16: 148, 14: 372}`). -/
def H2_7 : ℕ := 0x220000000000000184000620013800094000860017400086000f80008e000f8000ad00188001990014d0023a003f200220005fe0024000000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_8
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 8 of stage 2 (`{1: 640, 5: 719, 2: 1520, 7: 499, 4: 978, 11: 156, 15: 144, 8: 384, 9: 192, 13: 144, 6: 292, 17: 342, 10: 240, 12: 178, 19: 352, 18: 42, 14: 264, 3: 256, 22: 256, 16: 36}`). -/
def H2_8 : ℕ := 0x1000000000000001600002a0015600024000900010800090000b20009c000f0000c000180001f300124002cf003d200100005f00028000000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_9
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 9 of stage 2 (`{5: 733, 2: 1528, 7: 559, 1: 402, 4: 1100, 11: 182, 15: 168, 8: 322, 9: 224, 13: 168, 6: 268, 17: 399, 10: 154, 12: 112, 19: 291, 18: 26, 14: 204, 3: 78, 22: 78, 16: 38}`). -/
def H2_9 : ℕ := 0x4e0000000000001230001a0018f00026000a8000cc000a800070000b60009a000e0001420022f0010c002dd0044c0004e005f80019200000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_10
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 10 of stage 2 (`{5: 518, 2: 1352, 7: 399, 1: 551, 4: 896, 11: 130, 15: 120, 8: 492, 9: 160, 13: 120, 6: 720, 17: 285, 10: 150, 12: 61, 19: 89, 18: 4, 14: 32, 3: 242, 22: 2, 16: 12}`). -/
def H2_10 : ℕ := 0x2000000000000059000040011d0000c0007800020000780003d0008200096000a0001ec0018f002d00020600380000f2005480022700000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_11
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 11 of stage 2 (`{4: 1593, 8: 851, 2: 1860, 12: 530, 16: 638, 10: 360, 14: 430, 6: 188, 18: 1757, 3: 878, 20: 66, 22: 559, 1: 214, 19: 214}`). -/
def H2_11 : ℕ := 0x22f0000000042000d6006dd000000027e00000001ae00000002120000000168000000035300000000bc00000006390036e00744000d600000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_12
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 12 of stage 2 (`{3: 906, 22: 8285, 16: 409, 2: 822, 18: 233, 12: 220, 1: 6298, 19: 226, 14: 258, 4: 372, 6: 360, 10: 144, 8: 96}`). -/
def H2_12 : ℕ := 0x205d0000000000000e2000e90000000199000000010200000000dc00000000900000000060000000016800000001740038a003360189a00000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetChk2_13
namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw

/-- Packed histogram of segment 13 of stage 2 (`{23: 2024, 1: 14696, 2: 8184, 5: 3320, 6: 1254, 4: 762, 8: 1166, 10: 904, 12: 764, 16: 918, 20: 5008, 14: 816, 18: 4160, 22: 11, 7: 1704, 9: 768, 13: 576, 11: 624, 15: 622, 17: 1151, 19: 1800}`). -/
def H2_13 : ℕ := 0x7e80000b000000139000708010400047f003960026e0033000240002fc0027000388003000048e006a8004e600cf8002fa0000001ff80396800000

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetOps
/-!
# Every spec's ops act on its own wires (`OpsIn`)

`progK_sound` needs `OpsIn s` for every spec of a checked segment; here it is derived from the
data facts `DataOK` (gate slots in range, readout slots in range, gates with inputs).
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Cx.NetEff

open NetSpec NetMask NetScal NetLoc NetFast

variable (d : Dat)

@[simp] lemma ws_mk (V : ℕ) (ws : List ℕ) (ops : List (ℕ × ℕ × ℤ)) : (Spec.mk V ws ops).ws = ws := rfl
@[simp] lemma ops_mk (V : ℕ) (ws : List ℕ) (ops : List (ℕ × ℕ × ℤ)) : (Spec.mk V ws ops).ops = ops := rfl

/-- The data facts used by the stage effects and the op/wire checks. -/
structure DataOK : Prop where
  gok : GOK (d.gates.flatMap gq)
  src : ∀ t < NV, d.src t < NR
  rd : RdOK d
  len : d.pieces.length = NV
  ins : ∀ g ∈ d.gates, g.ins ≠ []

/-! ## The segments -/

end IntMul.Kappa.R6.Cx.NetEff

end

section
-- Source module: Solutions.R6CxNetSeg
/-!
# Chaining the kernel label checks of the two stage programs

`stage1Seg` / `stage2Seg`: the checked programs `specs1 dat` / `specs2 dat` from the snapshot
states `S1_0` / `S2_0` are valid (`progChk … = true`), with the summed packed histograms and move
counts, ending in `S1_14` / `S2_14`.
-/

set_option maxRecDepth 100000
set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Cx.NetSeg

open NetBT NetLoc NetSpec NetFast NetRaw NetData NetEff

variable {nl : ℕ} {mvOK : ℕ → ℕ → ℕ → Bool} {wd : ℕ → ℕ → ℕ → ℕ}

/-- A checked segment from `t` to `t'` with packed histogram `H` and move count `C`. -/
def Seg (nl : ℕ) (mvOK : ℕ → ℕ → ℕ → Bool) (wd : ℕ → ℕ → ℕ → ℕ) (ss : List Spec) (t t' : BT)
    (H C : ℕ) : Prop :=
  (progChk nl mvOK wd ss t).1 = true ∧ (progChk nl mvOK wd ss t).2.1 = H ∧
    (progChk nl mvOK wd ss t).2.2.1 = C ∧ (progRun ss t).2 = t'

end IntMul.Kappa.R6.Cx.NetSeg

end

section
-- Source module: Solutions.R6CxNetChkI
/-!
# Kernel checks of the boundary states and of the triple data

* `chkW`: the snapshot trees are well formed;
* `chkI1` / `chkI2`: the initial snapshots hold `init1` / `init2`;
* `chkF1` / `chkF2`: the final codes of the `x`, `y`, `a` wires;
* `chkTV`: every triple mask has three bits and its line code is `psp a b {c}` with `{a,b,c}` the triple;
* `chkG`: every gate has an input.
-/

set_option Elab.async false

namespace IntMul.Kappa.R6.Cx.NetData

open NetBT NetLoc NetSpec NetFast NetRaw NetMask

/-- `f i` for all `i < n` (recursor form). -/
def allN (f : ℕ → Bool) (n : ℕ) : Bool := Nat.rec (motive := fun _ => Bool) true (fun i ih => f i && ih) n

/-- Final codes of stage one: `x ↦ ⊤`, `y_S ↦ perp t_S`, `a ↦ ⊤`. -/
def fin1 (w : ℕ) : ℕ :=
  cond (Nat.blt w NV) TOPC (cond (Nat.blt w (2 * NV)) (perpC (dat.tv (w - NV))) TOPC)

/-- Final codes of stage two: `x_b ↦ ⟨t_b⟩`, `y ↦ ⊥`, `a ↦ ⊥`. -/
def fin2 (w : ℕ) : ℕ := cond (Nat.blt w NV) (dat.lc w) 0

/-- The line code of triple `t`: `psp a b C` with `C` one bit, `a, b ∉ C`, and the triple mask is
`2^a ||| 2^b ||| C`. -/
def lineOK (t : ℕ) : Bool :=
  let c := dat.lc t
  let a := Nat.mod (Nat.div c 4) 32
  let b := Nat.mod (Nat.div c 128) 32
  let C := Nat.div c 4096
  Nat.beq (Nat.mod c 4) 1 && Nat.blt a 24 && Nat.blt b 24 && !(Nat.beq a b) && Nat.beq (pcR C) 1 &&
    !(Nat.testBit C a) && !(Nat.testBit C b) &&
    Nat.beq (dat.tv t) (Nat.lor (Nat.lor (Nat.pow 2 a) (Nat.pow 2 b)) C)

end IntMul.Kappa.R6.Cx.NetData

end

section
-- Source module: Solutions.R6CxNetInvoc
/-!
# One stage invocation in global terms

* `triOK`, `dataOK`: the data facts (from the kernel checks);
* `G1 b` / `G2 a`: the global chunk programs of stage-one invocation `b` / stage-two invocation `a`
  (the checked local program mapped by `ι1 b` / `ι2 a` with the frames of `R6CxNetFrame`);
* `inv1` / `inv2`: validity and labels (from `prog_valid`);
* `log1` / `log2`: the logical effect (from `NetEff.stage1/2` via `runOps_map`);
* `wid1` / `wid2`: the child widths are the nonzero checked move widths (independent of `b`/`a`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx.NetG

open Matrix Finset Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8 NetF2 NetT NetLoc
  NetSpec NetBT NetFast NetMask NetData NetEff NetSeg NetScal NetFr NetRaw

/-! ## Data facts -/

/-! ## Local-to-global plumbing -/

/-! ## Role lemmas -/

/-! ## The two invocation programs -/

/-- The checked local programs. -/
def cs1 : List LChunk := (progRun (specs1 dat) S1_0).1
def cs2 : List LChunk := (progRun (specs2 dat) S2_0).1

/-- Stage-one invocation `b`. -/
noncomputable def G1 (b : ℕ) : List (GChunk Rl 576) :=
  mapProg (ι1 b) (labV1 dat b) (fun _ c => labV1 dat b c) cs1

/-- Stage-two invocation `a`. -/
noncomputable def G2 (a : ℕ) : List (GChunk Rl 576) :=
  mapProg (ι2 a) (labV2 dat a) (lab2 dat a) cs2

/-! ## Widths -/

/-- The nonzero move widths of the two local programs. -/
def W1 : List ℕ := (progMvW wd1 cs1).filter (fun x => x != 0)
def W2 : List ℕ := (progMvW wd2 cs2).filter (fun x => x != 0)

end IntMul.Kappa.R6.Cx.NetG

end

section
-- Source module: Solutions.R6CxNetGlobL
/-!
# The global chunk program and its labels

`CH = S1 ++ E4s ++ S2 ++ KK`:
* `S1`: stage-one invocations `G1 b` (`b < v`);
* `E4s`: for every `b`, the scratch outputs `A1(b, ·)` moved `𝔽₂^24 ⊗ t_b → ⊤` (E4, width 552);
* `S2`: stage-two invocations `G2 a`;
* `KK`: per `(a, b)` the sign corrections `τ += X` (at `⊤`), `Y += τ` (at `⟨u_{ab}⟩^⊥`, moving `τ`
  by E5, width 1), `X ← -X` (at `⊤`).

`progValid_CH`: the program is valid from the initial labels `g0`; `gF_*`: the final labels.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option maxRecDepth 20000

namespace IntMul.Kappa.R6.Cx.NetG

open Matrix Finset Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8 NetF2 NetT NetLoc
  NetSpec NetBT NetFast NetMask NetData NetEff NetSeg NetScal NetFr NetRaw

/-! ## Numeric role codes -/

/-! ## Initial labels -/

/-- The initial labels: stage-one roles get the stage-one initial codes, stage-two scratch roles
the stage-two initial codes, the correction temporaries `⊤`. -/
noncomputable def g0 (r : Rl) : Lab 576 :=
  if rc r < 2 * NN + NV * NR ∨ (Wn ≤ rc r ∧ rc r < Wn + 24 * NV) then
    labV1 dat (d1 (rc r)).1 (init1 dat (d1 (rc r)).2)
  else if (2 * NN + NV * NR ≤ rc r ∧ rc r < Wn) ∨ (Wn + 24 * NV ≤ rc r ∧ rc r < Wn + 48 * NV) then
    lab2 dat (d2 (rc r)).1 (d2 (rc r)).2 (init2 dat (d2 (rc r)).2)
  else ⊤

/-! ## Distinctness -/

/-! ## Kernel-checked boundary codes -/

/-! ## Moves to distinct roles -/

/-! ## The program -/

/-- The E4 chunk of `b`: the scratch outputs `A1(b, ·)` to `⊤`. -/
noncomputable def E4mv (b : ℕ) : List (Rl × Lab 576) :=
  (List.range NR).map (fun q => (A1r b q, lift1 (tb dat b) ⊤))

attribute [local irreducible] E4mv

noncomputable def E4c (b : ℕ) : GChunk Rl 576 := ⟨⊤, E4mv b, []⟩

/-- The correction vector `u_{ab} = t_a ⊗ t_b`. -/
def Uv (a b : ℕ) : V576 := NetT.tens (tb dat a) (tb dat b)

/-- `⟨u_{ab}⟩^⊥`. -/
def Up (a b : ℕ) : Lab 576 := orth 1 (lineM (Uv a b))

noncomputable def C1 (a b : ℕ) : GChunk Rl 576 := ⟨⊤, [], [⟨τr a b, Xr a b, 1⟩]⟩
noncomputable def C2 (a b : ℕ) : GChunk Rl 576 := ⟨Up a b, [(τr a b, ⊤)], [⟨Yr a b, τr a b, 1⟩]⟩
noncomputable def C3 (a b : ℕ) : GChunk Rl 576 := ⟨⊤, [], [⟨Xr a b, Xr a b, -2⟩]⟩

/-- The corrections of `(a, b)`. -/
noncomputable def K (p : ℕ × ℕ) : List (GChunk Rl 576) := [C1 p.1 p.2, C2 p.1 p.2, C3 p.1 p.2]

/-- All pairs. -/
def PL : List (ℕ × ℕ) := List.product (List.range NV) (List.range NV)

noncomputable def S1 : List (GChunk Rl 576) := (List.range NV).flatMap G1
noncomputable def E4s : List (GChunk Rl 576) := (List.range NV).map E4c
noncomputable def S2 : List (GChunk Rl 576) := (List.range NV).flatMap G2
noncomputable def KK : List (GChunk Rl 576) := PL.flatMap K

/-- **The global chunk program.** -/
noncomputable def CH : List (GChunk Rl 576) := S1 ++ E4s ++ S2 ++ KK

attribute [local irreducible] S1 E4s S2 KK PL

/-! ## Stage one -/

/-- Labels after stage-one invocations `b < k`. -/
def P1 (k : ℕ) (g : Rl → Lab 576) : Prop :=
  (∀ b < NV, ∀ w < NL, g (ι1 b w) = labV1 dat b (gget (if b < k then S1_14 else S1_0) w)) ∧
  (∀ r, (∀ b < NV, ∀ w < NL, ι1 b w ≠ r) → g r = g0 r)

/-- Labels after stage one. -/
noncomputable def gS1 : Rl → Lab 576 := progLab S1 g0

/-! ## E4 -/

/-- Labels after the E4 chunks `b < k`. -/
def Q4 (k : ℕ) (g : Rl → Lab 576) : Prop :=
  (∀ b < NV, ∀ q < NR, g (A1r b q) = if b < k then ⊤ else gS1 (A1r b q)) ∧
  (∀ r, (∀ b < k, ∀ q < NR, A1r b q ≠ r) → g r = gS1 r)

/-- Labels after the E4 chunks. -/
noncomputable def gE : Rl → Lab 576 := progLab E4s gS1

/-! ## Stage two -/

/-- Labels after stage-two invocations `a < k`. -/
def P2 (k : ℕ) (g : Rl → Lab 576) : Prop :=
  (∀ a < NV, ∀ w < NL, g (ι2 a w) = lab2 dat a w (gget (if a < k then S2_14 else S2_0) w)) ∧
  (∀ r, (∀ a < NV, ∀ w < NL, ι2 a w ≠ r) → g r = gE r)

/-- Labels after stage two. -/
noncomputable def gS2 : Rl → Lab 576 := progLab S2 gE

/-! ## Corrections -/

/-- Final labels. -/
noncomputable def gF : Rl → Lab 576 := progLab CH g0

/-! ## Initial labels of the data roles -/

end IntMul.Kappa.R6.Cx.NetG

end

section
-- Source module: Solutions.R6CxNetGlobS
/-!
# The logical effect of the global chunk program

With all temporaries starting at zero (`Λ0 (inr _) = 0`), the logical state after `CH` is, on
the data roles, `X(a,b) ↦ Y0(a,b)`, `Y(a,b) ↦ X0(a,b)`, `A ↦ A0` (`ΛF_X`, `ΛF_Y`, `ΛF_A1`, `ΛF_A2`):
stage one adds `X` to `Y`, stage two subtracts `Y` from `X`, the corrections fix the signs.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option maxRecDepth 20000

namespace IntMul.Kappa.R6.Cx.NetG

open Matrix Finset Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8 NetF2 NetT NetLoc
  NetSpec NetBT NetFast NetMask NetData NetEff NetSeg NetScal NetFr NetRaw

variable {Vt : Type*} [AddCommGroup Vt] [Module ℂ Vt]

/-! ## Stage one -/

def L1 (Λ0 : Rl → Vt) (k : ℕ) (Λ : Rl → Vt) : Prop :=
  (∀ b < NV, ∀ S < NV, Λ (Yr S b) = Λ0 (Yr S b) + (if b < k then Λ0 (Xr S b) else 0)) ∧
  (∀ b < NV, ∀ t < NV, Λ (Xr t b) = Λ0 (Xr t b)) ∧
  (∀ b < NV, ∀ q < NR, Λ (A1r b q) = Λ0 (A1r b q)) ∧
  (∀ b < NV, k ≤ b → ∀ j < 24, Λ (M1r b j) = 0) ∧
  (∀ r, (∀ b < NV, ∀ w < NL, ι1 b w ≠ r) → Λ r = Λ0 r)

variable (Λ0 : Rl → Vt) (htemp : ∀ n, Λ0 (Sum.inr n) = 0)
include htemp

/-- The logical state after stage one. -/
noncomputable def Λ1 : Rl → Vt := runOps (progOps S1) Λ0

/-! ## Stage two -/

def L2 (Λ1 : Rl → Vt) (k : ℕ) (Λ : Rl → Vt) : Prop :=
  (∀ a < NV, ∀ S < NV, Λ (Xr a S) = Λ1 (Xr a S) - (if a < k then Λ1 (Yr a S) else 0)) ∧
  (∀ a < NV, ∀ t < NV, Λ (Yr a t) = Λ1 (Yr a t)) ∧
  (∀ a < NV, ∀ q < NR, Λ (A2r a q) = Λ1 (A2r a q)) ∧
  (∀ a < NV, k ≤ a → ∀ j < 24, Λ (M2r a j) = 0) ∧
  (∀ r, (∀ a < NV, ∀ w < NL, ι2 a w ≠ r) → Λ r = Λ1 r)

/-- The logical state after stage two. -/
noncomputable def Λ2 : Rl → Vt := runOps (progOps S2) (Λ1 Λ0)

/-! ## Corrections -/

/-! ## The final logical state on the data roles -/

/-- The logical state after the whole program. -/
noncomputable def ΛF : Rl → Vt := runOps (progOps CH) Λ0

end IntMul.Kappa.R6.Cx.NetG

end

section
-- Source module: Solutions.R6CxNetHist
/-!
# The child-width histogram of the global chunk program

* `W1`, `W2` (nonzero move widths of the two checked local programs) have the histograms `h1`, `h2`
  (decoded from the kernel-checked packed sums, `multiset_of_pack`);
* `progWidths CH` = `v` copies of `W1`, `v·R` widths 552 (E4), `v` copies of `W2`, `v²` widths 1 (E5);
* `CH_hist`: its multiset is `histMS cxR6`; `CH_small`: every width is `< 576`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option maxRecDepth 20000

namespace IntMul.Kappa.R6.Cx.NetG

open Matrix Finset Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8 NetF2 NetT NetLoc
  NetSpec NetBT NetFast NetMask NetData NetEff NetSeg NetScal NetFr NetRaw

/-- Histogram of the stage-one moves. -/
def h1 : List (ℕ × ℕ) :=
  [(1, 44643), (2, 26482), (3, 12496), (4, 13211), (5, 8160), (6, 6821), (7, 3648), (8, 4989), (9, 1536),
    (10, 3488), (11, 1248), (12, 3395), (13, 1152), (14, 3672), (15, 1198), (16, 3215), (17, 2519),
    (18, 8244), (19, 3360), (20, 5626), (22, 10879), (23, 4071), (24, 1)]

/-- Histogram of the stage-two moves. -/
def h2 : List (ℕ × ℕ) := h1 ++ [(529, 4048), (552, 49208)]

/-- The histogram identity, digit by digit (kernel check). -/
def cntAll (k : ℕ) : ℕ :=
  2024 * (if k = 0 then 0 else cntH h1 k) + 2024 * (49208 * (if k = 552 then 1 else 0)) +
    2024 * (if k = 0 then 0 else cntH h2 k) + 2024 * 2024 * (if k = 1 then 1 else 0)

end IntMul.Kappa.R6.Cx.NetG

end

section
-- Source module: Solutions.R6CxNetFinal
/-!
# Track B: the round-six complex network as a `Prop8IfaceH`

`net = Z_u on every X ++ steps of CH ++ i^{wt u} Z_u on every Y ++ (X ↔ Y)`, on the roles
`Fin 207387136 ⊕ Fin 4193728`.

* `net_correct`: for every column type `κ`, the data block of its denotation is `C^{⊗}` on every
  data role (clean temporaries), from `prog_sim` with the initial labels `g0`, the final labels
  `gF_*` and the logical effect `ΛF_*`, as in `P8Lift.prog_correct`;
* `net_widths`: its child widths are `progWidths CH` (histogram `cxR6`, all `< 576`).

**`cxNetR6 : ∃ T, Nonempty (Prop8IfaceH 207387136 T 576 Jain.cxR6)`.**
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option maxRecDepth 20000
set_option synthInstance.maxSize 512

namespace IntMul.Kappa.R6.Cx.NetG

open Matrix Finset Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8 NetF2 NetT NetLoc
  NetSpec NetBT NetFast NetMask NetData NetEff NetSeg NetScal NetFr NetRaw Complex Butterfly P8Lift

/-! ## Role decoding -/

/-- Pair index of an `X`/`Y` role. -/
def xy (r : Rl) : ℕ := if rc r < NN then rc r else rc r - NN

/-- The correction vector of an `X`/`Y` role. -/
def ua (r : Rl) : Fin 576 → ZMod 2 := Uv (xy r / NV) (xy r % NV)

def uN (r : Rl) : Fin 576 → ℕ := fun i => 2 * (ua r i).val

lemma NN_lt : 2 * NN < Wn := by norm_num [NN, NV, Wn]

lemma rc_inl (w : Fin Wn) : rc (Sum.inl w : Rl) = w.val := rfl

lemma inl_eq_rW (w : Fin Wn) : (Sum.inl w : Rl) = rW w.val := by
  unfold rW; congr 1; exact Fin.ext (Nat.mod_eq_of_lt w.isLt).symm

lemma rW_rc {r : Rl} (h : rc r < Wn) : rW (rc r) = r := by
  rcases r with w | n
  · rw [rc_inl, ← inl_eq_rW]
  · exfalso; simp only [rc] at h; omega

/-! ## Phases and the role permutation -/

noncomputable def preR (r : Rl) : List (RStep Rl 576) :=
  if rc r < NN then [RStep.phase r 0 0 (uN r)] else []

noncomputable def postR (r : Rl) : List (RStep Rl 576) :=
  if NN ≤ rc r ∧ rc r < 2 * NN then [RStep.phase r 0 (NetComplexPhase.wt (ua r)) (uN r)] else []

variable {κ : Type} [Fintype κ] [DecidableEq κ]

variable (κ) in
noncomputable def preOpR (r : Rl) : Op (Fin 576 × κ) :=
  if rc r < NN then colT (ZuMat (ua r)) else 1

variable (κ) in
noncomputable def postOpR (r : Rl) : Op (Fin 576 × κ) :=
  if NN ≤ rc r ∧ rc r < 2 * NN then
    (I ^ NetComplexPhase.wt (ua r)) ^ Fintype.card κ • colT (ZuMat (ua r)) else 1

/-- `X(a,b) ↔ Y(a,b)`. -/
def σf (r : Rl) : Rl :=
  if rc r < NN then rW (rc r + NN) else if rc r < 2 * NN then rW (rc r - NN) else r

lemma σf_invol (r : Rl) : σf (σf r) = r := by
  unfold σf
  by_cases h1 : rc r < NN
  · have hc : rc (rW (rc r + NN)) = rc r + NN := rc_rW (by have := NN_lt; omega)
    rw [if_pos h1, hc, if_neg (by omega), if_pos (by omega), Nat.add_sub_cancel, rW_rc (by have := NN_lt; omega)]
  · rw [if_neg h1]
    by_cases h2 : rc r < 2 * NN
    · have hc : rc (rW (rc r - NN)) = rc r - NN := rc_rW (by have := NN_lt; omega)
      rw [if_pos h2, hc, if_pos (by omega), Nat.sub_add_cancel (by omega), rW_rc (by have := NN_lt; omega)]
    · rw [if_neg h2, if_neg h1, if_neg h2]

def σE : Equiv.Perm Rl := ⟨σf, σf, σf_invol, σf_invol⟩

/-! ## The network -/

/-- **The round-six complex network.** -/
noncomputable def net : List (HStep Rl 576) :=
  ((univ : Finset Rl).toList.flatMap preR).map HStep.ofR ++ progSteps CH ++
    ((univ : Finset Rl).toList.flatMap postR).map HStep.ofR ++ [HStep.perm σE]

/-! ## Correctness -/

end IntMul.Kappa.R6.Cx.NetG

namespace IntMul.Kappa.R6.Cx

open NetG NetFr

end IntMul.Kappa.R6.Cx

end

section
-- Source module: R6Pk.R6CxNetG
/-!
# The round-six complex network in the item-language gate class (`GClassH`)

`R6CxNetFinal.net` uses `mergedChunk` (an opaque `Classical.choose` of `merge_chunk`) for its frame
changes; its steps cannot be inspected. `netG` is the same network with every merged chunk replaced by
the explicit `chunkH` (row additions, one child, row additions) chosen from `merge_identity`: same
denotation, same child widths. Its only gates are the chunk gates `GOp.mat`:

* `z_d += (k/2) z_s` with `d ≠ s` (all local ops, `C1`, `C2`): `|k|` KFG atoms `(d, s, sign k, h = 1)`;
* `z_X += -2 z_X` (`C3`): the `±1` diagonal `-1` at `X`.

**`cxNetR6G : ∃ T (J : Prop8IfaceH 207387136 T 576 Jain.cxR6) A, GClassH J A`.**
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false
set_option maxRecDepth 20000

namespace IntMul.Kappa.R6.Cx.NetG

open Matrix Finset Module NetLabels NetComplexOrtho NetComplexLabels NetComplexP8 NetF2 NetT NetLoc
  NetSpec NetBT NetFast NetMask NetData NetEff NetSeg NetScal NetFr NetRaw Complex Butterfly P8Lift

/-! ## Local ops act on two distinct wires -/

section LocalDist

variable (d : Dat)

/-- Every op has distinct target and source. -/
def LD (l : List (ℕ × ℕ × ℤ)) : Prop := ∀ o ∈ l, o.1 ≠ o.2.1

/-- Specs whose ops are all `LD`. -/
def LDs (ss : List Spec) : Prop := ∀ s ∈ ss, LD s.ops

end LocalDist

/-! ## Explicit merged chunks -/

/-- The merge condition of a kernel list. -/
def MC (L : List (ℤ × (Fin 576 → ZMod 2))) : Prop :=
  L ≠ [] ∧ (∀ p ∈ L, p.1 = 1 ∨ p.1 = -1) ∧ LIndep L

lemma merge_ex (L : List (ℤ × (Fin 576 → ZMod 2))) (hL : MC L) :
    ∃ t : List (Fin 576 × Fin 576) × Finset (Fin 576) × Finset (Fin 576), t.2.1.card = L.length ∧
      ∀ (κ : Type) [Fintype κ] [DecidableEq κ],
        (_root_.IntMul.Kappa.R6.Cx.PL t.1.reverse * signedOp (chEx (κ := κ)) t.2.1 t.2.2 *
          _root_.IntMul.Kappa.R6.Cx.PL t.1 : Op (Fin 576 × κ)) =
          colT (L.map fun p => Tk p.1 p.2).prod := by
  obtain ⟨js, S, neg, h1, -, h3⟩ := merge_identity (fun k : Fin L.length => (L.get k).1)
    (fun k => hL.2.1 _ (List.get_mem L k)) _ hL.2.2
  exact ⟨(js, S, neg), h1, fun κ _ _ => by rw [h3 κ, prod_finRange_get]⟩

open Classical in
/-- The explicit merged chunk: `chunkH` with the data of `merge_identity`. -/
noncomputable def mcG (w : Rl) (L : List (ℤ × (Fin 576 → ZMod 2))) : List (HStep Rl 576) :=
  if hL : MC L then
    chunkH w (Classical.choose (merge_ex L hL)).1 (Classical.choose (merge_ex L hL)).2.1
      (Classical.choose (merge_ex L hL)).2.2
  else []

/-! ## The network with explicit merged chunks -/

/-- Steps of a chunk, with explicit merged chunks. -/
noncomputable def stepsG (C : GChunk Rl 576) : List (HStep Rl 576) :=
  C.mv.flatMap (fun p => mcG p.1 (kersM C.V p.2)) ++ C.ops.map fun o => HStep.gate o.mat

noncomputable def progStepsG (cs : List (GChunk Rl 576)) : List (HStep Rl 576) := cs.flatMap stepsG

/-- **The network with explicit merged chunks.** -/
noncomputable def netG : List (HStep Rl 576) :=
  ((univ : Finset Rl).toList.flatMap preR).map HStep.ofR ++ progStepsG CH ++
    ((univ : Finset Rl).toList.flatMap postR).map HStep.ofR ++ [HStep.perm σE]

/-! ## The gates of `netG` -/

/-! ## The ops of `CH` -/

/-- An op of `CH`: `z_d += (k/2) z_s` with `d ≠ s`, or `z_X += -2 z_X`. -/
def OpK (o : GOp Rl) : Prop := (o.dst ≠ o.src ∧ ∃ k : ℤ, o.c = (k : ℂ) / 2) ∨ (o.dst = o.src ∧ o.c = -2)

/-! ## Ops as KFG atoms -/

open IntMul.Kappa.R6.IL3H

/-- The atom of `z_d += (sign k / 2) z_s`. -/
def atK (d s : Rl) (k : ℤ) : NLogN.KFG.Atom := ⟨rc d, rc s, (k.sign, 0), 1⟩

/-- The gate-class predicate of one op with atom bound `A`. -/
def GP (o : GOp Rl) (A : ℕ) : Prop :=
  (∃ as : List NLogN.KFG.Atom, as.length ≤ A ∧ (∀ a ∈ as, a.Ok (Wn + Tn) ∧ a.h ≤ 1) ∧ NLogN.KFG.NoTS as ∧
      o.mat = (NLogN.KFG.gateMat (Wn + Tn) as).submatrix (roleEqv Wn Tn) (roleEqv Wn Tn)) ∨
    (∃ U : Finset Rl, o.mat = Matrix.diagonal fun w => if w ∈ U then -1 else 1)

end IntMul.Kappa.R6.Cx.NetG

namespace IntMul.Kappa.R6.Cx

open NetG NetFr IL3H

end IntMul.Kappa.R6.Cx

-- #print axioms IntMul.Kappa.R6.Cx.cxNetR6G

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/R6CxNetChk2_0.lean, Solutions/R6CxNetChk2_1.lean, Solutions/R6CxNetChk2_2.lean, Solutions/R6CxNetChk2_3.lean, Solutions/R6CxNetChk2_4.lean, Solutions/R6CxNetChk2_5.lean, Solutions/R6CxNetChk2_6.lean, Solutions/R6CxNetChk2_7.lean, Solutions/R6CxNetChk2_8.lean, Solutions/R6CxNetChk2_9.lean, Solutions/R6CxNetChk2_10.lean, Solutions/R6CxNetChk2_11.lean, Solutions/R6CxNetChk2_12.lean, Solutions/R6CxNetChk2_13.lean, Solutions/R6CxNetOps.lean, Solutions/R6CxNetSeg.lean, Solutions/R6CxNetChkI.lean, Solutions/R6CxNetInvoc.lean, Solutions/R6CxNetGlobL.lean, Solutions/R6CxNetGlobS.lean, Solutions/R6CxNetHist.lean, Solutions/R6CxNetFinal.lean, Solutions/R6CxNetG.lean.

View graph