Round-six κ development, definitions part 4

-- 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
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_Kappa_K_Defs1
import Definitions.Def_IntMul_Kappa_K_Defs2

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.AModel
/-!
# Array model: mixed-radix arrays, pull maps, and linear address maps via Bruhat factors

Arrays are lists in row-major lexicographic order over fields (first field most significant).
All denotations are plain `List` functions.
-/

namespace AModel

open Matrix

/-! ## 1. Mixed-radix basics -/

/-! ## 2. Pull maps -/

section Pull
variable {α : Type*}

@[simp] lemma length_pull (sh sh' : Shape) (g : List ℕ → List ℕ) (d : α) (xs : List α) :
    (pull sh sh' g d xs).length = vol sh' := by simp [pull]

end Pull

/-! ## 3. Active fields -/

variable {sh : Shape} {n Q : ℕ} (Λ : Layout sh n Q)

namespace Layout

end Layout

/-! ## 4. Controlled shift -/

/-! ## 5. Field transposition -/

/-! ## Primitive steps and their composition -/

namespace Step

variable [NeZero Q]

end Step

/-! ## 6. Linear address maps through Bruhat factors -/

end AModel

end

section
-- Source module: Solutions.AModelRuns
/-!
# Array model, Stage 2: runs of pivots as single interchanges of merged fields

Builds on `Solutions/AModel.lean` (whose definitions are unchanged).

* §1 Reshape (`mergeShape`, `mergeAddr`, `splitAddr`): merging adjacent fields is free —
  `pull_merge`, `pull_split`, general `pull_reshape`.
* §2 Block swap (`blockSwap`): it is the composition of the single position swaps
  (`chain_runPairs`), and after merging both runs it is one swap of two merged fields
  (`merge2_blockSwap`, `pull_blockSwap`).
* §3 A run of `r` consecutive pivots on contiguous active fields acts on arrays as that block swap
  (`runArr_pivotRun`), hence as one merged-field interchange (`runArr_pivotRun_merged`).
* §4 A pivot list splits into `numRuns` maximal runs (`groupRuns`, `flatMap_groupRuns`), and
  `runArr` over its swaps is the composition of one merged-field swap per run
  (`runArr_swapSteps_runs`).
-/

namespace AModel

/-! ## 1. Reshape -/

/-! ## 2. Block swaps -/

section BlockSwap

/-- Composition of position swaps along a list of pairs (first pair applied last, as for
`invChain`). -/
def chain (L : List (ℕ × ℕ)) (a : List ℕ) : List ℕ := L.foldr (fun p b => swapPos p.1 p.2 b) a

/-- The `r` aligned position pairs `(i+k, j+k)`. -/
def runPairs (i j r : ℕ) : List (ℕ × ℕ) := (List.range r).map fun k => (i + k, j + k)

/-! ### Segments of a block-swapped address -/

/-! ### Merging both runs -/

end BlockSwap

/-! ## 3. A run of consecutive pivots is one merged-field interchange -/

section PivotRun

variable {sh : Shape} {n Q : ℕ} (Λ : Layout sh n Q)

/-- The list positions of a list of pivots. -/
def posPairs (ps : List (Fin n × Fin n)) : List (ℕ × ℕ) :=
  ps.map fun p => ((Λ.pos p.1 : ℕ), (Λ.pos p.2 : ℕ))

variable [NeZero Q]

end PivotRun

/-! ## 4. Counting runs -/

end AModel

end

section
-- Source module: Solutions.R6BitNet
/-!
# Round six, bit side: interchange networks with general frames (`QHNet`)

The array-model notion of network needed by S. Jain's round six (ARCH.md §2 R1, design
decision 2). Compared with `AModel.Circuit` (OpenAI Prop. 11):

* there is no `unit` restriction and no shear structure: every **edge** is an explicit frame
  change on one stream, given by Bruhat data `E₁ · σ · E₂` with rational `2m × 2m` lower
  triangular factors (reduced mod the field size `N`) and a permutation `σ` that is a product of
  field transpositions `H_{i+k} ↔ D_{j+k}`, grouped into **runs** `(i, j, r)` (`k < r`);
  each run is executed as **one** recursive child interchange of width `r` fields (so child widths
  are arbitrary `0 < r < m`, as in the partial-swap Bruhat run decomposition);
* **gates** are arbitrary pointwise linear maps on a set of wires (copies, XORs, the copy
  correction, the scalar word);
* wires are `Fin W ⊕ Fin T`: `W` roles (one per row residue of the row split) and `T`
  temporaries (initialised to `0`, discarded at the end);
* correctness (`QHNet.IdealOK N`) is stated for the **ideal** execution, in which every edge runs
  its Bruhat steps exactly (`runArr`), on streams of *any* shape with *any* layout of `2m` active
  fields of size `N`: role `ρ w` ends with the chunk interchange `amap swapMat` of the input
  stream `w`. This is the hypothesis later workers prove for the real network (e.g. from
  `AModel.linear_via_bruhat_array` and a frame-label invariant);
* `hist`: the child-width histogram `[(r, 1)]`, one entry per run of every edge.
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Bit

open AModel AModelFac Matrix

/-- Rational `2m × 2m` matrices (the Bruhat factors of a frame change). -/
abbrev QMat2 (m : ℕ) := Matrix (Fin (m + m)) (Fin (m + m)) ℚ

/-- Reduction mod `N` of a rational matrix (`redQ`, total). -/
def redM {m : ℕ} (N : ℕ) (E : QMat2 m) : Matrix (Fin (m + m)) (Fin (m + m)) (ZMod N) :=
  E.map (redQ N)

/-- Frame-change data of one edge: the frame change is `E₁ · σ · E₂` where `σ` is the product of
the transpositions `H_{i+k} ↔ D_{j+k}` (`k < r`) over the runs `(i, j, r) ∈ runs`. -/
structure Edge (m : ℕ) where
  E₁ : QMat2 m
  runs : List (ℕ × ℕ × ℕ)
  E₂ : QMat2 m

/-- The pivots `(H_{i+k}, D_{j+k})`, `k < r`, of a run (out-of-range ones dropped). -/
def runPiv (m : ℕ) (ρ : ℕ × ℕ × ℕ) : List (Fin (m + m) × Fin (m + m)) :=
  (List.range ρ.2.2).filterMap fun k =>
    if h : ρ.1 + k < m ∧ ρ.2.1 + k < m then
      some (Fin.castAdd m ⟨ρ.1 + k, h.1⟩, Fin.natAdd m ⟨ρ.2.1 + k, h.2⟩)
    else none

/-- The Bruhat steps of an edge at field size `N`: shifts for `E₂`, the transpositions, shifts
for `E₁` (`AModel.bruhatSteps`). -/
def Edge.steps {m : ℕ} (e : Edge m) (N : ℕ) : List (Step (m + m) N) :=
  bruhatSteps (redM N e.E₁) (e.runs.flatMap (runPiv m)) (redM N e.E₂)

/-- A run is valid: nonempty, narrower than `m`, and inside both chunks. -/
def RunOK (m : ℕ) (ρ : ℕ × ℕ × ℕ) : Prop :=
  0 < ρ.2.2 ∧ ρ.2.2 < m ∧ ρ.1 + ρ.2.2 ≤ m ∧ ρ.2.1 + ρ.2.2 ≤ m

/-- One instruction of the network. -/
inductive Instr (Wr R : Type*) (m : ℕ) where
  /-- Pointwise linear gate on the wires of `S`: `x_w ← Σ_{w' ∈ S} g w w' x_{w'}`. -/
  | gate (g : Matrix Wr Wr R) (S : Finset Wr)
  /-- Frame change `e` on wire `w`. -/
  | edge (w : Wr) (e : Edge m)

namespace Instr

variable {Wr R : Type*} {m : ℕ}

/-- The edge of an instruction, if any. -/
def edgeOf : Instr Wr R m → Option (Edge m)
  | gate _ _ => none
  | edge _ e => some e

/-- The number of touched wires of a gate (`0` for an edge). -/
def gateWork : Instr Wr R m → ℕ
  | gate _ S => S.card
  | edge _ _ => 0

end Instr

/-- **Round-six bit interchange network.** `W` roles, `T` temporaries, frames on `2m` fields.
`ρ`: output role `ρ w` carries input role `w` (the merge undoes `ρ`). -/
structure QHNet (R : Type*) (W T m : ℕ) where
  prog : List (Instr (Fin W ⊕ Fin T) R m)
  ρ : Fin W → Fin W

/-! ## Execution of a network on streams (generic in the edge implementation) -/

section Run

variable {Wr R : Type*} [Fintype Wr] [DecidableEq Wr] [CommRing R] {m : ℕ}

/-- A pointwise gate on streams of length `n`. -/
def gateApply (n : ℕ) (g : Matrix Wr Wr R) (S : Finset Wr) (st : Wr → List R) : Wr → List R :=
  fun w => if w ∈ S then List.ofFn (fun i : Fin n => ∑ w' ∈ S, g w w' * (st w').getD i 0)
    else st w

/-- One instruction, with edges executed by `impl`. -/
def instrRun (n : ℕ) (impl : Edge m → List R → List R) (st : Wr → List R) :
    Instr Wr R m → Wr → List R
  | .gate g S => gateApply n g S st
  | .edge w e => Function.update st w (impl e (st w))

/-- Run a program, with edges executed by `impl`. -/
def netRunH (n : ℕ) (impl : Edge m → List R → List R) (prog : List (Instr Wr R m))
    (st : Wr → List R) : Wr → List R :=
  prog.foldl (instrRun n impl) st

/-- The edges of a program. -/
def progEdges (prog : List (Instr Wr R m)) : List (Edge m) := prog.filterMap Instr.edgeOf

end Run

/-! ## The network data: edges, histogram, hypotheses -/

namespace QHNet

variable {R : Type*} [CommRing R] {W T m : ℕ}

/-- All edges of the network. -/
def edges (C : QHNet R W T m) : List (Edge m) := progEdges C.prog

/-- All child widths (one per run of every edge). -/
def widths (C : QHNet R W T m) : List ℕ := C.edges.flatMap fun e => e.runs.map fun ρ => ρ.2.2

/-- The child-width histogram `[(w, n_w)]` (here with `n_w = 1` per child). -/
def hist (C : QHNet R W T m) : List (ℕ × ℕ) := C.widths.map fun w => (w, 1)

/-- Number of edges. -/
def numEdges (C : QHNet R W T m) : ℕ := C.edges.length

/-- Total gate work: the number of (gate, touched wire) pairs. -/
def gateWork (C : QHNet R W T m) : ℕ := (C.prog.map Instr.gateWork).sum

/-- Initial wires: roles from the input streams, temporaries zero. -/
def initH (n : ℕ) (ins : Fin W → List R) : Fin W ⊕ Fin T → List R
  | .inl w => ins w
  | .inr _ => List.replicate n 0

/-- **Ideal execution** on streams of shape `sh` with layout `Λ` of the `2m` active fields
(field size `N`): every edge runs its Bruhat steps exactly. The value is the final content of
role `w`. -/
def idealOut (C : QHNet R W T m) (N : ℕ) {sh : Shape} (Λ : Layout sh (m + m) N)
    (ins : Fin W → List R) (w : Fin W) : List R :=
  netRunH (vol sh) (fun e => runArr Λ 0 (e.steps N)) C.prog (initH (vol sh) ins) (.inl w)

/-- All runs are valid (`0 < r < m`, inside the chunks). -/
def RunsOK (C : QHNet R W T m) : Prop := ∀ e ∈ C.edges, ∀ ρ ∈ e.runs, RunOK m ρ

/-- **Correctness of the ideal network at field size `N`.** For every stream shape and layout
of the `2m` active fields, role `ρ w` ends with the chunk interchange `(H, D) ↦ (D, H)` of input
stream `w`. -/
def IdealOK (C : QHNet R W T m) (N : ℕ) : Prop :=
  ∀ (sh : Shape) (Λ : Layout sh (m + m) N) (ins : Fin W → List R),
    (∀ w, (ins w).length = vol sh) →
      ∀ w, C.idealOut N Λ ins (C.ρ w) = pull sh sh (amap Λ swapMat) 0 (ins w)

/-- The hypotheses of the generalized Prop. 11 at field size `N`. -/
structure OK (C : QHNet R W T m) (N : ℕ) : Prop where
  runs : C.RunsOK
  ideal : C.IdealOK N

end QHNet

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6BitLevel
/-!
# Round six, bit side: one level of the generalized Prop. 11

On the shape `P :: (W L') :: hdShape A B Cs m N` (two chunks of `m` fields of size `N`):
split the rows into `W` role streams (plus `T` zero temporaries), run the network with every
edge implemented by its shifts and **one child call per run** (`realEdge`), merge back undoing
`ρ`. With correct children and `C.OK N` this is the chunk interchange (`levelH_correct`).

1. `realEdge_eq`: with children equal to the exact run transpositions, the implemented edge is
   the ideal one (`runArr` of the Bruhat steps).
2. `runArr_runPiv`: on the stream layout, the transpositions of a run `(i, j, r)` are the block
   swap of the field runs `H_i … H_{i+r-1}` and `D_j … D_{j+r-1}`.
3. `levelH_correct`.
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Bit

open AModel AModelFac Matrix

variable {R : Type*} [CommRing R] {m : ℕ}

/-! ## 1. Implemented edges -/

section Edge

variable {sh : Shape} {N : ℕ} (Λ : Layout sh (m + m) N)

/-- **Implemented edge**: shifts for `E₂` (passes), one child call per run, shifts for `E₁`. -/
def realEdge (child : ℕ × ℕ × ℕ → List R → List R) (e : Edge m) (ys : List R) : List R :=
  runArr Λ 0 (shiftSteps (redM N e.E₁))
    (e.runs.foldl (fun ys ρ => child ρ ys) (runArr Λ 0 (shiftSteps (redM N e.E₂)) ys))

end Edge

/-! ## 2. Runs on the stream layout are block swaps of field runs -/

/-! ## 3. One level -/

section Level

variable {W T : ℕ} [NeZero W] (C : QHNet R W T m) (N P L' : ℕ) (A B Cs : Shape)

/-- **One level of the generalized Prop. 11** on `P :: (W L') :: hdShape A B Cs m N`: row split
into `W` role streams and `T` zero temporaries; the network, every edge implemented by
`realEdge` with the run interchanges delegated to `child`; merge undoing `ρ`. -/
def levelH (child : ℕ × ℕ × ℕ → List R → List R) (xs : List R) : List R :=
  rowMerge P W L' (hdShape A B Cs m N) 0 (fun w =>
    netRunH (vol (P :: L' :: hdShape A B Cs m N))
      (realEdge ((hdLayout A B Cs m N).cons2 P L') child) C.prog
      (QHNet.initH (T := T) (vol (P :: L' :: hdShape A B Cs m N))
        (fun w' => rowSplit P W L' (hdShape A B Cs m N) w' 0 xs)) (.inl (C.ρ w)))

/-- The child hypothesis: for every valid run `(i, j, r)`, `child` interchanges the field runs
`H_i … H_{i+r-1}` and `D_j … D_{j+r-1}` of a stream. -/
def ChildOKH (child : ℕ × ℕ × ℕ → List R → List R) : Prop :=
  ∀ ρ, RunOK m ρ → ∀ ys : List R, ys.length = vol (P :: L' :: hdShape A B Cs m N) →
    child ρ ys = pull (P :: L' :: hdShape A B Cs m N) (P :: L' :: hdShape A B Cs m N)
      (blockSwap (A.length + 2 + ρ.1) (A.length + B.length + m + 2 + ρ.2.1) ρ.2.2) 0 ys

variable [NeZero N]

end Level

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6BitProg
/-!
# Round six, bit side: the recursive interchange program for every width `e`

`progH C q e P L A B Cs` interchanges the two chunks of `e` radix-`q` digits of
`P :: L :: hdShape A B Cs e q`, for **every** `e` (not only `e = m^k`):

* `e < m`: `e` single digit swaps (`tailSwaps`);
* `e = m f + r`, `f ≥ 1`: one level (`levelH`) on the first `m f` digits of each chunk, viewed as
  `m` fields of size `q ^ f`, every run `(i, j, r')` of every edge being a recursive call of width
  `r' f < e`; then the `r` leftover digits by single digit swaps.

`progH_correct`: the denotation is the block swap of the two digit runs, when `C.OK (q ^ f)` for
all `f` and `W ^ depH m e ∣ L` (`depH` = recursion depth).
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Bit

open AModel AModelFac Matrix

variable {R : Type*} [CommRing R]

/-! ## Digit swaps -/

section Tail

/-- Swap the digit runs `[c, c+r)` and `[c', c'+r)` by `r` single digit swaps (one pass each). -/
def tailSwaps (sh : Shape) (c c' r : ℕ) (xs : List R) : List R :=
  (runPairs c c' r).foldl (fun ys pr => pull sh sh (swapPos pr.1 pr.2) 0 ys) xs

end Tail

/-! ## Digit shapes -/

/-! ## Recursion depth -/

section Depth

lemma depH_dec {m e : ℕ} (h : m ≤ e ∧ 2 ≤ m) : (m - 1) * (e / m) < e := by
  have h1 : 1 ≤ e / m := (Nat.le_div_iff_mul_le (by omega)).2 (by omega)
  have h2 : e / m * m ≤ e := Nat.div_mul_le_self e m
  have h3 : (m - 1) * (e / m) + e / m = m * (e / m) := by
    rw [← Nat.succ_mul]; congr 1; omega
  nlinarith

/-- Recursion depth of `progH`: `0` below `m`, else one more than at `(m - 1) ⌊e / m⌋`
(the widest possible child). -/
def depH (m : ℕ) (e : ℕ) : ℕ :=
  if h : m ≤ e ∧ 2 ≤ m then depH m ((m - 1) * (e / m)) + 1 else 0
termination_by e
decreasing_by exact depH_dec h

end Depth

/-! ## The program -/

section Prog

variable {W T m : ℕ} [NeZero W]

/-- **The generalized interchange program.** `progH C q e P L A B Cs` interchanges the two chunks
of `e` radix-`q` digits of `P :: L :: hdShape A B Cs e q`. For `e ≥ m`, with `f = ⌊e/m⌋`,
`r = e mod m`: one level (`levelH`, field size `q ^ f`, `L / W` stream rows) on the first `m f`
digits of each chunk, the run `(i, j, r')` of an edge being the recursive call of width `r' f`
on the stream; then the `r` leftover digit pairs are swapped one by one. For `e < m`: `e` digit
swaps. -/
def progH (C : QHNet R W T m) (q : ℕ) (e P L : ℕ) (A B Cs : Shape) (xs : List R) : List R :=
  if m ≤ e then
    tailSwaps (P :: L :: hdShape A B Cs e q) (A.length + 2 + m * (e / m))
      (A.length + B.length + e + 2 + m * (e / m)) (e % m)
      (levelH C (q ^ (e / m)) P (L / W) A (List.replicate (e % m) q ++ B)
        (List.replicate (e % m) q ++ Cs)
        (fun ρ ys => if _hρ : ρ.2.2 * (e / m) < e then
            progH C q (ρ.2.2 * (e / m)) P (L / W) (A ++ List.replicate ρ.1 (q ^ (e / m)))
              (List.replicate (m - ρ.1 - ρ.2.2) (q ^ (e / m)) ++
                ((List.replicate (e % m) q ++ B) ++ List.replicate ρ.2.1 (q ^ (e / m))))
              (List.replicate (m - ρ.2.1 - ρ.2.2) (q ^ (e / m)) ++
                (List.replicate (e % m) q ++ Cs)) ys
          else ys) xs)
  else tailSwaps (P :: L :: hdShape A B Cs e q) (A.length + 2) (A.length + B.length + e + 2) e xs
termination_by e

end Prog

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6BitCost
/-!
# Round six, bit side: cost of `progH` and the generalized Prop. 11

`costH C e V`: the structural cost of `progH C q e …` on an array of volume `V`, following the
program: `e < m`: `e` digit-swap passes; `e = m f + r`: `r` digit-swap passes, the row split and
merge (`2V`), `T` zero temporaries (`T V / W`), each gate one pass per touched wire (`V / W`),
each edge `4m` shift passes (`V / W` each) plus its run children, each a recursive call of width
`r' f` on a stream of volume `V / W`.

* `costH_lin`: `costH e V = V · costH e 1`.
* `cH_rec`: `c(e) = (e mod m) + K₀ + (1/W) Σ_{children} c(w ⌊e/m⌋)` (`c = costH · 1`).
* `costH_bound`: with `histMoment C.hist m τ < W`, `costH e V ≤ K V e^τ` for all `e` (via the
  monotone majorant of `c` and `R6.MomentRec.moment_recurrence_bound`).
* `prop11H`: denotation and cost together.
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Bit

open AModel AModelFac Matrix

variable {R : Type*} [CommRing R] {W T m : ℕ} [NeZero W]

/-- Cost of one instruction on streams of volume `v`, children costed by `child`. -/
noncomputable def instrCost {Wr : Type*} (child : ℕ × ℕ × ℕ → ℝ → ℝ) (v : ℝ) :
    Instr Wr R m → ℝ
  | .gate _ S => (S.card : ℝ) * v
  | .edge _ e => (2 * (m + m) : ℝ) * v + (e.runs.map fun ρ => child ρ v).sum

/-- **Structural cost of `progH`** at width `e` on volume `V`. -/
noncomputable def costH (C : QHNet R W T m) (e : ℕ) (V : ℝ) : ℝ :=
  if m ≤ e then
    ((e % m : ℕ) : ℝ) * V + (2 * V + (T : ℝ) * (V / W) +
      (C.prog.map (instrCost (fun ρ v => if ρ.2.2 * (e / m) < e then costH C (ρ.2.2 * (e / m)) v
        else 0) (V / W))).sum)
  else (e : ℝ) * V
termination_by e

/-- Per-unit-volume cost. -/
noncomputable def cH (C : QHNet R W T m) (e : ℕ) : ℝ := costH C e 1

/-- The linear constant `K₀ = 2 + (T + gate work + 4m · #edges) / W`. -/
noncomputable def K0 (C : QHNet R W T m) : ℝ :=
  2 + ((T : ℝ) + C.gateWork + 2 * (m + m) * C.numEdges) / W

/-- The monotone majorant `ĉ(x) = max_{y ≤ x} c(y)`. -/
noncomputable def cHat (C : QHNet R W T m) (x : ℕ) : ℝ :=
  (Finset.range (x + 1)).sup' ⟨0, by simp⟩ (cH C)

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6BitLab
/-!
# Round six, bit side: `IdealOK` from frame labels and a scalar routing identity

A sufficient condition for `QHNet.IdealOK N` in the style of OpenAI's network theorem
(`AModel.network_realizes`), but with **multiplicative** (non-commuting) frames:

* every edge `e` has lower triangular rational Bruhat factors with unit diagonals mod `N`
  (`EdgesOK`); its frame matrix is `X_e = E₁ · σ_e · E₂` mod `N` (`edgeMat`);
* labels (frames) are tracked along the program: initially `1` on every wire, an edge on `w`
  multiplies the label of `w` on the left by `X_e`; every gate touches wires with equal labels,
  and the final label of every role `ρ w` is `swapMat` (`LabOK`);
* the scalar circuit (gates only; temporaries start at `0`) routes role `w` to role `ρ w`
  (`ScalarOK`).

Then `C.IdealOK N` (`idealOK_of_labels`). The physical content of each wire is the array
permutation `Φ(F) = pull (amap F⁻¹)` of its logical content (`frameArr`), `Φ` is multiplicative
(`frameArr_mul`), commutes with pointwise gates (`frameArr_gate`), and the ideal edge is
`Φ(X_e)` (`runArr_steps_eq`, from `AModel.linear_via_bruhat_array`).
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Bit

open AModel AModelFac Matrix

variable {R : Type*} [CommRing R] {m : ℕ}

/-! ## Frames as array permutations -/

section Frame

variable {sh : Shape} {N : ℕ} [NeZero N] (Λ : Layout sh (m + m) N)

/-- The array permutation realizing the address map of `F` (pull by `amap F⁻¹`). -/
noncomputable def frameArr (F : Matrix (Fin (m + m)) (Fin (m + m)) (ZMod N)) (xs : List R) : List R :=
  pull sh sh (amap Λ F⁻¹) 0 xs

@[simp] lemma length_frameArr (F : Matrix (Fin (m + m)) (Fin (m + m)) (ZMod N)) (xs : List R) :
    (frameArr Λ F xs).length = vol sh := by simp [frameArr]

/-- The frame matrix of an edge at field size `N`. -/
noncomputable def edgeMat (N : ℕ) (e : Edge m) : Matrix (Fin (m + m)) (Fin (m + m)) (ZMod N) :=
  redM N e.E₁ * ((e.runs.flatMap (runPiv m)).map fun p => Equiv.swap p.1 p.2).prod.permMatrix
    (ZMod N) * redM N e.E₂

/-- The Bruhat data of an edge is admissible mod `N`. -/
def EdgeOK (N : ℕ) (e : Edge m) : Prop :=
  (∀ i j, i < j → e.E₁ i j = 0) ∧ (∀ i j, i < j → e.E₂ i j = 0) ∧
    (∀ i, IsUnit (redQ N (e.E₁ i i))) ∧ (∀ i, IsUnit (redQ N (e.E₂ i i)))

end Frame

/-! ## Labels and the scalar circuit -/

section Labels

variable {Wr : Type*} [Fintype Wr] [DecidableEq Wr] (N : ℕ)

/-- Label update by one instruction. -/
noncomputable def labStepH (F : Wr → Matrix (Fin (m + m)) (Fin (m + m)) (ZMod N)) :
    Instr Wr R m → Wr → Matrix (Fin (m + m)) (Fin (m + m)) (ZMod N)
  | .gate _ _ => F
  | .edge w e => Function.update F w (edgeMat N e * F w)

/-- Every gate touches wires with equal labels. -/
def LabGates : List (Instr Wr R m) → (Wr → Matrix (Fin (m + m)) (Fin (m + m)) (ZMod N)) → Prop
  | [], _ => True
  | i :: l, F => (match i with
      | .gate _ S => ∀ w ∈ S, ∀ w' ∈ S, F w = F w'
      | .edge _ _ => True) ∧ LabGates l (labStepH N F i)

/-- Scalar action of a gate. -/
def gateVec (g : Matrix Wr Wr R) (S : Finset Wr) (v : Wr → R) : Wr → R :=
  fun w => if w ∈ S then ∑ w' ∈ S, g w w' * v w' else v w

/-- The scalar circuit (edges act trivially on logical values). -/
def scalarStepH (v : Wr → R) : Instr Wr R m → Wr → R
  | .gate g S => gateVec g S v
  | .edge _ _ => v

end Labels

namespace QHNet

variable {W T : ℕ}

/-- Every edge has admissible Bruhat data mod `N`. -/
def EdgesOK (C : QHNet R W T m) (N : ℕ) : Prop := ∀ e ∈ C.edges, EdgeOK N e

/-- Labels: gates touch equal labels, and every role `ρ w` ends with label `swapMat`. -/
def LabOK (C : QHNet R W T m) (N : ℕ) : Prop :=
  LabGates N C.prog (fun _ => 1) ∧
    ∀ w, C.prog.foldl (labStepH N) (fun _ => 1) (.inl (C.ρ w)) = swapMat

/-- The scalar circuit (temporaries start at `0`) routes role `w` to role `ρ w`. -/
def ScalarOK (C : QHNet R W T m) : Prop :=
  ∀ (v : Fin W → R) (w : Fin W),
    C.prog.foldl scalarStepH (Sum.elim v fun _ => 0) (.inl (C.ρ w)) = v w

end QHNet

/-! ## The invariant and `idealOK_of_labels` -/

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6BitEx
/-!
# Round six, bit side: a sanity instance of `QHNet.OK`

`exNet`: `m = 2`, one role, no temporaries, a single edge with trivial Bruhat factors and the
two runs `H₀ ↔ D₀`, `H₁ ↔ D₁` (widths `1 < m`). It satisfies `QHNet.OK N` at every field size
(`exNet_OK`), via `idealOK_of_labels`. This checks that the hypotheses of `prop11H` are
consistent (non-vacuous); of course this network has no saving (`histMoment = 2 (1/2)^τ ≥ 1`).
-/

namespace IntMul.Kappa.R6.Bit

open AModel AModelFac Matrix

variable {R : Type*} [CommRing R]

/-- The edge: `E₁ = E₂ = 1`, runs `(0, 0, 1)` and `(1, 1, 1)`. -/
def exEdge : Edge 2 := ⟨1, [(0, 0, 1), (1, 1, 1)], 1⟩

/-- The example network. -/
def exNet : QHNet R 1 0 2 := ⟨[.edge (.inl 0) exEdge], id⟩

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6BitNBRunsLib
/-! Verbatim copy of `Solutions/Runs.lean` (OpenAI layer) inside a namespace, so that it can be
imported together with other root-level `solution` theorems. -/

namespace IntMul.Kappa.R6.Bit.RunsLib

section Sec_PSwap

namespace PSwapAux
open Submodule Module

variable {K : Type*} [Field K]

def PD (m X Y : ℕ) : Fin m ⊕ {r : Fin m // r.val < X} → Prop :=
  Sum.elim (fun r => Y ≤ r.val) (fun _ => False)

instance (m X Y : ℕ) : DecidablePred (PD m X Y) := fun i => by
  cases i <;> (simp only [PD, Sum.elim_inl, Sum.elim_inr]; infer_instance)

def QD (m X : ℕ) : Fin m → Prop := fun j => j.val < X

instance (m X : ℕ) : DecidablePred (QD m X) := fun j => by
  simp only [QD]; infer_instance

end PSwapAux

end Sec_PSwap

section Sec_Bruhat

open Matrix Finset

namespace BruhatAux

variable {K : Type*} [Field K] {m : ℕ}

end BruhatAux

end Sec_Bruhat

section Sec_BruhatRank

open Matrix Finset

namespace BruhatRankAux

variable {K : Type*} [Field K] {m : ℕ}

end BruhatRankAux

end Sec_BruhatRank

section Sec_PPUniq

open Finset

namespace PPUniqAux

variable {n : ℕ} {K : Type*} [One K] [DecidableEq K]

/-- Number of ones of `P` in rows `< X` and columns `≥ Y`. -/
def cnt (P : Matrix (Fin n) (Fin n) K) (X Y : ℕ) : ℕ :=
  (univ.filter fun x : Fin n × Fin n => x.1.val < X ∧ Y ≤ x.2.val ∧ P x.1 x.2 = 1).card

end PPUniqAux

end Sec_PPUniq

section Sec_Runs

open Matrix Finset

namespace RunsAux

variable {K : Type*} [Field K]

end RunsAux

end Sec_Runs

end IntMul.Kappa.R6.Bit.RunsLib

end

section
-- Source module: Solutions.R6BitNBPiv
/-!
# Round six, bit network: pivots from ranks, and edges from pivots

* `rk q X Y`: rank of the rows `< X`, columns `≥ Y` of `q`; `IsPiv q i j`: the
  inclusion–exclusion of `rk` at `(i, j)` is one.
* `isPiv_iff`: for a Bruhat factorization `E₁ P E₂`, `IsPiv` is exactly `P i j = 1`.
* `edge_of_pivs`: for an idempotent `q` over `ℚ` and runs whose positions are pivots of `q`, there
  is an edge (lower triangular `E₁, E₂`, nonzero diagonals) with runs `rs ++ rs'`, `rs'` singletons,
  `|rs| + |rs'| = rank q`, and frame `E₁ σ E₂ = pswQ q` (the partial swap of `q`).
-/

namespace IntMul.Kappa.R6.Bit.NB

open Matrix Finset

section Piv

variable {K : Type*} [Field K] {n a b : ℕ}

/-- Rank of the rows `< X` and columns `≥ Y`. -/
noncomputable def rk (q : Matrix (Fin a) (Fin b) K) (X Y : ℕ) : ℕ :=
  (q.submatrix (fun r : {r : Fin a // r.val < X} => r.1)
    (fun c : {c : Fin b // Y ≤ c.val} => c.1)).rank

/-- `(i, j)` is a pivot: the rank inclusion–exclusion at `(i, j)` is one. -/
def IsPiv (q : Matrix (Fin a) (Fin b) K) (i j : ℕ) : Prop :=
  rk q (i + 1) j + rk q i (j + 1) = rk q i j + rk q (i + 1) (j + 1) + 1

end Piv

/-! ## Products of disjoint transpositions -/

section Swaps

variable {α : Type*} [DecidableEq α]

/-- Pairwise disjoint pairs. -/
def PDisj (p q : α × α) : Prop := p.1 ≠ q.1 ∧ p.1 ≠ q.2 ∧ p.2 ≠ q.1 ∧ p.2 ≠ q.2

end Swaps

/-! ## Edges from pivots -/

section Edge

variable {m : ℕ}

/-- The partial swap `[[1 - q, q], [q, 1 - q]]` over `ℚ`. -/
def pswQ (q : Matrix (Fin m) (Fin m) ℚ) : QMat2 m :=
  (Matrix.fromBlocks (1 - q) q q (1 - q)).submatrix finSumFinEquiv.symm finSumFinEquiv.symm

/-- Positions of a list of runs. -/
def runPairs (rs : List (ℕ × ℕ × ℕ)) : List (ℕ × ℕ) :=
  rs.flatMap fun ρ => (List.range ρ.2.2).map fun k => (ρ.1 + k, ρ.2.1 + k)

/-- A position as a pair of frame fields. -/
def finPair (m : ℕ) (x : ℕ × ℕ) : Option (Fin (m + m) × Fin (m + m)) :=
  if h : x.1 < m ∧ x.2 < m then some (Fin.castAdd m ⟨x.1, h.1⟩, Fin.natAdd m ⟨x.2, h.2⟩) else none

end Edge

end IntMul.Kappa.R6.Bit.NB

end

section
-- Source module: Solutions.R6BitNBFlag
/-!
# Round six, bit network: the flag basis

The edge projectors are `q = S X S⁻¹` with `X` a Kronecker product on pairs `Fin n × Fin n`
(`n = h + 4`), `S = Π T K`, `K = Uᵀ ⊗ Vᵀ`. Here `T` is a unipotent change of coordinates on pairs
and `Π` an ordering of the pairs (`flagEquiv`) such that the first `k = 2n - 1` rows of `Π T` are
the sparse vectors `λ_β, ν_δ` (`Lterms`) and the last `k` columns of `T⁻¹ Πᵀ` are `ω_ε, μ_γ`
(`Rterms`). Everything here is for a pair matrix `M` (later `M = K X K⁻¹`):
`qM M = (T M T⁻¹)` reordered by `flagEquiv`.
-/

namespace IntMul.Kappa.R6.Bit.NB

open Matrix Finset

section Flag

variable {h : ℕ}

/-- Pairs. -/
abbrev Pr (n : ℕ) := Fin n × Fin n

/-- A sparse vector on pairs. -/
def sv {n : ℕ} (l : List (ℚ × Pr n)) (u : Pr n) : ℚ :=
  (l.map fun s => if s.2 = u then s.1 else 0).sum

/-- Rows `λ_β` (`i < n`) and `ν_δ` (`i = n + δ`) of `S₀`. -/
def Lterms (i : ℕ) : List (ℚ × Pr (h + 4)) :=
  if h1 : i < h + 3 then [(1, (⟨i, by omega⟩, ⟨i, by omega⟩))]
  else if i = h + 3 then [(1, (⟨h + 3, by omega⟩, ⟨0, by omega⟩)),
    (-1, (⟨0, by omega⟩, ⟨h + 3, by omega⟩))]
  else if h2 : i < 2 * h + 6 then [(1, (⟨i - (h + 4), by omega⟩, ⟨i - (h + 4) + 1, by omega⟩))]
  else if i = 2 * h + 6 then [(1, (⟨h + 3, by omega⟩, ⟨1, by omega⟩)),
    (-1, (⟨1, by omega⟩, ⟨h + 3, by omega⟩))]
  else []

/-- Columns `ω_ε` (`j < n - 1`) and `μ_γ` (`j = n - 1 + γ`) of `S₀⁻¹`. -/
def Rterms (j : ℕ) : List (ℚ × Pr (h + 4)) :=
  if h1 : j < h + 2 then [(1, (⟨j + 1, by omega⟩, ⟨j, by omega⟩))]
  else if j = h + 2 then [(1, (⟨0, by omega⟩, ⟨h + 2, by omega⟩))]
  else if h2 : j < 2 * h + 6 then [(1, (⟨j - (h + 3), by omega⟩, ⟨h + 3, by omega⟩)),
    (1, (⟨h + 3, by omega⟩, ⟨j - (h + 3), by omega⟩))]
  else if j = 2 * h + 6 then [(1, (⟨h + 3, by omega⟩, ⟨h + 3, by omega⟩))]
  else []

/-- The coordinate carrying row `i`. -/
def aL (i : ℕ) : Pr (h + 4) :=
  if h1 : i < h + 3 then (⟨i, by omega⟩, ⟨i, by omega⟩)
  else if i = h + 3 then (⟨h + 3, by omega⟩, ⟨0, by omega⟩)
  else if h2 : i < 2 * h + 6 then (⟨i - (h + 4), by omega⟩, ⟨i - (h + 4) + 1, by omega⟩)
  else (⟨h + 3, by omega⟩, ⟨1, by omega⟩)

/-- The coordinate carrying column `j` (counted from `m - k`). -/
def bL (j : ℕ) : Pr (h + 4) :=
  if h1 : j < h + 2 then (⟨j + 1, by omega⟩, ⟨j, by omega⟩)
  else if j = h + 2 then (⟨0, by omega⟩, ⟨h + 2, by omega⟩)
  else if h2 : j < 2 * h + 6 then (⟨j - (h + 3), by omega⟩, ⟨h + 3, by omega⟩)
  else (⟨h + 3, by omega⟩, ⟨h + 3, by omega⟩)

/-- The nilpotent part of `T`. -/
def Nm : Matrix (Pr (h + 4)) (Pr (h + 4)) ℚ := Matrix.of fun u v =>
  if u.1.val = h + 3 ∧ u.2.val < h + 3 ∧ v.1 = u.2 ∧ v.2.val = h + 3 then 1 else 0

/-- `T = 1 - Nm`, `T⁻¹ = 1 + Nm`. -/
def Tm : Matrix (Pr (h + 4)) (Pr (h + 4)) ℚ := 1 - Nm
def Ti : Matrix (Pr (h + 4)) (Pr (h + 4)) ℚ := 1 + Nm

lemma pr_eq_iff {a b c d : Fin (h + 4)} : ((a, b) : Pr (h + 4)) = (c, d) ↔
    a.val = c.val ∧ b.val = d.val := by
  simp [Prod.ext_iff, Fin.ext_iff]

lemma aL_inj {i i' : ℕ} (hi : i < 2 * h + 7) (hi' : i' < 2 * h + 7) (e : aL (h := h) i = aL i') :
    i = i' := by
  simp only [aL] at e
  split_ifs at e <;> simp only [pr_eq_iff] at e <;> omega

lemma bL_inj {j j' : ℕ} (hj : j < 2 * h + 7) (hj' : j' < 2 * h + 7) (e : bL (h := h) j = bL j') :
    j = j' := by
  simp only [bL] at e
  split_ifs at e <;> simp only [pr_eq_iff] at e <;> omega

lemma aL_ne_bL {i j : ℕ} (hi : i < 2 * h + 7) (hj : j < 2 * h + 7) : aL (h := h) i ≠ bL j := by
  intro e
  simp only [aL, bL] at e
  split_ifs at e <;> simp only [pr_eq_iff] at e <;> omega

lemma two_k_le : 2 * (2 * h + 7) ≤ (h + 4) * (h + 4) := by nlinarith

lemma exists_flagEquiv : ∃ e : Fin ((h + 4) * (h + 4)) ≃ Pr (h + 4),
    (∀ i (hi : i < 2 * h + 7), e ⟨i, by have := two_k_le (h := h); omega⟩ = aL i) ∧
    (∀ j (hj : j < 2 * h + 7),
      e ⟨(h + 4) * (h + 4) - (2 * h + 7) + j, by have := two_k_le (h := h); omega⟩ = bL j) := by
  classical
  have hk := two_k_le (h := h)
  let φ : Fin (2 * h + 7) ⊕ Fin (2 * h + 7) → Pr (h + 4) := Sum.elim (fun i => aL i) (fun j => bL j)
  let ψ : Fin (2 * h + 7) ⊕ Fin (2 * h + 7) → Fin ((h + 4) * (h + 4)) :=
    Sum.elim (fun i => ⟨i.val, by omega⟩) (fun j => ⟨(h + 4) * (h + 4) - (2 * h + 7) + j.val, by omega⟩)
  have hφ : Function.Injective φ := by
    rintro (i | i) (j | j) e <;> simp only [φ, Sum.elim_inl, Sum.elim_inr] at e
    · exact congrArg Sum.inl (Fin.ext (aL_inj i.isLt j.isLt e))
    · exact absurd e (aL_ne_bL i.isLt j.isLt)
    · exact absurd e.symm (aL_ne_bL j.isLt i.isLt)
    · exact congrArg Sum.inr (Fin.ext (bL_inj i.isLt j.isLt e))
  let F₀ : Fin ((h + 4) * (h + 4)) ≃ Pr (h + 4) := finProdFinEquiv.symm
  have hψ : Function.Injective (F₀ ∘ ψ) := by
    refine F₀.injective.comp ?_
    rintro (i | i) (j | j) e <;> simp only [ψ, Sum.elim_inl, Sum.elim_inr, Fin.mk.injEq] at e
    · exact congrArg Sum.inl (Fin.ext e)
    · have := i.isLt; omega
    · have := j.isLt; omega
    · exact congrArg Sum.inr (Fin.ext (by omega))
  let E : {x // x ∈ Set.range (F₀ ∘ ψ)} ≃ {x // x ∈ Set.range φ} :=
    (Equiv.ofInjective _ hψ).symm.trans (Equiv.ofInjective _ hφ)
  let σ := E.extendSubtype
  have key : ∀ s, F₀.trans σ (ψ s) = φ s := by
    intro s
    simp only [Equiv.trans_apply, σ]
    rw [Equiv.extendSubtype_apply_of_mem E (F₀ (ψ s)) ⟨s, rfl⟩]
    have h1 : (Equiv.ofInjective _ hψ).symm ⟨F₀ (ψ s), ⟨s, rfl⟩⟩ = s := by
      apply hψ
      exact Equiv.apply_ofInjective_symm hψ _
    simp only [E, Equiv.trans_apply, h1]
    rfl
  exact ⟨F₀.trans σ, fun i hi => key (Sum.inl ⟨i, hi⟩), fun j hj => key (Sum.inr ⟨j, hj⟩)⟩

/-- The ordering of the pairs. -/
noncomputable def flagEquiv : Fin ((h + 4) * (h + 4)) ≃ Pr (h + 4) :=
  Classical.choose (exists_flagEquiv (h := h))

/-- The edge projector of a pair matrix `M`, in the flag basis. -/
noncomputable def qM (M : Matrix (Pr (h + 4)) (Pr (h + 4)) ℚ) :
    Matrix (Fin ((h + 4) * (h + 4))) (Fin ((h + 4) * (h + 4))) ℚ :=
  (Tm * M * Ti).submatrix flagEquiv flagEquiv

/-- The corner entries. -/
def cor (M : Matrix (Pr (h + 4)) (Pr (h + 4)) ℚ) (i j : ℕ) : ℚ :=
  ((Rterms j).map fun t => ((Lterms i).map fun s => s.1 * M s.2 t.2).sum * t.1).sum

end Flag

end IntMul.Kappa.R6.Bit.NB

end

section
-- Source module: Solutions.R6BitNBCert
/-!
# Round six, bit network: kernel certificate for the data corner (`h = 23`)

At the witness labels `x₁ = 1`, `y₁ = (-21, 1, …, 1)`, `x₂ = (1, 2, …, 2)`,
`y₂ = (-41, 1, …, 1, 0)` (both pairs with `y ⬝ x = 1`) the `45 × 45` corner of the data-entrance
projector is invertible: modulo `p = 2³¹ - 1` it has the explicit inverse `certCols`
(checked by the kernel with list arithmetic, `decide +kernel`).
-/

set_option Elab.async false

namespace IntMul.Kappa.R6.Bit.NB

open Matrix
open scoped Kronecker

section Cert

/-- Integer versions of `Lterms`, `Rterms`. -/
def LtermsZ (h i : ℕ) : List (ℤ × Pr (h + 4)) :=
  if h1 : i < h + 3 then [(1, (⟨i, by omega⟩, ⟨i, by omega⟩))]
  else if i = h + 3 then [(1, (⟨h + 3, by omega⟩, ⟨0, by omega⟩)),
    (-1, (⟨0, by omega⟩, ⟨h + 3, by omega⟩))]
  else if h2 : i < 2 * h + 6 then [(1, (⟨i - (h + 4), by omega⟩, ⟨i - (h + 4) + 1, by omega⟩))]
  else if i = 2 * h + 6 then [(1, (⟨h + 3, by omega⟩, ⟨1, by omega⟩)),
    (-1, (⟨1, by omega⟩, ⟨h + 3, by omega⟩))]
  else []

def RtermsZ (h j : ℕ) : List (ℤ × Pr (h + 4)) :=
  if h1 : j < h + 2 then [(1, (⟨j + 1, by omega⟩, ⟨j, by omega⟩))]
  else if j = h + 2 then [(1, (⟨0, by omega⟩, ⟨h + 2, by omega⟩))]
  else if h2 : j < 2 * h + 6 then [(1, (⟨j - (h + 3), by omega⟩, ⟨h + 3, by omega⟩)),
    (1, (⟨h + 3, by omega⟩, ⟨j - (h + 3), by omega⟩))]
  else if j = 2 * h + 6 then [(1, (⟨h + 3, by omega⟩, ⟨h + 3, by omega⟩))]
  else []

/-- Integer corner entries. -/
def corZ {h : ℕ} (M : Matrix (Pr (h + 4)) (Pr (h + 4)) ℤ) (i j : ℕ) : ℤ :=
  ((RtermsZ h j).map fun t => ((LtermsZ h i).map fun s => s.1 * M s.2 t.2).sum * t.1).sum

/-! ## List arithmetic -/

def dotL : List ℕ → List ℕ → ℕ
  | a :: as, b :: bs => a * b + dotL as bs
  | _, _ => 0

/-- The product check: `rows · cols ≡ 1 (mod p)`. -/
def certChk (rows cols : List (List ℕ)) (k p : ℕ) : Bool :=
  (rows.length == k) && (cols.length == k) && rows.all (fun r => r.length == k) &&
    cols.all (fun c => c.length == k) &&
    (List.range k).all fun i => (List.range k).all fun j =>
      dotL (rows.getD i []) (cols.getD j []) % p == if i = j then 1 else 0

/-! ## The witness -/

def wx1 : Fin 23 → ℤ := fun _ => 1
def wy1 : Fin 23 → ℤ := fun i => if i.val = 0 then -21 else 1
def wx2 : Fin 23 → ℤ := fun i => if i.val = 0 then 1 else 2
def wy2 : Fin 23 → ℤ := fun i => if i.val = 0 then -41 else if i.val = 22 then 0 else 1

/-- The data pair matrix at the witness, over `ℤ`. -/
def MZ : Matrix (Pr 23) (Pr 23) ℤ := (1 - vecMulVec wx1 wy1) ⊗ₖ (1 - vecMulVec wx2 wy2)

def certRows : List (List ℕ) := [
  [2147483605, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2147483625, 2147483605, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0],
  [0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 1, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 1, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 1, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 1, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 1, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 1, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 1, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2147483626, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 0],
  [40, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 23, 60, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 1],
  [2147483565, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483603, 2147483565, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [0, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 0, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 0, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 0, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 0, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 0, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 0, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 0, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 0, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2, 1, 2, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2, 1, 2, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2, 1, 2, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2, 1, 2, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2, 1, 2, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2, 1, 2, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2, 1, 2147483605, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 2, 0],
  [2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 0, 2, 2147483626, 2147483565, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1, 0],
  [2147483565, 2147483646, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 61, 2147483645, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 1]]

def certCols : List (List ℕ) := [
  [2147483646, 41, 41, 41, 41, 41, 41, 41, 41, 41, 41, 41, 41, 41, 41, 41, 41, 41, 41, 41, 41, 41, 2147483646, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 2147483604, 859, 2147483623],
  [1807028922, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 1073741843, 20, 1414196537, 1073741781, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 1073741782, 398, 1780840275],
  [1099930648, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 19, 1047552989, 1073741785, 1073741785, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 1073741786, 380, 523776651],
  [1833217747, 18, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 1073741841, 18, 1388007714, 2147483610, 1073741787, 1073741787, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 1073741788, 360, 157133094],
  [419021199, 17, 17, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 17, 1728462439, 2147483612, 2147483612, 1073741789, 1073741789, 1073741790, 1073741790, 1073741790, 1073741790, 1073741790, 1073741790, 1073741790, 1073741790, 1073741790, 1073741790, 1073741790, 1073741790, 1073741790, 1073741790, 1073741790, 1073741790, 340, 1937973184],
  [1152308298, 16, 16, 16, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 1073741839, 16, 2068917164, 2147483614, 2147483614, 2147483614, 1073741791, 1073741791, 1073741792, 1073741792, 1073741792, 1073741792, 1073741792, 1073741792, 1073741792, 1073741792, 1073741792, 1073741792, 1073741792, 1073741792, 1073741792, 1073741792, 1073741792, 320, 1571329627],
  [1885595397, 15, 15, 15, 15, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 15, 261888242, 2147483616, 2147483616, 2147483616, 2147483616, 1073741793, 1073741793, 1073741794, 1073741794, 1073741794, 1073741794, 1073741794, 1073741794, 1073741794, 1073741794, 1073741794, 1073741794, 1073741794, 1073741794, 1073741794, 1073741794, 300, 1204686070],
  [471398849, 14, 14, 14, 14, 14, 1073741837, 1073741837, 1073741837, 1073741837, 1073741837, 1073741837, 1073741837, 1073741837, 1073741837, 1073741837, 1073741837, 1073741837, 1073741837, 1073741837, 1073741837, 14, 602342967, 2147483618, 2147483618, 2147483618, 2147483618, 2147483618, 1073741795, 1073741795, 1073741796, 1073741796, 1073741796, 1073741796, 1073741796, 1073741796, 1073741796, 1073741796, 1073741796, 1073741796, 1073741796, 1073741796, 1073741796, 280, 838042513],
  [1204685948, 13, 13, 13, 13, 13, 13, 1073741836, 1073741836, 1073741836, 1073741836, 1073741836, 1073741836, 1073741836, 1073741836, 1073741836, 1073741836, 1073741836, 1073741836, 1073741836, 1073741836, 13, 942797692, 2147483620, 2147483620, 2147483620, 2147483620, 2147483620, 2147483620, 1073741797, 1073741797, 1073741798, 1073741798, 1073741798, 1073741798, 1073741798, 1073741798, 1073741798, 1073741798, 1073741798, 1073741798, 1073741798, 1073741798, 260, 471398956],
  [1937973047, 12, 12, 12, 12, 12, 12, 12, 1073741835, 1073741835, 1073741835, 1073741835, 1073741835, 1073741835, 1073741835, 1073741835, 1073741835, 1073741835, 1073741835, 1073741835, 1073741835, 12, 1283252417, 2147483622, 2147483622, 2147483622, 2147483622, 2147483622, 2147483622, 2147483622, 1073741799, 1073741799, 1073741800, 1073741800, 1073741800, 1073741800, 1073741800, 1073741800, 1073741800, 1073741800, 1073741800, 1073741800, 1073741800, 240, 104755399],
  [523776499, 11, 11, 11, 11, 11, 11, 11, 11, 1073741834, 1073741834, 1073741834, 1073741834, 1073741834, 1073741834, 1073741834, 1073741834, 1073741834, 1073741834, 1073741834, 1073741834, 11, 1623707142, 2147483624, 2147483624, 2147483624, 2147483624, 2147483624, 2147483624, 2147483624, 2147483624, 1073741801, 1073741801, 1073741802, 1073741802, 1073741802, 1073741802, 1073741802, 1073741802, 1073741802, 1073741802, 1073741802, 1073741802, 220, 1885595489],
  [1257063598, 10, 10, 10, 10, 10, 10, 10, 10, 10, 1073741833, 1073741833, 1073741833, 1073741833, 1073741833, 1073741833, 1073741833, 1073741833, 1073741833, 1073741833, 1073741833, 10, 1964161867, 2147483626, 2147483626, 2147483626, 2147483626, 2147483626, 2147483626, 2147483626, 2147483626, 2147483626, 1073741803, 1073741803, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 200, 1518951932],
  [1990350697, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 1073741832, 1073741832, 1073741832, 1073741832, 1073741832, 1073741832, 1073741832, 1073741832, 1073741832, 1073741832, 9, 157132945, 2147483628, 2147483628, 2147483628, 2147483628, 2147483628, 2147483628, 2147483628, 2147483628, 2147483628, 2147483628, 1073741805, 1073741805, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 180, 1152308375],
  [576154149, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 1073741831, 1073741831, 1073741831, 1073741831, 1073741831, 1073741831, 1073741831, 1073741831, 1073741831, 8, 497587670, 2147483630, 2147483630, 2147483630, 2147483630, 2147483630, 2147483630, 2147483630, 2147483630, 2147483630, 2147483630, 2147483630, 1073741807, 1073741807, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 160, 785664818],
  [1309441248, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 1073741830, 1073741830, 1073741830, 1073741830, 1073741830, 1073741830, 1073741830, 1073741830, 7, 838042395, 2147483632, 2147483632, 2147483632, 2147483632, 2147483632, 2147483632, 2147483632, 2147483632, 2147483632, 2147483632, 2147483632, 2147483632, 1073741809, 1073741809, 1073741810, 1073741810, 1073741810, 1073741810, 1073741810, 1073741810, 140, 419021261],
  [2042728347, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 1073741829, 1073741829, 1073741829, 1073741829, 1073741829, 1073741829, 1073741829, 6, 1178497120, 2147483634, 2147483634, 2147483634, 2147483634, 2147483634, 2147483634, 2147483634, 2147483634, 2147483634, 2147483634, 2147483634, 2147483634, 2147483634, 1073741811, 1073741811, 1073741812, 1073741812, 1073741812, 1073741812, 1073741812, 120, 52377704],
  [628531799, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 1073741828, 1073741828, 1073741828, 1073741828, 1073741828, 1073741828, 5, 1518951845, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 1073741813, 1073741813, 1073741814, 1073741814, 1073741814, 1073741814, 100, 1833217794],
  [1361818898, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 1073741827, 1073741827, 1073741827, 1073741827, 1073741827, 4, 1859406570, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 1073741815, 1073741815, 1073741816, 1073741816, 1073741816, 80, 1466574237],
  [2095105997, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 1073741826, 1073741826, 1073741826, 1073741826, 3, 52377648, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 1073741817, 1073741817, 1073741818, 1073741818, 60, 1099930680],
  [680909449, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1073741825, 1073741825, 1073741825, 2, 392832373, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 1073741819, 1073741819, 1073741820, 40, 733287123],
  [1414196548, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1073741824, 1073741824, 1, 733287098, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 1073741821, 1073741821, 20, 366643566],
  [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1073741823, 0, 1073741823, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 1073741823, 2147483646, 9],
  [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2147483630],
  [1073741824, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 1073741803, 2147483626, 12, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 1073741868, 2147483230, 2147483453],
  [1780840098, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 1073741804, 2147483627, 366643559, 1073741863, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 1073741862, 2147483246, 1257063448],
  [1047552999, 2147483628, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 1073741805, 2147483628, 26188834, 38, 1073741861, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 1073741860, 2147483266, 1623707005],
  [314265900, 2147483629, 2147483629, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 1073741806, 2147483629, 1833217756, 36, 36, 1073741859, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 1073741858, 2147483286, 1990350562],
  [1728462448, 2147483630, 2147483630, 2147483630, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 1073741807, 2147483630, 1492763031, 34, 34, 34, 1073741857, 1073741856, 1073741856, 1073741856, 1073741856, 1073741856, 1073741856, 1073741856, 1073741856, 1073741856, 1073741856, 1073741856, 1073741856, 1073741856, 1073741856, 1073741856, 1073741856, 2147483306, 209510472],
  [995175349, 2147483631, 2147483631, 2147483631, 2147483631, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 1073741808, 2147483631, 1152308306, 32, 32, 32, 32, 1073741855, 1073741854, 1073741854, 1073741854, 1073741854, 1073741854, 1073741854, 1073741854, 1073741854, 1073741854, 1073741854, 1073741854, 1073741854, 1073741854, 1073741854, 1073741854, 2147483326, 576154029],
  [261888250, 2147483632, 2147483632, 2147483632, 2147483632, 2147483632, 1073741809, 1073741809, 1073741809, 1073741809, 1073741809, 1073741809, 1073741809, 1073741809, 1073741809, 1073741809, 1073741809, 1073741809, 1073741809, 1073741809, 1073741809, 2147483632, 811853581, 30, 30, 30, 30, 30, 1073741853, 1073741852, 1073741852, 1073741852, 1073741852, 1073741852, 1073741852, 1073741852, 1073741852, 1073741852, 1073741852, 1073741852, 1073741852, 1073741852, 1073741852, 2147483346, 942797586],
  [1676084798, 2147483633, 2147483633, 2147483633, 2147483633, 2147483633, 2147483633, 1073741810, 1073741810, 1073741810, 1073741810, 1073741810, 1073741810, 1073741810, 1073741810, 1073741810, 1073741810, 1073741810, 1073741810, 1073741810, 1073741810, 2147483633, 471398856, 28, 28, 28, 28, 28, 28, 1073741851, 1073741850, 1073741850, 1073741850, 1073741850, 1073741850, 1073741850, 1073741850, 1073741850, 1073741850, 1073741850, 1073741850, 1073741850, 1073741850, 2147483366, 1309441143],
  [942797699, 2147483634, 2147483634, 2147483634, 2147483634, 2147483634, 2147483634, 2147483634, 1073741811, 1073741811, 1073741811, 1073741811, 1073741811, 1073741811, 1073741811, 1073741811, 1073741811, 1073741811, 1073741811, 1073741811, 1073741811, 2147483634, 130944131, 26, 26, 26, 26, 26, 26, 26, 1073741849, 1073741848, 1073741848, 1073741848, 1073741848, 1073741848, 1073741848, 1073741848, 1073741848, 1073741848, 1073741848, 1073741848, 1073741848, 2147483386, 1676084700],
  [209510600, 2147483635, 2147483635, 2147483635, 2147483635, 2147483635, 2147483635, 2147483635, 2147483635, 1073741812, 1073741812, 1073741812, 1073741812, 1073741812, 1073741812, 1073741812, 1073741812, 1073741812, 1073741812, 1073741812, 1073741812, 2147483635, 1937973053, 24, 24, 24, 24, 24, 24, 24, 24, 1073741847, 1073741846, 1073741846, 1073741846, 1073741846, 1073741846, 1073741846, 1073741846, 1073741846, 1073741846, 1073741846, 1073741846, 2147483406, 2042728257],
  [1623707148, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 2147483636, 1073741813, 1073741813, 1073741813, 1073741813, 1073741813, 1073741813, 1073741813, 1073741813, 1073741813, 1073741813, 1073741813, 2147483636, 1597518328, 22, 22, 22, 22, 22, 22, 22, 22, 22, 1073741845, 1073741844, 1073741844, 1073741844, 1073741844, 1073741844, 1073741844, 1073741844, 1073741844, 1073741844, 1073741844, 2147483426, 261888167],
  [890420049, 2147483637, 2147483637, 2147483637, 2147483637, 2147483637, 2147483637, 2147483637, 2147483637, 2147483637, 2147483637, 1073741814, 1073741814, 1073741814, 1073741814, 1073741814, 1073741814, 1073741814, 1073741814, 1073741814, 1073741814, 2147483637, 1257063603, 20, 20, 20, 20, 20, 20, 20, 20, 20, 20, 1073741843, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 1073741842, 2147483446, 628531724],
  [157132950, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 2147483638, 1073741815, 1073741815, 1073741815, 1073741815, 1073741815, 1073741815, 1073741815, 1073741815, 1073741815, 2147483638, 916608878, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 18, 1073741841, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 1073741840, 2147483466, 995175281],
  [1571329498, 2147483639, 2147483639, 2147483639, 2147483639, 2147483639, 2147483639, 2147483639, 2147483639, 2147483639, 2147483639, 2147483639, 2147483639, 1073741816, 1073741816, 1073741816, 1073741816, 1073741816, 1073741816, 1073741816, 1073741816, 2147483639, 576154153, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 16, 1073741839, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 1073741838, 2147483486, 1361818838],
  [838042399, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 2147483640, 1073741817, 1073741817, 1073741817, 1073741817, 1073741817, 1073741817, 1073741817, 2147483640, 235699428, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 14, 1073741837, 1073741836, 1073741836, 1073741836, 1073741836, 1073741836, 1073741836, 2147483506, 1728462395],
  [104755300, 2147483641, 2147483641, 2147483641, 2147483641, 2147483641, 2147483641, 2147483641, 2147483641, 2147483641, 2147483641, 2147483641, 2147483641, 2147483641, 2147483641, 1073741818, 1073741818, 1073741818, 1073741818, 1073741818, 1073741818, 2147483641, 2042728350, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 12, 1073741835, 1073741834, 1073741834, 1073741834, 1073741834, 1073741834, 2147483526, 2095105952],
  [1518951848, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 2147483642, 1073741819, 1073741819, 1073741819, 1073741819, 1073741819, 2147483642, 1702273625, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 1073741833, 1073741832, 1073741832, 1073741832, 1073741832, 2147483546, 314265862],
  [785664749, 2147483643, 2147483643, 2147483643, 2147483643, 2147483643, 2147483643, 2147483643, 2147483643, 2147483643, 2147483643, 2147483643, 2147483643, 2147483643, 2147483643, 2147483643, 2147483643, 1073741820, 1073741820, 1073741820, 1073741820, 2147483643, 1361818900, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 1073741831, 1073741830, 1073741830, 1073741830, 2147483566, 680909419],
  [52377650, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 2147483644, 1073741821, 1073741821, 1073741821, 2147483644, 1021364175, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 1073741829, 1073741828, 1073741828, 2147483586, 1047552976],
  [1466574198, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 1073741822, 1073741822, 2147483645, 680909450, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 1073741827, 1073741826, 2147483606, 1414196533],
  [733287099, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 2147483646, 1073741823, 2147483646, 340454725, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 1073741825, 2147483626, 1780840090],
  [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2147483646, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 2147483645, 18]]

/-- The prime of the certificate. -/
abbrev certP : ℕ := 2147483647

instance : Fact (1 < certP) := ⟨by norm_num⟩

/-- The witness vectors over `ℚ`. -/
def qx1 : Fin 23 → ℚ := fun i => (wx1 i : ℚ)
def qy1 : Fin 23 → ℚ := fun i => (wy1 i : ℚ)
def qx2 : Fin 23 → ℚ := fun i => (wx2 i : ℚ)
def qy2 : Fin 23 → ℚ := fun i => (wy2 i : ℚ)

end Cert

end IntMul.Kappa.R6.Bit.NB

end

section
-- Source module: Solutions.R6BitNBClass
/-!
# Round six, bit network: Bruhat profiles of the edge classes (flag basis, ℚ)

For transformed label data (vectors `x, y` with `y ⬝ x = 1`, idempotents `π`) satisfying the
genericity conditions, the projectors `qM M` of the edge classes have the claimed pivots, hence
edges with the claimed runs (`edge_of_pivs`).
-/

namespace IntMul.Kappa.R6.Bit.NB

open Matrix Finset
open scoped Kronecker

section Class

variable {h : ℕ}

section Data

variable (x₁ y₁ x₂ y₂ : Fin (h + 4) → ℚ)

/-- The rank-one row factor of the data corner block. -/
def dU (i : ℕ) : ℚ := if hi : i < h + 3 then x₁ ⟨i, by omega⟩ * x₂ ⟨i, by omega⟩ else 0

/-- The rank-one column factor of the data corner block. -/
def dV (γ : ℕ) : ℚ :=
  if hγ : γ < h + 3 then y₁ ⟨γ, by omega⟩ * y₂ ⟨h + 3, by omega⟩ + y₁ ⟨h + 3, by omega⟩ * y₂ ⟨γ, by omega⟩
  else y₁ ⟨h + 3, by omega⟩ * y₂ ⟨h + 3, by omega⟩

end Data

/-! ## Side edges: factorization through `Fin n` -/

section Side

/-- `(1 ⊗ x)` and `(1 ⊗ yᵀ)` (stage one), `(x ⊗ 1)`, `(yᵀ ⊗ 1)` (stage two). -/
def Cx (x : Fin (h + 4) → ℚ) : Matrix (Pr (h + 4)) (Fin (h + 4)) ℚ :=
  Matrix.of fun u a => if u.1 = a then x u.2 else 0
def Ry (y : Fin (h + 4) → ℚ) : Matrix (Fin (h + 4)) (Pr (h + 4)) ℚ :=
  Matrix.of fun a v => if a = v.1 then y v.2 else 0
def Cx2 (x : Fin (h + 4) → ℚ) : Matrix (Pr (h + 4)) (Fin (h + 4)) ℚ :=
  Matrix.of fun u a => if u.2 = a then x u.1 else 0
def Ry2 (y : Fin (h + 4) → ℚ) : Matrix (Fin (h + 4)) (Pr (h + 4)) ℚ :=
  Matrix.of fun a v => if a = v.2 then y v.1 else 0

/-- The flag frame, rows (`Te`) and columns (`Te'`). -/
noncomputable def Te : Matrix (Fin ((h + 4) * (h + 4))) (Pr (h + 4)) ℚ := Tm.submatrix flagEquiv id
noncomputable def Te' : Matrix (Pr (h + 4)) (Fin ((h + 4) * (h + 4))) ℚ := Ti.submatrix id flagEquiv

variable (x y : Fin (h + 4) → ℚ)

end Side

end Class

end IntMul.Kappa.R6.Bit.NB

end

section
-- Source module: Solutions.R6BitNBEdges
/-!
# Round six, bit network: edges of the classes (over ℚ)

`EdgeQ e q`: valid runs, lower triangular `E₁, E₂` with nonzero diagonals, and frame
`E₁ σ E₂ = pswQ q`. For each class, under the genericity conditions on the transformed labels,
an edge with the claimed runs exists.
-/

namespace IntMul.Kappa.R6.Bit.NB

open Matrix Finset
open scoped Kronecker

/-- An edge realizing the partial swap of `q` over `ℚ`. -/
def EdgeQ {m : ℕ} (e : Edge m) (q : Matrix (Fin m) (Fin m) ℚ) : Prop :=
  (∀ ρ ∈ e.runs, RunOK m ρ) ∧
    (∀ i j, i < j → e.E₁ i j = 0) ∧ (∀ i, e.E₁ i i ≠ 0) ∧
    (∀ i j, i < j → e.E₂ i j = 0) ∧ (∀ i, e.E₂ i i ≠ 0) ∧
    e.E₁ * ((e.runs.flatMap (runPiv m)).map fun p => Equiv.swap p.1 p.2).prod.permMatrix ℚ *
      e.E₂ = pswQ q

/-! ## Labels -/

/-! ## Aux edges -/

/-! ## Side edges -/

section Side

variable {h : ℕ}

/-- The side runs of a rank-`r` idempotent of size `n`. -/
def sideRuns (n m r : ℕ) : List (ℕ × ℕ × ℕ) := if n < 2 * r then [(n - r, m - r, 2 * r - n)] else []

end Side

/-! ## Data entrance edges -/

section Data

variable {h : ℕ}

/-- The data runs: the middle block and the corner run. -/
def dataRuns (n m : ℕ) : List (ℕ × ℕ × ℕ) :=
  [(2 * n - 1, 2 * n - 1, m - 2 * (2 * n - 1)), (1, m - n + 1, n - 2)]

end Data

end IntMul.Kappa.R6.Bit.NB

end

section
-- Source module: Solutions.R6BitNBFormal
/-!
# Round six, bit side: the formal-frame calculus (`FormalOK`), replacing `LabOK`

`R6BitNBObst` shows that single-label networks (`LabOK`: every gate touches wires with equal
frames) cannot save anything. S. Jain's two-stage network needs wires whose content is a **sum of
terms at different frames**: after the two stages the data outputs are `A = F y` and
`B = F x + E y`, and the copy correction (copy `A`, frame change `T` on the copy, `T F = E`, XOR
into `B`) cancels `E y` in characteristic two.

The calculus: a wire's content is tracked as a **formal value**, a finite `R`-combination of
framed inputs `(F, u)`, meaning `Φ(F)(ins u)` (`frameArr`). Edges multiply every frame on the left
by the edge matrix (`lmulF`), gates act linearly; no label condition on gates. If every role
`ρ w` ends with the single term `(swapMat, w)`, the ideal network is correct
(`idealOK_of_formal`), and the generalized Prop. 11 follows (`prop11H_formal`).

For proofs about concrete networks:
* `formal_labels`: on a program segment whose gates are label consistent (the old `LabGates`),
  formal values of the form `L_w · φ_w` evolve as `L'_w · (scalar circuit on φ)_w`, where the
  scalar circuit runs on **module**-valued wires (`scalarStepM`; here the module of formal
  values). So each stage of the two-stage motif is handled by its frame labels plus its scalar
  identity, and the stages compose through formal values.
* partial swaps `psw p = [[1-p, p], [p, 1-p]]`: `psw p * psw q = psw (p + q - 2pq)`,
  `psw 0 = 1`, `psw 1 = swapMat` (`psw_mul`, …);
* `correction_gadget`: the copy correction on formal values.
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Bit

open AModel AModelFac Matrix

/-- Frame matrices at field size `N`. -/
abbrev FMat (m N : ℕ) := Matrix (Fin (m + m)) (Fin (m + m)) (ZMod N)

/-- Formal values: finite `R`-combinations of framed inputs `(F, u)`. -/
abbrev FV (R : Type*) [CommRing R] (U : Type*) (m N : ℕ) := (FMat m N × U) →₀ R

section Formal

variable {R : Type*} [CommRing R] {U : Type*} {m N : ℕ}

/-- Left multiplication of every frame by `L`. -/
noncomputable def lmulF (L : FMat m N) : FV R U m N →ₗ[R] FV R U m N :=
  Finsupp.lmapDomain R R (fun p : FMat m N × U => (L * p.1, p.2))

end Formal

/-! ## Module-valued scalar circuits -/

section ModuleScalar

variable {R : Type*} [CommRing R] {m : ℕ} {Wr : Type*} [DecidableEq Wr]
  {M : Type*} [AddCommGroup M] [Module R M]

/-- A gate on module-valued wires. -/
def gateVecM (g : Matrix Wr Wr R) (S : Finset Wr) (v : Wr → M) : Wr → M :=
  fun w => if w ∈ S then ∑ w' ∈ S, g w w' • v w' else v w

/-- The scalar circuit on module-valued wires (edges act trivially). -/
def scalarStepM (v : Wr → M) : Instr Wr R m → Wr → M
  | .gate g S => gateVecM g S v
  | .edge _ _ => v

end ModuleScalar

/-! ## Formal execution -/

section FormalRun

variable {R : Type*} [CommRing R] {m : ℕ} {Wr : Type*} [Fintype Wr] [DecidableEq Wr] {U : Type*}
  (N : ℕ)

/-- One instruction on formal values: gates linearly, edges by left multiplication. -/
noncomputable def fStep (f : Wr → FV R U m N) : Instr Wr R m → Wr → FV R U m N
  | .gate g S => gateVecM g S f
  | .edge w e => Function.update f w (lmulF (edgeMat N e) (f w))

end FormalRun

/-! ## Denotation and soundness -/

section Sound

variable {R : Type*} [CommRing R] {m : ℕ} {Wr : Type*} [Fintype Wr] [DecidableEq Wr] {U : Type*}
  {sh : Shape} {N : ℕ} [NeZero N] (Λ : Layout sh (m + m) N) (ins : U → List R)

/-- Entry `i` of the array denoted by a formal value. -/
noncomputable def den (i : ℕ) : FV R U m N →ₗ[R] R :=
  Finsupp.linearCombination R (fun p : FMat m N × U => (frameArr Λ p.1 (ins p.2)).getD i 0)

end Sound

namespace QHNet

variable {R : Type*} [CommRing R] {W T m : ℕ}

/-- Initial formal values: role `u` holds `(1, u)`, temporaries `0`. -/
noncomputable def fInit (N : ℕ) : Fin W ⊕ Fin T → FV R (Fin W) m N :=
  Sum.elim (fun u => Finsupp.single (1, u) 1) fun _ => 0

/-- **Formal correctness**: role `ρ w` ends with the single framed term `(swapMat, w)`. -/
def FormalOK (C : QHNet R W T m) (N : ℕ) : Prop :=
  ∀ w, C.prog.foldl (fStep N) (fInit N) (.inl (C.ρ w)) = Finsupp.single (swapMat, w) 1

end QHNet

/-! ## Partial swaps and the copy correction -/

section PSwap

variable {N m : ℕ}

/-- The partial swap `[[1 - p, p], [p, 1 - p]]`. -/
def psw (p : Matrix (Fin m) (Fin m) (ZMod N)) : FMat m N := blk (1 - p) p p (1 - p)

end PSwap

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6BitNBSim
/-!
# Round six, bit network: similarity of idempotents, explicit corner idempotent, transitivity

* `idem_similar`: idempotent matrices over `ℚ` of equal rank are similar.
* `eIdem n r`: an explicit idempotent of rank `r` whose top-right `(n-r)`-corner is the identity
  (for `n < 2r`).
* `conj_rank_one`: for `y ⬝ x = 1 = y' ⬝ x'` some invertible `Q` has `Q (x yᵀ) Q⁻¹ = x' y'ᵀ`.
-/

namespace IntMul.Kappa.R6.Bit.NB

open Matrix Finset

section EIdem

/-- The explicit idempotent: rows `i < n - r` are `e_{r+i}`, the others `e_i`. -/
def eIdem (n r : ℕ) : Matrix (Fin n) (Fin n) ℚ :=
  Matrix.of fun i j => if i.val < n - r then (if j.val = r + i.val then 1 else 0)
    else (if j = i then 1 else 0)

variable {n r : ℕ}

end EIdem

end IntMul.Kappa.R6.Bit.NB

end

section
-- Source module: Solutions.R6BitNBGen
/-!
# Round six, bit network: genericity of the flag basis

Polynomials in the entries of two generic matrices `U, V` (`MvPolynomial (Bool × Fin n × Fin n) ℚ`)
encode the genericity conditions through the scaled conjugate `sconj W A = Wᵀ A adj(W)ᵀ`
(`= det W • Wᵀ A W⁻ᵀ`). Each condition polynomial is nonzero (witness via `idem_similar`), so a
rational point avoids all of them (`exists_eval_ne`).
-/

namespace IntMul.Kappa.R6.Bit.NB

open Matrix Finset MvPolynomial
open scoped Kronecker

section Poly

variable {n : ℕ}

abbrev Vr (n : ℕ) := Bool × Fin n × Fin n
abbrev Rp (n : ℕ) := MvPolynomial (Vr n) ℚ

noncomputable def XU : Matrix (Fin n) (Fin n) (Rp n) := Matrix.of fun i j => X (false, i, j)
noncomputable def XV : Matrix (Fin n) (Fin n) (Rp n) := Matrix.of fun i j => X (true, i, j)
noncomputable def cm {ι κ : Type*} (A : Matrix ι κ ℚ) : Matrix ι κ (Rp n) := A.map C

def Uf (f : Vr n → ℚ) : Matrix (Fin n) (Fin n) ℚ := Matrix.of fun i j => f (false, i, j)
def Vf (f : Vr n → ℚ) : Matrix (Fin n) (Fin n) ℚ := Matrix.of fun i j => f (true, i, j)
def ptUV (U V : Matrix (Fin n) (Fin n) ℚ) : Vr n → ℚ :=
  fun p => if p.1 then V p.2.1 p.2.2 else U p.2.1 p.2.2

/-- Scaled conjugate `Wᵀ A adj(W)ᵀ`. -/
def sconj {S : Type*} [CommRing S] (W A : Matrix (Fin n) (Fin n) S) : Matrix (Fin n) (Fin n) S :=
  Wᵀ * A * W.adjugateᵀ

end Poly

/-! ## Condition polynomials -/

section Conds

variable {n : ℕ}

/-- Label entry `(β, last)` of the scaled conjugate. -/
noncomputable def pA (W : Matrix (Fin n) (Fin n) (Rp n)) (P : Matrix (Fin n) (Fin n) ℚ) (β l : Fin n) :
    Rp n := sconj W (cm P) β l

/-- Corner minor of the scaled conjugate. -/
noncomputable def pCor (W : Matrix (Fin n) (Fin n) (Rp n)) (A : Matrix (Fin n) (Fin n) ℚ) (r : ℕ) :
    Rp n := ((sconj W (cm A)).submatrix (fun l : Fin (n - r) => (⟨l.val, by omega⟩ : Fin n))
      (fun c : Fin (n - r) => (⟨n - (n - r) + c.val, by omega⟩ : Fin n))).det

/-- The mixed condition `x₁'_l y₁'_last + x₂'_l y₂'_last ≠ 0`, scaled. -/
noncomputable def pT (P₁ P₂ : Matrix (Fin n) (Fin n) ℚ) (l e : Fin n) : Rp n :=
  pA XU P₁ l e * (XV (n := n)).det + pA XV P₂ l e * (XU (n := n)).det

end Conds

/-! ## Witnesses -/

section Wit

variable {n : ℕ}

/-- The model rank-one label: `x = 1`, `y = e_last`. -/
def wP (n : ℕ) (hn : 0 < n) : Matrix (Fin n) (Fin n) ℚ :=
  vecMulVec (fun _ => 1) (Pi.single (⟨n - 1, by omega⟩ : Fin n) 1)

end Wit

end IntMul.Kappa.R6.Bit.NB

end

section
-- Source module: Solutions.R6BitNBMain
/-!
# 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.
-/

namespace IntMul.Kappa.R6.Bit.NB

open Matrix Finset MvPolynomial
open scoped Kronecker

section Data

variable {h : ℕ}

noncomputable def kM (P₁ P₂ : Matrix (Fin (h + 4)) (Fin (h + 4)) ℚ) :
    Matrix (Pr (h + 4)) (Pr (h + 4)) (Rp (h + 4)) :=
  ((XU (n := h + 4)).det • 1 - sconj XU (cm P₁)) ⊗ₖ ((XV (n := h + 4)).det • 1 - sconj XV (cm P₂))

noncomputable def pDat (P₁ P₂ : Matrix (Fin (h + 4)) (Fin (h + 4)) ℚ) : Rp (h + 4) :=
  (Matrix.of fun i j : Fin (2 * h + 7) =>
    (cm (n := h + 4) (Te (h := h)) * kM P₁ P₂ * cm (n := h + 4) (Te' (h := h)))
      ⟨i.val, by have := two_k_le (h := h); omega⟩
      ⟨(h + 4) * (h + 4) - (2 * h + 7) + j.val, by have := two_k_le (h := h); omega⟩).det

end Data

/-! ## Conjugation algebra -/

/-! ## The frame -/

section Frame

variable {h : ℕ}

noncomputable def Kf (U V : Matrix (Fin (h + 4)) (Fin (h + 4)) ℚ) : Matrix (Pr (h + 4)) (Pr (h + 4)) ℚ :=
  Uᵀ ⊗ₖ Vᵀ
noncomputable def Kfi (U V : Matrix (Fin (h + 4)) (Fin (h + 4)) ℚ) : Matrix (Pr (h + 4)) (Pr (h + 4)) ℚ :=
  U⁻¹ᵀ ⊗ₖ V⁻¹ᵀ

noncomputable def Sb (U V : Matrix (Fin (h + 4)) (Fin (h + 4)) ℚ) :
    Matrix (Fin ((h + 4) * (h + 4))) (Pr (h + 4)) ℚ := Te (h := h) * Kf U V
noncomputable def Sbi (U V : Matrix (Fin (h + 4)) (Fin (h + 4)) ℚ) :
    Matrix (Pr (h + 4)) (Fin ((h + 4) * (h + 4))) ℚ := Kfi U V * Te' (h := h)

end Frame

/-! ## Main theorem -/

section Main

variable {h : ℕ}

def auxRuns (h : ℕ) : List (ℕ × ℕ × ℕ) :=
  [(0, (h + 4) * (h + 4) - (h + 4), h + 4), (h + 4, h + 4, (h + 4) * (h + 4) - 2 * (h + 4))]

/-- An aux-class edge. -/
def AuxE (q : Matrix (Fin ((h + 4) * (h + 4))) (Fin ((h + 4) * (h + 4))) ℚ) : Prop :=
  ∃ e : Edge ((h + 4) * (h + 4)), EdgeQ e q ∧ e.runs = auxRuns h

/-- A side-class edge of rank `r`. -/
def SideE (q : Matrix (Fin ((h + 4) * (h + 4))) (Fin ((h + 4) * (h + 4))) ℚ) (r : ℕ) : Prop :=
  ∃ e : Edge ((h + 4) * (h + 4)), EdgeQ e q ∧ ∃ rs',
    e.runs = sideRuns (h + 4) ((h + 4) * (h + 4)) r ++ rs' ∧ (∀ ρ ∈ rs', ρ.2.2 = 1) ∧
    (runPairs (sideRuns (h + 4) ((h + 4) * (h + 4)) r)).length + rs'.length = r

/-- A data-class edge. -/
def DataE (q : Matrix (Fin ((h + 4) * (h + 4))) (Fin ((h + 4) * (h + 4))) ℚ) : Prop :=
  ∃ e : Edge ((h + 4) * (h + 4)), EdgeQ e q ∧ ∃ rs',
    e.runs = dataRuns (h + 4) ((h + 4) * (h + 4)) ++ rs' ∧ (∀ ρ ∈ rs', ρ.2.2 = 1) ∧
    rs'.length = h + 5

def lst (h : ℕ) : Fin (h + 4) := ⟨h + 4 - 1, by omega⟩

end Main

end IntMul.Kappa.R6.Bit.NB

end