Round-six κ development, definitions part 51

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_R6_Defs50
import Mathlib
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_Kappa_R6_Defs9
import Definitions.Def_IntMul_Kappa_R6_Data_BitDataSup2_1
import Definitions.Def_IntMul_Kappa_R6_Data_BitDataSup1_7
import Definitions.Def_IntMul_Kappa_R6_Data_BitDataSup0_7
import Definitions.Def_IntMul_Kappa_R6_Data_BitNBLocData
import Definitions.Def_IntMul_Kappa_R6_Data_ChkBitDim2_2
import Definitions.Def_IntMul_Kappa_R6_Data_ChkBitDim1_2
import Definitions.Def_IntMul_Kappa_R6_Data_ChkBitDim0_2
import Definitions.Def_IntMul_Kappa_R6_Data_ChkBitDagC
import Definitions.Def_IntMul_Kappa_R6_Data_BitNBGenData_0
import Definitions.Def_IntMul_Kappa_R6_Defs4
import Definitions.Def_IntMul_Kappa_R6_Data_BitNBGenData_2
import Definitions.Def_IntMul_Kappa_R6_Data_BitNBGenData_3
import Definitions.Def_IntMul_Kappa_K_Defs2

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.R6ChkPack
/-!
# Packed bit-vector kernels for reflective certificate checking (round six)

Kernel-friendly primitives on `ℕ` (every operation is a single GMP-accelerated kernel step:
`Nat.land`, `Nat.xor`, `Nat.mul`, `Nat.shiftLeft`, `Nat.shiftRight`, ...), with their bit-level
specifications.

* `row X i`: the `i`-th 32-bit field of `X` (a list of `F₂` vectors packed with stride 32).
* `pkf s f k = Σ_{i<k} f i · 2^{s i}`, `testBit_pkf`: bits of packed sums.
* `fold32`: five xor-shifts; bit `p` of `fold32 x` is the parity of bits `p, …, p+31` of `x`.
* `dotsP A B`: **all 24 × 24 inner products over `F₂` in 16 big-number operations**: for
  `A, B < 2^768` (at most 24 rows each), bit `800 j + 32 i` of `dotsP A B` is the parity of
  `row A j &&& row B i` (`dotsP_spec`).
* `tgt o k`: the target pattern with ones exactly at `(j, o + j)`, `j < k` (`testBit_tgt`).

Definitions use the `Nat.*` functions directly (not the `HAnd`/`HMul` notation) because kernel
reduction through the notation instances is about four times slower.
-/

namespace R6Chk

/-! ## Notation bridges (all `rfl`) -/

theorem nland (x y : ℕ) : Nat.land x y = x &&& y := rfl

theorem nshr (x y : ℕ) : Nat.shiftRight x y = x >>> y := rfl

/-! ## Packed sums -/

/-! ## Rows -/

/-! ## Parity and the xor-shift fold -/

/-! ## All inner products of two 24-row lists -/

/-! ## Target patterns -/

/-! ## Range check: fields below `2^n` -/

end R6Chk

end

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

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

namespace R6Chk.Bit

open R6Chk

theorem blt_dec (a b : ℕ) : Nat.blt a b = decide (a < b) := by
  rw [Bool.eq_iff_iff, Nat.blt_eq, decide_eq_true_iff]

/-- Leaf lookup: at depth `d`, branch on bit `d-1` of `i`. -/
noncomputable def btGet (t : BT) : ℕ → ℕ → ℕ :=
  BT.rec (motive := fun _ => ℕ → ℕ → ℕ) (fun x _ _ => x)
    (fun _ _ ihl ihr d i => cond (tb i (Nat.sub d 1)) (ihr (Nat.sub d 1) i) (ihl (Nat.sub d 1) i)) t

/-- Triples meeting the point set `P` (`P < 2^24`). -/
def um (P : ℕ) : ℕ :=
  Nat.lor (Nat.lor (fieldOf UMT0 1792 (Nat.land P 63)) (fieldOf UMT1 1792 (Nat.land (Nat.shiftRight P 6) 63)))
    (Nat.lor (fieldOf UMT2 1792 (Nat.land (Nat.shiftRight P 12) 63))
      (fieldOf UMT3 1792 (Nat.land (Nat.shiftRight P 18) 63)))

theorem allN_spec {n : ℕ} {p : ℕ → Bool} (h : allN n p = true) : ∀ i < n, p i = true := by
  induction n with
  | zero => intro i hi; omega
  | succ n ih =>
    have h' : p n = true ∧ allN n p = true := by simpa [allN] using h
    intro i hi
    rcases Nat.lt_succ_iff_lt_or_eq.1 hi with hi | rfl
    · exact ih h'.2 i hi
    · exact h'.1

end R6Chk.Bit

end

section
-- Source module: Solutions.R6ChkBitSup
/-!
# Bit round six (h = 23): the node-support lookup

`supT` stores the 1771-bit support masks of the 36 513 nodes of the gm-side DAG, 16 nodes per
leaf (1792-bit fields), in a depth-12 binary tree; `supG k` is the support of node `k`.
-/

set_option maxRecDepth 100000

namespace R6Chk.Bit

/-- The whole support tree (depth 12). -/
noncomputable def supT : BT := BT.node (BT.node supT0 supT1) (BT.node supT2 (BT.leaf 0))

/-- Support mask of node `k`. -/
noncomputable def supG (k : ℕ) : ℕ := fieldOf (btGet supT 12 (Nat.shiftRight k 4)) 1792 (Nat.land k 15)

end R6Chk.Bit

end

section
-- Source module: Solutions.R6ChkBitDimDefs
/-!
# Bit round six (h = 23): kernel checker for node span dimensions

For a node with support `sup` (a set of triples of `Fin 23`), its rational span is
`S = span_ℚ {𝟙_t : t ∈ sup}`. A **dimension record** certifies `finrank S = d`:

* header (64 bits): `c` (8), `d` (8), `nc` (8), `md` (8), `Q` (32): a centre `c`, the claimed
  dimension, the number of components, the certificate mode and a coordinate mask `Q`;
* `nc` components (64 bits each): `X` (24), `Y` (24), `x0` (8); `Y = 0` marks a non-bipartite
  component with point set `X`, otherwise `(X, Y)` is a bipartition and `x0 ∈ X`;
* `d` triple indices (16 bits each), then the dual rows: for `md = 0` packed `F₂` rows
  (32-bit fields), for `md = 1` rows over `ℤ/3` (2-bit coordinates, 64-bit fields).

Upper bound: every `t ∈ sup` contains `c` and lies inside one component (crossing it, if
bipartite), so `S` lies in the subspace `Wp` cut out by `x_p = 0` off `V ∪ {c}`,
`Σ_X x = Σ_Y x` per bipartite component and `Σ_V x = 2 x_c`; on `Wp` the coordinates in `Q`
determine `x` (all of `V` is in `Q` except one `x0` per bipartite component), so
`finrank S ≤ |Q| = d`.
Lower bound: the `d` listed triples lie in `sup` and have a dual family mod 2 (resp. mod 3), so
their Gram-type integer matrix has odd (resp. prime-to-3) determinant and they are independent
over `ℚ`.
-/

set_option maxRecDepth 100000

namespace R6Chk.Bit

open R6Chk

/-- Population count of the low `n` bits. -/
def popc (x : ℕ) (n : ℕ) : ℕ :=
  Nat.rec (motive := fun _ => ℕ) 0 (fun i ih => Nat.add ih (Nat.land (Nat.shiftRight x i) 1)) n

/-- All 23 points. -/
def PF : ℕ := 8388607
/-- All 1792 triple slots. -/
def TF : ℕ := Nat.sub (Nat.shiftLeft 1 1792) 1

/-- Point-set complement. -/
def pc (m : ℕ) : ℕ := Nat.xor m PF
/-- Triple-set complement (within the 1792 slots). -/
def tnot (m : ℕ) : ℕ := Nat.xor m TF

/-- Decoded component list `(X, Y, x0)`. -/
def compsDec (nc : ℕ) : ℕ → List (ℕ × ℕ × ℕ) :=
  Nat.rec (motive := fun _ => ℕ → List (ℕ × ℕ × ℕ)) (fun _ => [])
    (fun _ ih s => (fieldOf s 24 0, fieldOf s 24 1, fieldOf s 8 6) :: ih (Nat.shiftRight s 64)) nc

/-- Decoded index list (16-bit fields). -/
def idxDec (d : ℕ) : ℕ → List ℕ :=
  Nat.rec (motive := fun _ => ℕ → List ℕ) (fun _ => [])
    (fun _ ih s => fieldOf s 16 0 :: ih (Nat.shiftRight s 16)) d

/-- Points of a component. -/
def cm (e : ℕ × ℕ × ℕ) : ℕ := Nat.lor e.1 e.2.1

/-- Components pairwise disjoint (and disjoint from `acc`). -/
def pwD (acc : ℕ) : List (ℕ × ℕ × ℕ) → Bool
  | [] => true
  | e :: L => Nat.beq (Nat.land acc (cm e)) 0 && pwD (Nat.lor acc (cm e)) L

/-- One component is well formed w.r.t. centre `c` and coordinate mask `Q`. -/
def compOK (c Q : ℕ) (e : ℕ × ℕ × ℕ) : Bool :=
  Nat.blt e.1 PF.succ && Nat.blt e.2.1 PF.succ && !(tb e.1 c) && !(tb e.2.1 c) &&
    Nat.beq (Nat.land e.1 e.2.1) 0 &&
    cond (Nat.beq e.2.1 0) (Nat.beq (Nat.land e.1 Q) e.1)
      (Nat.blt e.2.2 23 && tb e.1 e.2.2 &&
        Nat.beq (Nat.land (cm e) (pc Q)) (Nat.shiftLeft 1 e.2.2))

/-- Triples allowed by one component (as a 1792-bit mask). -/
def compMask (c : ℕ) (e : ℕ × ℕ × ℕ) : ℕ :=
  cond (Nat.beq e.2.1 0) (tnot (um (pc (Nat.lor e.1 (Nat.shiftLeft 1 c)))))
    (Nat.land (Nat.land (um e.1) (um e.2.1)) (tnot (um (pc (Nat.lor (cm e) (Nat.shiftLeft 1 c))))))

/-- Union of the component masks. -/
def orL (c : ℕ) : List (ℕ × ℕ × ℕ) → ℕ
  | [] => 0
  | e :: L => Nat.lor (compMask c e) (orL c L)

/-- Allowed triples: through `c` and allowed by some component. -/
def alw (c : ℕ) (L : List (ℕ × ℕ × ℕ)) : ℕ := Nat.land (star c) (orL c L)

/-- Pack the triples of an index list into 32-bit rows. -/
def triP : List ℕ → ℕ
  | [] => 0
  | i :: I => Nat.add (tri i) (Nat.shiftLeft (triP I) 32)

/-- `F₂` dual check: `A·Bᵀ = [I_d]` with `A` the listed triples. -/
def cert2 (d : ℕ) (I : List ℕ) (P : ℕ) : Bool :=
  let A := triP I
  let B := tk P d
  Nat.ble d 24 && okR BAD23L A && okR BAD23L B && Nat.beq (dotsF A B) (tgtF 0 d)

/-- `⟨triple i, y⟩` over `ℕ` (`y` with 2-bit coordinates). -/
def dot3 (i y : ℕ) : ℕ :=
  Nat.rec (motive := fun _ => ℕ) 0
    (fun p ih => Nat.add ih (Nat.mul (Nat.land (Nat.shiftRight (tri i) p) 1) (fieldOf y 2 p))) 23

/-- Mod-3 dual check (`d` rows of 64 bits). -/
def cert3 (d : ℕ) (I : List ℕ) (P : ℕ) : Bool :=
  allN d (fun b => let y := fieldOf P 64 b;
    allN d (fun a => Nat.beq (Nat.mod (dot3 (I.getD a 0) y) 3) (cond (Nat.beq a b) 1 0))) &&
  Nat.beq I.length d

/-- Record length in bits. -/
def recLen (R : ℕ) : ℕ :=
  let d := fieldOf R 8 1
  let nc := fieldOf R 8 2
  Nat.add (Nat.add (Nat.mul 64 (Nat.succ nc)) (Nat.mul 16 d))
    (Nat.mul (cond (Nat.beq (fieldOf R 8 3) 0) 32 64) d)

/-- Check one record against the support `sup`. -/
def recBody (sup c d md Q : ℕ) (L : List (ℕ × ℕ × ℕ)) (I : List ℕ) (P : ℕ) : Bool :=
  Nat.blt c 23 && Nat.blt Q PF.succ && Nat.beq (popc Q 23) d &&
    pwD 0 L && allL (compOK c Q) L && Nat.beq (Nat.land sup (alw c L)) sup &&
    allL (fun i => Nat.blt i 1771 && tb sup i) I &&
    cond (Nat.beq md 0) (cert2 d I P) (cert3 d I P)

def recChk (sup R : ℕ) : Bool :=
  let c := fieldOf R 8 0
  let d := fieldOf R 8 1
  let nc := fieldOf R 8 2
  let md := fieldOf R 8 3
  let Q := fieldOf R 32 1
  let s := Nat.shiftRight R (Nat.mul 64 (Nat.succ nc))
  recBody sup c d md Q (compsDec nc (Nat.shiftRight R 64)) (idxDec d s) (Nat.shiftRight s (Nat.mul 16 d))

/-- `cnt` consecutive records for nodes `k, k+1, …`. -/
def recsChk (sg : ℕ → ℕ) (cnt : ℕ) : ℕ → ℕ → Bool :=
  Nat.rec (motive := fun _ => ℕ → ℕ → Bool) (fun _ _ => true)
    (fun _ ih k s => recChk (sg k) s && ih (Nat.succ k) (Nat.shiftRight s (recLen s))) cnt

/-- An element: first node (16 bits), count (16 bits), then the records. -/
def dimChk (sg : ℕ → ℕ) (G : ℕ) : Bool :=
  recsChk sg (fieldOf G 16 1) (fieldOf G 16 0) (Nat.shiftRight G 32)

end R6Chk.Bit

end

section
-- Source module: Solutions.R6ChkBitDim
/-!
# Bit round six (h = 23): soundness of the node-dimension checker

`spanS sup = span_ℚ {𝟙_{tri i} : sup.testBit i}` (`𝟙_{tri i} ∈ ℚ^23` the indicator vector of the
`i`-th triple). `recChk_sound`: if `recChk sup R = true` then `finrank ℚ (spanS sup) = d`
(the record's claimed dimension); `dimChk_sound` lifts this to a whole element.
-/

set_option maxRecDepth 100000
set_option exponentiation.threshold 2000

namespace R6Chk.Bit

open R6Chk Matrix Module

/-! ## Independence over `ℚ` from a dual family modulo `q` -/

/-! ## Bit helpers -/

theorem land1 (x i : ℕ) : Nat.land (Nat.shiftRight x i) 1 = if x.testBit i then 1 else 0 := by
  rw [nland, nshr, Nat.and_one_is_mod, Nat.testBit_eq_decide_div_mod_eq, Nat.shiftRight_eq_div_pow]
  rcases Nat.mod_two_eq_zero_or_one (x / 2 ^ i) with h | h <;> simp [h]

/-- The points of a mask. -/
def F (m : ℕ) : Finset (Fin 23) := Finset.univ.filter fun p => m.testBit p = true

theorem popc_eq (x : ℕ) : ∀ n, popc x n = ∑ i ∈ Finset.range n, if x.testBit i then 1 else 0
  | 0 => rfl
  | n + 1 => by
    rw [Finset.sum_range_succ, ← popc_eq x n]
    show Nat.add (popc x n) (Nat.land (Nat.shiftRight x n) 1) = _
    rw [land1]; rfl

theorem popc_card (x : ℕ) : popc x 23 = (F x).card := by
  rw [popc_eq, F, Finset.card_filter, ← Fin.sum_univ_eq_sum_range (fun i => if x.testBit i then 1 else 0)]

/-! ## Table facts -/

theorem tri_chk : allN 1771 (fun i => Nat.blt (tri i) PF.succ && Nat.beq (popc (tri i) 23) 3) = true := by
  decide +kernel

theorem tri_spec {i : ℕ} (hi : i < 1771) : tri i < 2 ^ 23 ∧ (F (tri i)).card = 3 := by
  have := allN_spec tri_chk i hi
  simp only [Bool.and_eq_true, Nat.beq_eq, blt_dec, decide_eq_true_eq] at this
  exact ⟨this.1, popc_card _ ▸ this.2⟩

/-- Field `r` of `UMTj`, spelled out: triples meeting `{6j + t : r.testBit t}`. -/
def umq (j r : ℕ) : ℕ → ℕ :=
  Nat.rec (motive := fun _ => ℕ) 0 (fun t ih => Nat.lor ih (cond (tb r t) (star (Nat.add (Nat.mul 6 j) t)) 0))

/-! ## Mask semantics -/

/-- What one component mask allows at a triple `i < 1771`. -/
def CompAllows (c : ℕ) (e : ℕ × ℕ × ℕ) (i : ℕ) : Prop :=
  if e.2.1 = 0 then ∀ p < 23, (tri i).testBit p = true → e.1.testBit p = true ∨ p = c
  else (∃ p < 23, e.1.testBit p = true ∧ (tri i).testBit p = true) ∧
    (∃ p < 23, e.2.1.testBit p = true ∧ (tri i).testBit p = true) ∧
    ∀ p < 23, (tri i).testBit p = true → e.1.testBit p = true ∨ e.2.1.testBit p = true ∨ p = c

/-- Components pairwise disjoint. -/
def DisjC (e e' : ℕ × ℕ × ℕ) : Prop := cm e &&& cm e' = 0

instance : Std.Symm DisjC := ⟨fun a b (h : cm a &&& cm b = 0) => by
  show cm b &&& cm a = 0; rw [Nat.land_comm]; exact h⟩

/-! ## The rational span and the upper bound -/

/-- Indicator vector of triple `i`. -/
def tvQ (i : ℕ) : Fin 23 → ℚ := fun p => if (tri i).testBit p = true then 1 else 0

/-- The rational span of the triples of `sup`. -/
def spanS (sup : ℕ) : Submodule ℚ (Fin 23 → ℚ) :=
  Submodule.span ℚ {v | ∃ i, sup.testBit i = true ∧ v = tvQ i}

/-- Union of the components. -/
def vM : List (ℕ × ℕ × ℕ) → ℕ
  | [] => 0
  | e :: L => cm e ||| vM L

def sumOn (m : ℕ) (x : Fin 23 → ℚ) : ℚ := ∑ p ∈ F m, x p

/-- The subspace cut out by the component data. -/
def Wp (c : ℕ) (L : List (ℕ × ℕ × ℕ)) : Submodule ℚ (Fin 23 → ℚ) where
  carrier := {x | (∀ p : Fin 23, (vM L).testBit p = false → (p : ℕ) ≠ c → x p = 0) ∧
    (∀ e ∈ L, e.2.1 ≠ 0 → sumOn e.1 x = sumOn e.2.1 x) ∧ sumOn (vM L) x = 2 * sumOn (2 ^ c) x}
  zero_mem' := ⟨fun _ _ _ => rfl, fun _ _ _ => by simp [sumOn], by simp [sumOn]⟩
  add_mem' := by
    rintro x y ⟨hx1, hx2, hx3⟩ ⟨hy1, hy2, hy3⟩
    refine ⟨fun p h1 h2 => by simp [hx1 p h1 h2, hy1 p h1 h2], fun e he h => ?_, ?_⟩
    · simp only [sumOn, Pi.add_apply, Finset.sum_add_distrib] at hx2 hy2 ⊢
      rw [hx2 e he h, hy2 e he h]
    · simp only [sumOn, Pi.add_apply, Finset.sum_add_distrib] at hx3 hy3 ⊢
      rw [hx3, hy3]; ring
  smul_mem' := by
    rintro a x ⟨hx1, hx2, hx3⟩
    refine ⟨fun p h1 h2 => by simp [hx1 p h1 h2], fun e he h => ?_, ?_⟩
    · simp only [sumOn, Pi.smul_apply, smul_eq_mul, ← Finset.mul_sum] at hx2 ⊢
      rw [hx2 e he h]
    · simp only [sumOn, Pi.smul_apply, smul_eq_mul, ← Finset.mul_sum] at hx3 ⊢
      rw [hx3]; ring

/-- Componentwise data facts used by the upper bound. -/
structure CompFacts (c Q : ℕ) (e : ℕ × ℕ × ℕ) : Prop where
  cX : e.1.testBit c = false
  cY : e.2.1.testBit c = false
  XY : e.1 &&& e.2.1 = 0
  nb : e.2.1 = 0 → F e.1 ⊆ F Q
  bp : e.2.1 ≠ 0 → ∃ x0 : Fin 23, x0 ∈ F e.1 ∧ ∀ p ∈ F (cm e), p ∉ F Q → p = x0
  hX : e.1 < 2 ^ 23
  hY : e.2.1 < 2 ^ 23

/-! ## Lower bound -/

/-- Integer indicator vector of a mask. -/
def bz (m : ℕ) : Fin 23 → ℤ := fun p => if m.testBit p = true then 1 else 0

/-! ## Assembly -/

/-- Decoded `(node, dimension)` pairs. -/
def recsDec (cnt : ℕ) : ℕ → ℕ → List (ℕ × ℕ) :=
  Nat.rec (motive := fun _ => ℕ → ℕ → List (ℕ × ℕ)) (fun _ _ => [])
    (fun _ ih k s => (k, fieldOf s 8 1) :: ih (Nat.succ k) (Nat.shiftRight s (recLen s))) cnt

/-- The `(node, dimension)` pairs of an element. -/
def dimList (G : ℕ) : List (ℕ × ℕ) := recsDec (fieldOf G 16 1) (fieldOf G 16 0) (Nat.shiftRight G 32)

/-! ## Label nesting from the DAG checks -/

end R6Chk.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]

end PSwapAux

end Sec_PSwap

section Sec_Bruhat

open Matrix Finset

namespace BruhatAux

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

/-- Lower triangular with nonzero diagonal. -/
def LowerND (M : Matrix (Fin m) (Fin m) K) : Prop :=
  (∀ i j, i < j → M i j = 0) ∧ ∀ i, M i i ≠ 0

/-- Rows with index `< k` are clean: zero, or a single `1` whose column is otherwise zero. -/
def Clean (B : Matrix (Fin m) (Fin m) K) (k : ℕ) : Prop :=
  ∀ i : Fin m, i.val < k → (∀ j, B i j = 0) ∨
    ∃ j, B i j = 1 ∧ (∀ j', j' ≠ j → B i j' = 0) ∧ ∀ i', i' ≠ i → B i' j = 0

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]

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.R6BitNBProjA
/-!
# Round six, bit network: `G`-orthogonal projectors on the point space

On `ℚ^23` the form `B(u, v) = u·v - (Σu)(Σv)/9` (the Gram form `G = I - J/9` of the labels). A
subspace inside a centre hyperplane `{v | Σ v = 3 v_c}` is `B`-positive definite, hence
complemented by its `B`-orthogonal; its `B`-orthogonal projector `P` is characterized by
`P v = v` on the subspace and `P w = 0` on the orthogonal (`IsPrj`). Consequences: `P² = P`,
nesting of subspaces gives both product relations, `rank P = dim`.

Line projectors `Pl T = x_T y_Tᵀ` (`x_T` the triple indicator, `y_T = G x_T / 2`, `y_T·x_T = 1`)
project onto the line of `x_T`.
-/

namespace IntMul.Kappa.R6.Bit.NB

open Matrix Module R6Chk R6Chk.Bit

/-- Points space. -/
abbrev V23 := Fin 23 → ℚ

/-- The label form. -/
def bfF (u v : V23) : ℚ := u ⬝ᵥ v - (∑ p, u p) * (∑ p, v p) / 9

/-- The label form as a bilinear form. -/
noncomputable def Bf : LinearMap.BilinForm ℚ V23 :=
  LinearMap.mk₂ ℚ bfF
    (fun u u' v => by simp only [bfF, add_dotProduct, Pi.add_apply, Finset.sum_add_distrib]; ring)
    (fun c u v => by simp only [bfF, smul_dotProduct, Pi.smul_apply, smul_eq_mul, ← Finset.mul_sum]; ring)
    (fun u v v' => by simp only [bfF, dotProduct_add, Pi.add_apply, Finset.sum_add_distrib]; ring)
    (fun c u v => by simp only [bfF, dotProduct_smul, Pi.smul_apply, smul_eq_mul, ← Finset.mul_sum]; ring)

theorem Bf_apply (u v : V23) : Bf u v = bfF u v := rfl

theorem bfF_comm (u v : V23) : bfF u v = bfF v u := by
  simp only [bfF, dotProduct_comm]; ring

theorem Bf_refl : Bf.IsRefl := fun u v h => by rw [Bf_apply, bfF_comm, ← Bf_apply]; exact h

theorem mem_orth {V : Submodule ℚ V23} {w : V23} : w ∈ Bf.orthogonal V ↔ ∀ v ∈ V, bfF v w = 0 :=
  LinearMap.BilinForm.mem_orthogonal_iff

/-- Positivity on a centre hyperplane. -/
theorem bf_pos {c : Fin 23} {v : V23} (hv : ∑ p, v p = 3 * v c) (h0 : bfF v v = 0) : v = 0 := by
  have hsq : ∑ p, v p * v p = v c * v c + ∑ p ∈ Finset.univ.erase c, v p * v p :=
    (Finset.add_sum_erase _ _ (Finset.mem_univ c)).symm
  have hsum : ∑ p, v p = v c + ∑ p ∈ Finset.univ.erase c, v p :=
    (Finset.add_sum_erase _ _ (Finset.mem_univ c)).symm
  have h1 : ∑ p ∈ Finset.univ.erase c, v p * v p = 0 := by
    have : bfF v v = ∑ p ∈ Finset.univ.erase c, v p * v p := by
      simp only [bfF, dotProduct]; rw [hsq, hv]; ring
    rw [← this, h0]
  have h2 : ∀ p ∈ Finset.univ.erase c, v p = 0 := by
    intro p hp
    have := (Finset.sum_eq_zero_iff_of_nonneg (fun q _ => mul_self_nonneg (v q))).1 h1 p hp
    exact mul_self_eq_zero.1 this
  have h3 : ∑ p ∈ Finset.univ.erase c, v p = 0 := Finset.sum_eq_zero h2
  have hc : v c = 0 := by rw [hsum, h3] at hv; linarith
  funext p
  by_cases hp : p = c
  · rw [hp, hc]; rfl
  · exact h2 p (Finset.mem_erase.2 ⟨hp, Finset.mem_univ p⟩)

/-- Subspaces of a centre hyperplane are complemented by their orthogonal. -/
theorem compl_of_centre {V : Submodule ℚ V23} {c : Fin 23} (hV : ∀ v ∈ V, ∑ p, v p = 3 * v c) :
    IsCompl V (Bf.orthogonal V) := by
  rw [LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint Bf_refl, Submodule.disjoint_def]
  intro x hx hxo
  exact bf_pos (hV x hx) (mem_orth.1 hxo x hx)

/-! ## Projector characterization -/

/-- `P` is the `B`-orthogonal projector onto `V`. -/
def IsPrj (P : Matrix (Fin 23) (Fin 23) ℚ) (V : Submodule ℚ V23) : Prop :=
  (∀ v ∈ V, P *ᵥ v = v) ∧ ∀ w ∈ Bf.orthogonal V, P *ᵥ w = 0

/-- The projector of a complemented subspace. -/
noncomputable def prjM (V : Submodule ℚ V23) (h : IsCompl V (Bf.orthogonal V)) :
    Matrix (Fin 23) (Fin 23) ℚ :=
  LinearMap.toMatrix' (V.projection (Bf.orthogonal V) h)

/-! ## Triples -/

theorem sum_tvQ {i : ℕ} (hi : i < 1771) : ∑ p, tvQ i p = 3 := by
  have h := (tri_spec hi).2
  have : ∑ p, tvQ i p = ((F (tri i)).card : ℚ) := by
    rw [F, Finset.card_filter, Nat.cast_sum]
    refine Finset.sum_congr rfl fun p _ => ?_
    simp only [tvQ]; split_ifs <;> simp_all
  rw [this, h]; norm_num

/-! ## Line projectors -/

def xv (T : ℕ) : V23 := tvQ T

def yv (T : ℕ) : V23 := fun p => (tvQ T p - (∑ q, tvQ T q) / 9) / 2

/-- The line projector `x_T y_Tᵀ`. -/
def Pl (T : ℕ) : Matrix (Fin 23) (Fin 23) ℚ := vecMulVec (xv T) (yv T)

/-- The line of a triple. -/
noncomputable def lineS (T : ℕ) : Submodule ℚ V23 := ℚ ∙ xv T

/-- Centre hyperplane condition for a support mask. -/
def HasCentre (sup : ℕ) : Prop :=
  ∃ c < 23, ∀ i, sup.testBit i = true → i < 1771 ∧ (tri i).testBit c = true

theorem centre_span {sup : ℕ} (h : HasCentre sup) : ∃ c : Fin 23, ∀ v ∈ spanS sup, ∑ p, v p = 3 * v c := by
  obtain ⟨c, hc, hsup⟩ := h
  refine ⟨⟨c, hc⟩, fun v hv => ?_⟩
  let H : Submodule ℚ V23 :=
    { carrier := {v | ∑ p, v p = 3 * v ⟨c, hc⟩}
      add_mem' := fun {a b} ha hb => by
        simp only [Set.mem_ofPred_eq, Pi.add_apply, Finset.sum_add_distrib] at *; rw [ha, hb]; ring
      zero_mem' := by simp
      smul_mem' := fun r a ha => by
        simp only [Set.mem_ofPred_eq, Pi.smul_apply, smul_eq_mul, ← Finset.mul_sum] at *; rw [ha]; ring }
  have hle : spanS sup ≤ H := by
    rw [spanS, Submodule.span_le]
    rintro _ ⟨i, hi, rfl⟩
    obtain ⟨hi1, hic⟩ := hsup i hi
    show ∑ p, tvQ i p = 3 * tvQ i ⟨c, hc⟩
    rw [sum_tvQ hi1]
    simp [tvQ, hic]
  exact hle hv

theorem compl_spanS {sup : ℕ} (h : HasCentre sup) : IsCompl (spanS sup) (Bf.orthogonal (spanS sup)) := by
  obtain ⟨c, hc⟩ := centre_span h
  exact compl_of_centre hc

open Classical in
/-- The projector of a node support (`0` without a centre). -/
noncomputable def Pnd (sup : ℕ) : Matrix (Fin 23) (Fin 23) ℚ :=
  if h : HasCentre sup then prjM (spanS sup) (compl_spanS h) else 0

end IntMul.Kappa.R6.Bit.NB

end

section
-- Source module: Solutions.R6BitNBLoc
/-!
# Round six, bit network: the local invocation programs (h = 23), definitions

Local wires: `x_t = t`, `y_T = v + T`, slot `q ↦ 2v + q`, temporary `c ↦ 2v + R + c`.
Codes: `0` (zero label), `1` (full label), `2 + T` (`t_T^⊥`), `2 + v + n` (span of node `n`).
-/

set_option maxRecDepth 100000

namespace R6Chk.Bit.Loc

noncomputable section

open R6Chk R6Chk.Bit

def NV : ℕ := 1771
def NR : ℕ := 40077

def wX (t : ℕ) : ℕ := t
def wY (T : ℕ) : ℕ := Nat.add 1771 T
def wS (q : ℕ) : ℕ := Nat.add 3542 q
def wT (c : ℕ) : ℕ := Nat.add 43619 c

def cLOW : ℕ := 0
def cHIGH : ℕ := 1
def cPT (T : ℕ) : ℕ := Nat.add 2 T
def cND (n : ℕ) : ℕ := Nat.add 1773 n

/-! ## Decoding -/

/-- A producer record: node, pivot slot, second slot + 1 (`0`: leaf), extra slots. -/
abbrev Rec := ℕ × ℕ × ℕ × List ℕ

def exDec (k : ℕ) : ℕ → List ℕ :=
  Nat.rec (motive := fun _ => ℕ → List ℕ) (fun _ => [])
    (fun _ ih s => fieldOf s 16 0 :: ih (Nat.shiftRight s 16)) k

def recsDec (cnt : ℕ) : ℕ → List Rec :=
  Nat.rec (motive := fun _ => ℕ → List Rec) (fun _ => [])
    (fun _ ih s =>
      let ne := fieldOf s 8 6
      (fieldOf s 16 0, fieldOf s 16 1, fieldOf s 16 2, exDec ne (Nat.shiftRight s 56)) ::
        ih (Nat.shiftRight s (Nat.add 56 (Nat.mul 16 ne)))) cnt

def chunkDec (x : ℕ) : List Rec := recsDec (Nat.land x 65535) (Nat.shiftRight x 16)

/-- All producer records, in topological order. -/
def recs : List Rec := GREC.flatMap chunkDec

def injS (T k : ℕ) : ℕ := fieldOf INJ 16 (Nat.add (Nat.mul 3 T) k)
def pts (T k : ℕ) : ℕ := fieldOf TPTS 5 (Nat.add (Nat.mul 3 T) k)
def retS (c : ℕ) : ℕ := fieldOf RETS 16 c
def retN (c : ℕ) : ℕ := fieldOf RETN 16 c
def srcS (t : ℕ) : ℕ := fieldOf SRC 16 t
def dimN (n : ℕ) : ℕ := fieldOf DIMT 5 n

/-! ## The word -/

/-- An instruction: code, touched wires, elementary gates `dst += src`. -/
abbrev LInstr := ℕ × List ℕ × List (ℕ × ℕ)

def touch (el : List (ℕ × ℕ)) : List ℕ := el.flatMap fun p => [p.1, p.2]

def mk (c : ℕ) (el : List (ℕ × ℕ)) : LInstr := (c, touch el, el)

/-- Elementary gates of one producer record. -/
def recEl (r : Rec) : List (ℕ × ℕ) :=
  (if r.2.2.1 = 0 then [] else [(wS r.2.1, wS (r.2.2.1 - 1))]) ++ r.2.2.2.map fun o => (wS o, wS r.2.1)

def mixF (code : ℕ → ℕ) : List LInstr := recs.map fun r => mk (code r.1) (recEl r)
def mixI (code : ℕ → ℕ) : List LInstr := recs.reverse.map fun r => mk (code r.1) (recEl r).reverse

def tri3 : List ℕ := [0, 1, 2]

def scatEl (rd : ℕ → ℕ) (T : ℕ) : List (ℕ × ℕ) := tri3.map fun k => (wY T, rd (pts T k))
def scat (rd : ℕ → ℕ) (code : ℕ → ℕ) : List LInstr :=
  (List.range NV).map fun T => mk (code T) (scatEl rd T)
def injo (code : ℕ → ℕ) : List LInstr :=
  (List.range NV).map fun T => mk (code T) (tri3.map fun k => (wY T, wS (injS T k)))
def copyo (code : ℕ → ℕ) : List LInstr :=
  (List.range NV).map fun t => mk (code t) [(wS (srcS t), wX t)]

/-- Copies of the retained slots into the temporaries. -/
def tcopy : List LInstr := (List.range 23).map fun c => mk (cND (retN c)) [(wT c, wS (retS c))]

def rdS (c : ℕ) : ℕ := wS (retS c)

/-- The ten ops of the stage-one word (plain: scatters read the retained slots). -/
def P1 : List (List LInstr) :=
  [mixF fun _ => cLOW, scat rdS fun _ => cLOW, injo fun _ => cLOW, mixI fun _ => cLOW,
    copyo fun t => cND (t + 1), mixF cND, scat rdS fun _ => cLOW, injo cPT,
    mixI fun _ => cHIGH, copyo fun _ => cHIGH]

/-- Reversal (stage two). -/
def revW (W : List (List LInstr)) : List (List LInstr) :=
  W.reverse.map fun op => op.reverse.map fun i => (i.1, i.2.1, i.2.2.reverse)

/-- The designated scatter with temporaries. -/
def scatT : List LInstr := tcopy ++ scat wT fun _ => cLOW

def W1 : List LInstr := (P1.set 6 scatT).flatten
def W2 : List LInstr := ((revW P1).set 3 (tcopy ++ (scat wT fun _ => cLOW).reverse.map
  fun i => (i.1, i.2.1, i.2.2.reverse))).flatten

/-! ## Label state -/

inductive LT where
  | leaf (x : ℕ)
  | node (l r : LT)

def ltGet (t : LT) : ℕ → ℕ → ℕ :=
  LT.rec (motive := fun _ => ℕ → ℕ → ℕ) (fun x _ _ => x)
    (fun _ _ ihl ihr d i => cond (tb i (Nat.sub d 1)) (ihr (Nat.sub d 1) i) (ihl (Nat.sub d 1) i)) t

def ltSet (t : LT) : ℕ → ℕ → ℕ → LT :=
  LT.rec (motive := fun _ => ℕ → ℕ → ℕ → LT) (fun _ _ _ x => LT.leaf x)
    (fun l r ihl ihr d i x => cond (tb i (Nat.sub d 1)) (LT.node l (ihr (Nat.sub d 1) i x))
      (LT.node (ihl (Nat.sub d 1) i x) r)) t

def ltFull (x : ℕ) : ℕ → LT :=
  Nat.rec (motive := fun _ => LT) (LT.leaf x) (fun _ ih => LT.node ih ih)

def DEP : ℕ := 16

/-- Move bookkeeping: for each touched wire not at `c`, record `(w, old)` and set it to `c`. -/
def mvStep (c : ℕ) (acc : LT × List (ℕ × ℕ)) (w : ℕ) : LT × List (ℕ × ℕ) :=
  let o := ltGet acc.1 DEP w
  cond (Nat.beq o c) acc (ltSet acc.1 DEP w c, (w, o) :: acc.2)

/-- A chunk: code, moves `(wire, old code)`, gates. -/
abbrev LChunk := ℕ × List (ℕ × ℕ) × List (ℕ × ℕ)

def genStep (acc : LT × List LChunk) (i : LInstr) : LT × List LChunk :=
  let r := i.2.1.foldl (mvStep i.1) (acc.1, [])
  (r.1, (i.1, r.2.reverse, i.2.2) :: acc.2)

def gen (st : LT) (W : List LInstr) : LT × List LChunk :=
  let r := W.foldl genStep (st, [])
  (r.1, r.2.reverse)

/-! ## Initial labels -/

def init1 : LT :=
  let t0 := (List.range NV).foldl (fun t x => ltSet t DEP (wX x) (cND (x + 1))) (ltFull cLOW DEP)
  (List.range 23).foldl (fun t c => ltSet t DEP (wT c) (cND (retN c))) t0

def init2 : LT :=
  let t0 := (List.range NV).foldl (fun t x => ltSet t DEP (wX x) cHIGH) (ltFull cLOW DEP)
  let t1 := (List.range NV).foldl (fun t T => ltSet t DEP (wY T) (cPT T)) t0
  let t2 := (List.range NR).foldl (fun t q => ltSet t DEP (wS q) cHIGH) t1
  (List.range 23).foldl (fun t c => ltSet t DEP (wT c) (cND (retN c))) t2

/-- Final sweep: every slot to code `f`. -/
def sweep (f : ℕ) : List LInstr := (List.range NR).map fun q => (f, [wS q], [])

def G1 : LT × List LChunk := gen init1 (W1 ++ sweep cHIGH)
def G2 : LT × List LChunk := gen init2 (W2 ++ sweep cLOW)

/-! ## Checks -/

end

end R6Chk.Bit.Loc

namespace R6Chk.Bit.Loc

noncomputable section

/-! ## Mask simulation of the producer on `C x` -/

end

end R6Chk.Bit.Loc

end

section
-- Source module: Solutions.R6BitNBDimCov
/-!
# Round six, bit network: the node dimension table `DIMT` is certified

The dimension records of `R6ChkBitDim0..2` list the nodes `0, 1, 2, …` in order; the kernel
checks that they cover all `36513` nodes and agree with `dimN` (the 5-bit table used by the
local programs). Hence `finrank ℚ (spanS (supG n)) = dimN n` for every node `n`.
-/

set_option maxRecDepth 100000
set_option Elab.async false

namespace R6Chk.Bit.Loc

open R6Chk R6Chk.Bit

noncomputable def dimChunks : List (List ℕ) := Dim0.chunks ++ Dim1.chunks ++ Dim2.chunks

noncomputable def dimAll : List (ℕ × ℕ) := dimChunks.flatMap fun c => c.flatMap dimList

def covStep (a : Bool × ℕ) (p : ℕ × ℕ) : Bool × ℕ :=
  (a.1 && Nat.beq p.1 a.2 && Nat.beq (dimN p.1) p.2, Nat.succ a.2)

end R6Chk.Bit.Loc

end

section
-- Source module: Solutions.R6BitNBIdSim
/-!
# Round six, bit network: node-id simulation of the producer (kernel checker)

The producer `A` (records of `recs`) runs on slots holding values of DAG nodes. The checker
tracks, for every slot, the id of the node whose value it holds (`0`: zero), packed in 16-bit
fields of one number, and checks each record against the support table `supG`:
a gate record `(n, p, b + 1, ex)` needs `supG (id p) xor supG (id b) = supG n`; a leaf record
`(n, p, 0, ex)` needs `id p = n`; the extra slots must be empty. At the end the six slots read
for target `T` hold supports xoring to `{T}`.
-/

set_option maxRecDepth 100000

namespace R6Chk.Bit.Loc

noncomputable section

open R6Chk R6Chk.Bit

/-- Set the 16-bit field `i` of `S` to `v`. -/
def setF (S i v : ℕ) : ℕ := Nat.xor S (Nat.shiftLeft (Nat.xor (fieldOf S 16 i) v) (Nat.mul 16 i))

/-- Slot ids, packed in 16-bit fields. -/
def idF (S : ℕ) (q : ℕ) : ℕ := fieldOf S 16 q

def idSet (S : ℕ) (q v : ℕ) : ℕ := setF S q v

/-- One extra slot `o` receives node `n` (it must be empty and differ from the pivot `p`). -/
def exStep (n p : ℕ) (a : Bool × ℕ) (o : ℕ) : Bool × ℕ :=
  (a.1 && Nat.blt o NR && Nat.beq (idF a.2 o) 0 && !(Nat.beq o p), idSet a.2 o n)

/-- The DAG gates `(k, a, b)`, in record order (`R6ChkBitDagC`, each `GateOK supG`). -/
def dagGL : List (ℕ × ℕ × ℕ) := DagC.gs.flatMap fun c => c.flatMap gchunkDec

/-- The pivot check of a record against the next DAG gate `g`. -/
def pivOK (S : ℕ) (r : Rec) (g : ℕ × ℕ × ℕ) : Bool :=
  Nat.blt r.2.1 NR && cond (Nat.beq r.2.2.1 0) (Nat.beq (idF S r.2.1) r.1)
    (Nat.blt (Nat.sub r.2.2.1 1) NR && !(Nat.beq r.2.1 (Nat.sub r.2.2.1 1)) &&
      Nat.beq g.1 r.1 && Nat.beq (idF S r.2.1) g.2.1 && Nat.beq (idF S (Nat.sub r.2.2.1 1)) g.2.2)

/-- Remaining gates after a record. -/
def glNext (r : Rec) (l : List (ℕ × ℕ × ℕ)) : List (ℕ × ℕ × ℕ) := cond (Nat.beq r.2.2.1 0) l l.tail

def recStep (acc : (Bool × ℕ) × List (ℕ × ℕ × ℕ)) (r : Rec) : (Bool × ℕ) × List (ℕ × ℕ × ℕ) :=
  (r.2.2.2.foldl (exStep r.1 r.2.1) (acc.1.1 && pivOK acc.1.2 r (acc.2.headD (0, 0, 0)),
    idSet acc.1.2 r.2.1 r.1), glNext r acc.2)

/-- Initial ids: source slot of triple `t` holds leaf `t + 1`. -/
def initStep (a : Bool × ℕ) (t : ℕ) : Bool × ℕ :=
  (a.1 && Nat.blt (srcS t) NR && Nat.beq (idF a.2 (srcS t)) 0, idSet a.2 (srcS t) (Nat.add t 1))

def idInit : Bool × ℕ := (List.range NV).foldl initStep (true, 0)

/-- Read check for target `T`. -/
def readOK (S : ℕ) (T : ℕ) : Bool :=
  tri3.all (fun k => Nat.blt (retS (pts T k)) NR && Nat.blt (injS T k) NR && Nat.blt (pts T k) 23) &&
  Nat.beq (tri3.foldl (fun a k => Nat.xor a (Nat.xor (supG (idF S (retS (pts T k))))
    (supG (idF S (injS T k))))) 0) (Nat.shiftLeft 1 T)

/-! ## Chained checks (three producer blocks, then the reads) -/

/-- Records of the record chunks `a, …, b - 1`. -/
def blkRecs (a b : ℕ) : List Rec := ((GREC.drop a).take (b - a)).flatMap chunkDec

/-- A block run from ids `S` (gates from position `g`) succeeds and ends at `S'`. -/
def blkChk (a b g S S' : ℕ) : Bool :=
  let r := (blkRecs a b).foldl recStep ((true, S), dagGL.drop g)
  r.1.1 && Nat.beq r.1.2 S'

def readsChk (S : ℕ) : Bool := (List.range NV).all (readOK S)

end

end R6Chk.Bit.Loc

end

section
-- Source module: Solutions.R6BitNBGenP
/-!
# Round six, bit network: the label generator on packed code states (definitions, checks)

The local code state is packed in 16-bit fields (`pget`, `setF`). `genP S W` processes the
instructions of `W`: for every touched wire whose code differs from the instruction's code it
emits a move `(wire, old code)` and updates the state; the chunk keeps the instruction's gates.

`segChk S S' cnt W`: the run from `S` ends at `S'`, every move is nested (`nestOK`), and the
move ranks are counted by `cnt`. The stage words are cut into the segments `segW1 j`, `segW2 j`.
-/

set_option maxRecDepth 100000

namespace R6Chk.Bit.Loc

noncomputable section

open R6Chk R6Chk.Bit

/-- Code states: a depth-4 tree of leaves packing 4096 codes (16-bit fields) each. -/
def pget (t : LT) (w : ℕ) : ℕ := fieldOf (ltGet t 4 (Nat.shiftRight w 12)) 16 (Nat.land w 4095)

def pset (t : LT) (w v : ℕ) : LT :=
  ltSet t 4 (Nat.shiftRight w 12) (setF (ltGet t 4 (Nat.shiftRight w 12)) (Nat.land w 4095) v)

/-- The depth-`d` tree of the leaves `k 2^d + j` (`j < 2^d`) of width `lw` of a packed number. -/
def mkTree (S lw : ℕ) : ℕ → ℕ → LT :=
  Nat.rec (motive := fun _ => ℕ → LT) (fun k => LT.leaf (fieldOf S lw k))
    (fun _ ih k => LT.node (ih (Nat.mul 2 k)) (ih (Nat.add (Nat.mul 2 k) 1)))

/-- The tree of a packed code state (leaf `k` = bits `65536 k, …`). -/
def toLT (S : ℕ) : LT := mkTree S 65536 4 0

/-- Packed number of a tree. -/
def ofLT (t : LT) : ℕ :=
  (List.range 16).foldr (fun k acc => Nat.lor (ltGet t 4 k) (Nat.shiftLeft acc 65536)) 0

def mvP (c : ℕ) (acc : LT × List (ℕ × ℕ)) (w : ℕ) : LT × List (ℕ × ℕ) :=
  cond (Nat.beq (pget acc.1 w) c) acc (pset acc.1 w c, (w, pget acc.1 w) :: acc.2)

def genStepP (acc : LT × List LChunk) (i : LInstr) : LT × List LChunk :=
  let r := i.2.1.foldl (mvP i.1) (acc.1, [])
  (r.1, (i.1, r.2.reverse, i.2.2) :: acc.2)

def genP (S : LT) (W : List LInstr) : LT × List LChunk :=
  let r := W.foldl genStepP (S, [])
  (r.1, r.2.reverse)

/-! ## Nesting of moves -/

/-- The argument table as a tree (2048 entries per leaf). -/
def argTr : LT := mkTree ARGT 65536 5 0

def argF (n : ℕ) : ℕ := fieldOf (ltGet argTr 5 (Nat.shiftRight n 11)) 32 (Nat.land n 2047)

/-- `a` is an argument of the gate `n`. -/
def argRel (a n : ℕ) : Bool :=
  Nat.beq (Nat.land (argF n) 65535) a || Nat.beq (Nat.shiftRight (argF n) 16) a

/-- The dimension table as a tree (8192 entries per leaf). -/
def dimTr : LT := mkTree DIMT 40960 3 0

def dimF (n : ℕ) : ℕ := fieldOf (ltGet dimTr 3 (Nat.shiftRight n 13)) 5 (Nat.land n 8191)

def dimCF (c : ℕ) : ℕ :=
  cond (Nat.beq c 0) 0 (cond (Nat.beq c 1) 23 (cond (Nat.blt c 1773) 22 (dimF (Nat.sub c 1773))))

/-- Count vector: rank `r` in the 32-bit field `r`. -/
def cntF (cs : List LChunk) : ℕ :=
  cs.foldl (fun acc ch => ch.2.1.foldl (fun a m =>
    Nat.add a (Nat.shiftLeft 1 (Nat.mul 32 (let a1 := dimCF m.2; let b1 := dimCF ch.1;
      cond (Nat.blt a1 b1) (Nat.sub b1 a1) (Nat.sub a1 b1))))) acc) 0

/-- Triples meeting the triple `T` in exactly one point. -/
def orthT (T : ℕ) : ℕ :=
  Nat.lor (Nat.lor (exclT (pts T 0) (pts T 1) (pts T 2)) (exclT (pts T 1) (pts T 0) (pts T 2)))
    (exclT (pts T 2) (pts T 0) (pts T 1))

def orthOK (n T : ℕ) : Bool := Nat.beq (Nat.land (supG n) (orthT T)) (supG n)

def isND (c : ℕ) : Bool := Nat.ble 1773 c && Nat.blt c 38286
def isPT (c : ℕ) : Bool := Nat.ble 2 c && Nat.blt c 1773

/-- A move between nested codes. -/
def nestOK (o c : ℕ) : Bool :=
  Nat.ble o 1 || Nat.ble c 1 ||
  (isND o && isND c && (argRel (Nat.sub o 1773) (Nat.sub c 1773) || argRel (Nat.sub c 1773) (Nat.sub o 1773))) ||
  (isND o && isPT c && orthOK (Nat.sub o 1773) (Nat.sub c 2)) ||
  (isPT o && isND c && orthOK (Nat.sub c 1773) (Nat.sub o 2))

def movesOK (cs : List LChunk) : Bool := cs.all fun ch => ch.2.1.all fun m => nestOK m.2 ch.1

def segRes (r : LT × List LChunk) (S' cnt : ℕ) : Bool :=
  Nat.beq (ofLT r.1) S' && movesOK r.2 && Nat.beq (cntF r.2) cnt

def segChk (S S' cnt : ℕ) (W : List LInstr) : Bool := segRes (genP (toLT S) W) S' cnt

/-! ## The segments -/

def mixFB (a b : ℕ) (code : ℕ → ℕ) : List LInstr := (blkRecs a b).map fun r => mk (code r.1) (recEl r)

/-- Reversal of an op (instruction order and gate order; touch lists kept). -/
def revI (op : List LInstr) : List LInstr := op.reverse.map fun i => (i.1, i.2.1, i.2.2.reverse)

/-- Sweep of the slots `a, …, b - 1` to code `f`. -/
def sweepR (a b f : ℕ) : List LInstr := (List.range' a (b - a)).map fun q => (f, [wS q], [])

def segW1 : ℕ → List LInstr
  | 0 => copyo (fun t => cND (t + 1)) ++ mixFB 0 12 cND
  | 1 => mixFB 12 24 cND
  | 2 => mixFB 24 48 cND
  | 3 => mixFB 48 72 cND
  | 4 => mixFB 72 96 cND
  | 5 => mixFB 96 120 cND
  | 6 => mixFB 120 143 cND
  | 7 => scatT ++ injo cPT
  | 8 => sweepR 0 20000 cHIGH
  | 9 => sweepR 20000 NR cHIGH
  | _ => copyo fun _ => cHIGH

def segW2 : ℕ → List LInstr
  | 0 => revI (injo cPT) ++ (tcopy ++ revI (scat wT fun _ => cLOW))
  | 1 => revI (mixFB 120 143 cND)
  | 2 => revI (mixFB 96 120 cND)
  | 3 => revI (mixFB 72 96 cND)
  | 4 => revI (mixFB 48 72 cND)
  | 5 => revI (mixFB 24 48 cND)
  | 6 => revI (mixFB 12 24 cND)
  | 7 => revI (mixFB 0 12 cND)
  | 8 => revI (copyo fun t => cND (t + 1)) ++ sweepR 0 20000 cLOW
  | _ => sweepR 20000 NR cLOW

end

end R6Chk.Bit.Loc

end

section
-- Source module: Solutions.R6BitNBArgk
/-! Round-six bit network: kernel checks tying the generator tables to the DAG data.
* `argChk`: the argument table `ARGT` lists, for every node `n ≥ 1772`, the two arguments of the
  DAG gate with head `n` (the gates of `dagGL` have heads `1772, 1773, …, 36512` in order), and `0`
  for the nodes `n < 1772`;
* `ptsChk`: the three points `pts T k` of triple `T` are the points of `tri T`. -/

set_option maxRecDepth 100000
set_option Elab.async false

namespace R6Chk.Bit.Loc

open R6Chk R6Chk.Bit

noncomputable section

def argOK (p : (ℕ × ℕ × ℕ) × ℕ) : Bool :=
  Nat.beq p.1.1 p.2 && Nat.blt p.1.2.1 65536 && Nat.blt p.1.2.2 65536 &&
    Nat.beq (argF p.2) (Nat.add p.1.2.1 (Nat.mul 65536 p.1.2.2))

def argChk : Bool :=
  Nat.beq dagGL.length 34741 && (dagGL.zip (List.range' 1772 34741)).all argOK &&
    (List.range 1772).all fun n => Nat.beq (argF n) 0

def ptsChk : Bool :=
  (List.range 1771).all fun T => Nat.blt (pts T 0) 23 && Nat.blt (pts T 1) 23 && Nat.blt (pts T 2) 23 &&
    Nat.beq (tri T) (Nat.lor (Nat.lor (Nat.shiftLeft 1 (pts T 0)) (Nat.shiftLeft 1 (pts T 1)))
      (Nat.shiftLeft 1 (pts T 2)))

end

end R6Chk.Bit.Loc

end

section
-- Source module: Solutions.R6BitNBChunk
/-!
# Round six, bit network: the label generator, soundness of the packed representation

* bit lemmas for `fieldOf` / `setF` and the trees `LT` (`ltGet`, `ltSet`, `mkTree`, `ofLT`);
* `genF`: the generator on code states `ℕ → ℕ` (the specification of `genP`);
  `genP_eq`: on trees of depth 4 with 65536-bit leaves, `genP` computes `genF` of the code
  function `pget t`;
* `segChk_sound`: the kernel segment checks give the chunks of `genF` from `fieldOf S 16`.
-/

set_option maxRecDepth 100000

namespace R6Chk.Bit.Loc

open R6Chk R6Chk.Bit

/-! ## Bits -/

/-! ## Trees -/

/-- A tree with all leaves at depth `d`, each below `2 ^ W`. -/
def Good (W : ℕ) : LT → ℕ → Prop
  | .leaf x, 0 => x < 2 ^ W
  | .leaf _, _ + 1 => False
  | .node _ _, 0 => False
  | .node l r, d + 1 => Good W l d ∧ Good W r d

/-! ## Packed code states -/

/-- Concatenation of `B`-bit words. -/
def catB (B : ℕ) (l : List ℕ) : ℕ := l.foldr (fun x acc => x ||| (acc <<< B)) 0

/-! ## The generator on code functions -/

/-- One touched wire: move it to `c` unless it is there. -/
def mvF (c : ℕ) (acc : (ℕ → ℕ) × List (ℕ × ℕ)) (w : ℕ) : (ℕ → ℕ) × List (ℕ × ℕ) :=
  if acc.1 w = c then acc else (Function.update acc.1 w c, (w, acc.1 w) :: acc.2)

def genStepF (acc : (ℕ → ℕ) × List LChunk) (i : LInstr) : (ℕ → ℕ) × List LChunk :=
  let r := i.2.1.foldl (mvF i.1) (acc.1, [])
  (r.1, (i.1, r.2.reverse, i.2.2) :: acc.2)

/-- **The label generator** (specification). -/
def genF (f : ℕ → ℕ) (W : List LInstr) : (ℕ → ℕ) × List LChunk :=
  let r := W.foldl genStepF (f, [])
  (r.1, r.2.reverse)

/-- Touched wires and codes fit 16 bits. -/
def Fits (W : List LInstr) : Prop := ∀ i ∈ W, i.1 < 65536 ∧ ∀ w ∈ i.2.1, w < 65536

/-- The code function of a packed state. -/
def codeOf (S : ℕ) : ℕ → ℕ := fun w => fieldOf S 16 w

end R6Chk.Bit.Loc

end

section
-- Source module: Solutions.R6BitNBLabGen
/-!
# Round six, bit network: programs from generated chunks

A local program is a list of chunks `(code, moves, gates)` over local wires `ℕ`. Mapped to global
wires by `ι`, a chunk becomes: one frame-change edge per move (`E old code`), then one XOR gate
`x_d ← x_d + x_s` per gate.

* `genF_labGates`: for chunks produced by `genF` (the label generator), all gates are label
  consistent (`LabGates`) as soon as every move edge maps the frame of its old code to the
  frame of its new code; the final labels are the frames of the final codes.
* `chunkProg_scalar`: the (module-valued) scalar circuit of a mapped chunk program is the local
  XOR run `xrL` of its gates.
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Bit

open R6Chk.Bit.Loc Matrix

section Prog

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

/-- The XOR gate `x_d ← x_d + x_s`. -/
def xorG (d s : Wr) : Instr Wr R m :=
  Instr.gate (fun x y => if x = y then 1 else if x = d ∧ y = s then 1 else 0) {d, s}

/-- The instructions of one chunk. -/
def chunkInstrs (ι : ℕ → Wr) (E : ℕ → ℕ → Edge m) (ch : LChunk) : List (Instr Wr R m) :=
  ch.2.1.map (fun mv => Instr.edge (ι mv.1) (E mv.2 ch.1)) ++ ch.2.2.map fun p => xorG (ι p.1) (ι p.2)

/-- The program of a chunk list. -/
def chunkProg (ι : ℕ → Wr) (E : ℕ → ℕ → Edge m) (cs : List LChunk) : List (Instr Wr R m) :=
  cs.flatMap (chunkInstrs ι E)

end Prog

/-! ## The scalar circuit of a chunk program -/

section Scalar

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

/-- Local XOR run: `u_d ← u_d + u_s` for each gate `(d, s)`. -/
def xrL (l : List (ℕ × ℕ)) (u : ℕ → M) : ℕ → M :=
  l.foldl (fun u p => Function.update u p.1 (u p.1 + u p.2)) u

variable (ι : ℕ → Wr) (D : ℕ → Prop) (E : ℕ → ℕ → Edge m)

end Scalar

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6BitNBScalA
/-!
# Round six, bit network: the producer computes the node values (`B A C = I`)

Over a module `M` of characteristic two, for inputs `x : ℕ → M`:

* XOR-run algebra: `xrL` is additive, is inverted by the reversed run, and acts on read/write
  separated gate lists by adding the sources;
* `msum x mask = Σ_{i ∈ mask} x_i`;
* `prod_vals`: after copying `x_t` into the source slots (`Cg`) and running the producer
  (`Ag`), slot `q` holds `msum x (supG (idF IDS3 q))` (the node-id simulation, checked by the
  kernel in `R6BitNBIdB0..2`);
* `reads_eq`: the six slots read for target `T` sum to `x_T` (`R6BitNBIdRd`).
-/

set_option linter.unusedSectionVars false
set_option maxRecDepth 100000

namespace IntMul.Kappa.R6.Bit

open R6Chk R6Chk.Bit R6Chk.Bit.Loc

/-! ## Masks -/

section Msum

variable {M : Type*} [AddCommGroup M]

/-- `Σ_{i ∈ mask} x_i` (masks below `2 ^ 1792`). -/
def msum (x : ℕ → M) (mask : ℕ) : M := ∑ i ∈ Finset.range 1792, if mask.testBit i then x i else 0

end Msum

/-! ## The node-id simulation -/

section IdSim

variable {M : Type*} [AddCommGroup M] (h2 : ∀ a : M, a + a = 0) (x : ℕ → M)

/-- Slot `q` holds the value of node `idF S q`. -/
def IdInv (S : ℕ) (z : ℕ → M) : Prop := ∀ q < NR, z (wS q) = msum x (supG (idF S q))

/-- The source copies `x_t ↦ slot srcS t`. -/
def Cg : List (ℕ × ℕ) := (List.range NV).map fun t => (wS (srcS t), wX t)

/-- The producer gates. -/
def Ag : List (ℕ × ℕ) := recs.flatMap recEl

/-- The reads for target `T`: retained slots of its points, then its injection slots. -/
def readSum (z : ℕ → M) (T : ℕ) : M :=
  (tri3.map fun k => z (wS (retS (pts T k)))).sum + (tri3.map fun k => z (wS (injS T k))).sum

end IdSim

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6BitNBScalB
/-!
# Round six, bit network: the scalar effect of one invocation

The gate lists of the two stage words (`G1`, `G2`) act on local wires (inputs `x`, targets `y`,
slots, temporaries) of any module of characteristic two. With the temporaries starting at `0`:
the inputs and slots are unchanged and the targets receive the inputs, `y_T ← y_T + x_T`.

The proof splits the start values into the input part and the rest. On the rest, both read blocks
add the same reads of the producer values, which cancel. On the inputs, the producer computes the
node values (`prod_vals`) and the reads give back `x_T` (`reads_eq`).
-/

set_option maxRecDepth 100000

namespace IntMul.Kappa.R6.Bit

open R6Chk R6Chk.Bit R6Chk.Bit.Loc

/-! ## Small table facts -/

/-- The retained slots and nodes of the 23 points. -/
def retChk : Bool := (List.range 23).all fun c => Nat.blt (retS c) NR && Nat.blt (retN c) 36513

/-! ## Well-formedness of the producer gates -/

/-- A slot-to-slot gate between distinct slots. -/
def SlotG (p : ℕ × ℕ) : Prop := ∃ q q', p = (wS q, wS q') ∧ q < NR ∧ q' < NR ∧ q ≠ q'

/-! ## Wire ranges -/

/-- Slot wires. -/
def IsSlot (w : ℕ) : Prop := 3542 ≤ w ∧ w < 43619

/-! ## XOR-run helpers -/

/-! ## The gate lists -/

/-- Scatter from the retained slots. -/
def Sg : List (ℕ × ℕ) := (List.range NV).flatMap (scatEl rdS)

/-- Injections. -/
def injEl (T : ℕ) : List (ℕ × ℕ) := tri3.map fun k => (wY T, wS (injS T k))

def Ig : List (ℕ × ℕ) := (List.range NV).flatMap injEl

/-- Copies of the retained slots into the temporaries. -/
def Tg : List (ℕ × ℕ) := (List.range 23).map fun c => (wT c, wS (retS c))

/-- Scatter from the temporaries. -/
def STg : List (ℕ × ℕ) := (List.range NV).flatMap (scatEl wT)

/-- The gates of the stage-one word. -/
def G1 : List (ℕ × ℕ) :=
  Ag ++ (Sg ++ Ig) ++ Ag.reverse ++ Cg ++ (Ag ++ (Tg ++ STg ++ Ig) ++ Ag.reverse) ++ Cg

/-- The gates of the stage-two word. -/
def G2 : List (ℕ × ℕ) :=
  Cg.reverse ++ (Ag ++ (Ig.reverse ++ (Tg ++ STg.reverse)) ++ Ag.reverse) ++ Cg.reverse ++
    (Ag ++ (Ig.reverse ++ Sg.reverse) ++ Ag.reverse)

/-- Target wires. -/
def IsTgt (w : ℕ) : Prop := 1771 ≤ w ∧ w < 3542

/-! ## Read blocks -/

section Reads

variable {M : Type*} [AddCommGroup M]

/-- The effect of a read block: inputs and slots kept, targets receive the reads. -/
def ReadsP (R : List (ℕ × ℕ)) (z z' : ℕ → M) : Prop :=
  (∀ w, w < 1771 ∨ IsSlot w → z' w = z w) ∧ ∀ T < NV, z' (wY T) = z (wY T) + readSum z T

/-- Temporaries hold `0`. -/
def TmpZ (z : ℕ → M) : Prop := ∀ c < 23, z (wT c) = 0

end Reads

/-! ## The sandwich `A · R · A⁻¹` -/

/-! ## The two stages -/

section Stages

variable {M : Type*} [AddCommGroup M] (h2 : ∀ a : M, a + a = 0)

/-- Input part: zero off the inputs. -/
def xPart (u : ℕ → M) : ℕ → M := fun w => if w < 1771 then u w else 0

end Stages

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6BitNBStWD
/-!
# Round six, bit network: the full stage words (definitions) and table checks

`W1F` (stage one) and `W2F` (stage two): the static ops and the generator segments of
`R6BitNBGenP` in order. Stage one: ops `0–3` (all touched wires at code `LOW`), segments `0–9`,
op `8` (`mixI` at `HIGH`), segment `10`. Stage two: the reversed ops `9, 8` (at `HIGH`), segments
`0–9`, the reversed ops `3, …, 0` (at `LOW`).
-/

set_option maxRecDepth 100000

namespace R6Chk.Bit.Loc

noncomputable section

open R6Chk R6Chk.Bit

/-- Stage-one word. -/
def W1F : List LInstr :=
  (mixF fun _ => cLOW) ++ (scat rdS fun _ => cLOW) ++ (injo fun _ => cLOW) ++ (mixI fun _ => cLOW) ++
    (segW1 0 ++ segW1 1 ++ segW1 2 ++ segW1 3 ++ segW1 4 ++ segW1 5 ++ segW1 6 ++ segW1 7 ++
      segW1 8 ++ segW1 9) ++ (mixI fun _ => cHIGH) ++ segW1 10

/-- Stage-two word. -/
def W2F : List LInstr :=
  revI (copyo fun _ => cHIGH) ++ revI (mixI fun _ => cHIGH) ++
    (segW2 0 ++ segW2 1 ++ segW2 2 ++ segW2 3 ++ segW2 4 ++ segW2 5 ++ segW2 6 ++ segW2 7 ++
      segW2 8 ++ segW2 9) ++
    revI (mixI fun _ => cLOW) ++ revI (injo fun _ => cLOW) ++ revI (scat rdS fun _ => cLOW) ++
      revI (mixF fun _ => cLOW)

/-- Number of touched wires. -/
def touchCnt (W : List LInstr) : ℕ := W.foldl (fun a i => Nat.add a i.2.1.length) 0

/-- Code facts of a packed state on the inputs, targets and slots. -/
def sgFacts (t : LT) (fx fy fs : ℕ → ℕ) : Bool :=
  (List.range NV).all (fun i => Nat.beq (pget t (wX i)) (fx i) && Nat.beq (pget t (wY i)) (fy i)) &&
    (List.range NR).all fun q => Nat.beq (pget t (wS q)) (fs q)

/-- All local codes are valid (`< 38286`). -/
def sgValid (t : LT) : Bool := (List.range 43642).all fun w => Nat.blt (pget t w) 38286

end

end R6Chk.Bit.Loc

end

section
-- Source module: Solutions.R6BitNBStW
/-!
# Round six, bit network: the generated chunks of the two stage words

For the stage words `W1F`, `W2F`:
* their gates are the lists `G1`, `G2` of `R6BitNBScalB`;
* every instruction has a valid code, touches local wires (`< NL`) and its gates join distinct
  touched wires;
* the generator, started at the packed states `SG1_0`, `SG2_0`, ends at `SG1_11`, `SG2_10`; all
  its moves are nested (`nestOK`) between valid codes, and the move ranks are counted by the sums
  of the segment counts.

The segments are the kernel checks `seg1_j`, `seg2_j`; the static ops are handled by
`genF_static` with the code facts `sgk*` of the packed states.
-/

set_option maxRecDepth 100000

namespace IntMul.Kappa.R6.Bit

open R6Chk R6Chk.Bit R6Chk.Bit.Loc

/-- Local wires. -/
def NL : ℕ := 43642

/-! ## Gates -/

/-- The gates of a word. -/
def gatesW (W : List LInstr) : List (ℕ × ℕ) := W.flatMap fun i => i.2.2

/-! ## Well-formed instructions -/

/-- A valid code, local touched wires, gates between distinct touched wires. -/
def InstrOK (i : LInstr) : Prop :=
  i.1 < 38286 ∧ (∀ w ∈ i.2.1, w < NL) ∧ ∀ p ∈ i.2.2, p.1 ∈ i.2.1 ∧ p.2 ∈ i.2.1 ∧ p.1 ≠ p.2

def WFw (W : List LInstr) : Prop := ∀ i ∈ W, InstrOK i

/-- Touched wires satisfy `P`, and the instruction code is `c`. -/
def TouchC (P : ℕ → Prop) (c : ℕ → Prop) (W : List LInstr) : Prop := ∀ i ∈ W, c i.1 ∧ ∀ w ∈ i.2.1, P w

/-- Wire classes. -/
def IsS (w : ℕ) : Prop := ∃ q < NR, w = wS q
def IsY (w : ℕ) : Prop := ∃ T < NV, w = wY T
def IsX (w : ℕ) : Prop := ∃ t < NV, w = wX t

/-! ## The generator: validity, ranks, counts -/

/-- Valid codes on the local wires. -/
def ValidOn (f : ℕ → ℕ) : Prop := ∀ w < NL, f w < 38286

/-- Moves between valid codes. -/
def MovesV (cs : List LChunk) : Prop :=
  ∀ ch ∈ cs, ∀ mv ∈ ch.2.1, nestOK mv.2 ch.1 = true ∧ mv.2 < 38286 ∧ ch.1 < 38286

/-- Move ranks. -/
noncomputable def rkC (a b : ℕ) : ℕ := let a1 := dimCF a; let b1 := dimCF b
  cond (Nat.blt a1 b1) (Nat.sub b1 a1) (Nat.sub a1 b1)

noncomputable def mvRanks (cs : List LChunk) : List ℕ := cs.flatMap fun ch => ch.2.1.map fun m => rkC m.2 ch.1

/-! ## Segments -/

/-- A piece of a stage word from packed state `S` to `S'` with rank count `c`. -/
def Seg (S S' c : ℕ) (W : List LInstr) : Prop :=
  WFw W ∧ ∀ f : ℕ → ℕ, (∀ w < 65536, f w = codeOf S w) → ValidOn f →
    (∀ w < 65536, (genF f W).1 w = codeOf S' w) ∧ ValidOn (genF f W).1 ∧ MovesV (genF f W).2 ∧
      cntF (genF f W).2 = c

/-! ## Code facts of the packed states -/

/-! ## The stages -/

/-- Stage-one rank count. -/
def CNs1 : ℕ := CN1_0 + CN1_1 + CN1_2 + CN1_3 + CN1_4 + CN1_5 + CN1_6 + CN1_7 + CN1_8 + CN1_9 + CN1_10

/-- Stage-two rank count. -/
def CNs2 : ℕ := CN2_0 + CN2_1 + CN2_2 + CN2_3 + CN2_4 + CN2_5 + CN2_6 + CN2_7 + CN2_8 + CN2_9

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6BitNBProjB
/-!
# Round six, bit network: projectors of the codes

The codes of the local generator name projectors on `ℚ^23` (`Pc`): `LOW = 0`, `HIGH = 1`,
`PT T = 1 - Pl T` (the hyperplane `B`-orthogonal to triple `T`), `ND n` the `B`-orthogonal projector
onto the span of the triples of node `n` (`Pnd (supG n)`). The dimension records certify both the
dimension of every node span and a common point (centre) of its triples, so `Pnd` is a projector of
rank `dimN n`. A move allowed by `nestOK` is between nested projectors; its difference `Dm` is an
idempotent of rank `rkC` with `Dm + P_old - 2 Dm P_old = P_new`.
-/

set_option maxRecDepth 100000

namespace IntMul.Kappa.R6.Bit.NB

open Matrix Module R6Chk R6Chk.Bit R6Chk.Bit.Loc

/-! ## Dimension records: dimension and centre -/

/-! ## Table lookups -/

/-! ## Arguments of gates -/

/-! ## Orthogonality to a triple -/

/-! ## Ranks of idempotents -/

/-- Nested idempotents: `A ≤ B`. -/
def Le {n : ℕ} (A B : Matrix (Fin n) (Fin n) ℚ) : Prop := B * A = A ∧ A * B = A

/-! ## The code projectors -/

/-- The projector named by a code. -/
noncomputable def Pc (c : ℕ) : Matrix (Fin 23) (Fin 23) ℚ :=
  if c = 0 then 0 else if c = 1 then 1 else if c < 1773 then 1 - Pl (c - 2) else Pnd (supG (c - 1773))

/-! ## Moves -/

/-- The move idempotent between codes `o` and `c`. -/
noncomputable def Dm (o c : ℕ) : Matrix (Fin 23) (Fin 23) ℚ :=
  if dimCF o ≤ dimCF c then Pc c - Pc o else Pc o - Pc c

end IntMul.Kappa.R6.Bit.NB

end

section
-- Source module: Solutions.R6BitNBRed
/-!
# Round six, bit network: reduction mod `N` of good rational matrices

`GoodM N A`: all entries of `A` have denominators coprime to `N`. Good matrices form a ring and
`redM N` is multiplicative and additive on them. Partial swaps over `ℚ` multiply as over
`ZMod N` (`pswQ_mul`), and an edge with rational Bruhat data (`EdgeQ e q`, good factors) has
frame matrix `redM N (pswQ q)` (`edgeMat_eq`).
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Bit

namespace NB

open Matrix AModelFac AModel

variable {l n p : Type*} [Fintype n] [DecidableEq n]

/-- All denominators coprime to `N`. -/
def GoodM (N : ℕ) (A : Matrix l p ℚ) : Prop := ∀ i j, Nat.Coprime (A i j).den N

/-- The good matrix as a matrix over `goodSub N`. -/
def toG (N : ℕ) (A : Matrix n n ℚ) : Matrix n n (goodSub N) := A.map (toGood N)

end NB

end IntMul.Kappa.R6.Bit

end

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

`K A B = S (A ⊗ B) S⁻¹` (`S`, `Sinv` from `flagBasis`). The stage frames are
`Φ₁ b c = pswQ (K (Pc c) (Pl b))` and `Φ₂ a c = pswQ (1 - K (Pl a) (Pc c))`; every edge of the network
is a partial swap `pswQ (K A B)` and carries frames along (identities over `ℚ`).
-/

namespace IntMul.Kappa.R6.Bit.NB

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

abbrev M23 := Matrix (Fin 23) (Fin 23) ℚ

section K

variable (S : Matrix (Fin 529) (Pr 23) ℚ) (Si : Matrix (Pr 23) (Fin 529) ℚ)

/-- The conjugated Kronecker product. -/
def K (A B : M23) : Matrix (Fin 529) (Fin 529) ℚ := S * (A ⊗ₖ B) * Si

variable {S Si}

/-- Stage-one frames. -/
noncomputable def Φ₁ (S : Matrix (Fin 529) (Pr 23) ℚ) (Si : Matrix (Pr 23) (Fin 529) ℚ) (b c : ℕ) :
    QMat2 529 := pswQ (K S Si (Pc c) (Pl b))

/-- Stage-two frames. -/
noncomputable def Φ₂ (S : Matrix (Fin 529) (Pr 23) ℚ) (Si : Matrix (Pr 23) (Fin 529) ℚ) (a c : ℕ) :
    QMat2 529 := pswQ (1 - K S Si (Pl a) (Pc c))

variable (hS : S * Si = 1) (hSi : Si * S = 1)
include hS hSi

end K

end IntMul.Kappa.R6.Bit.NB

end