Round-six κ development, definitions part 20

-- 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_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_M_Defs1
import Definitions.Def_IntMul_Kappa_R6_Defs10
import Definitions.Def_IntMul_Kappa_R6_Defs11
import Definitions.Def_IntMul_Kappa_R6_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs11
import Definitions.Def_IntMul_Kappa_K_Defs12
import Definitions.Def_IntMul_HvdH_M_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs10
import Definitions.Def_IntMul_Kappa_K_Defs13
import Definitions.Def_IntMul_Kappa_K_Defs14
import Definitions.Def_IntMul_Kappa_K_Defs15
import Definitions.Def_IntMul_Kappa_K_Defs9
import Definitions.Def_IntMul_Kappa_K_Defs21
import Definitions.Def_IntMul_Kappa_K_Defs20
import Definitions.Def_IntMul_Kappa_K_Defs31
import Definitions.Def_IntMul_Kappa_K_Defs32
import Definitions.Def_IntMul_Kappa_K_Defs16
import Definitions.Def_IntMul_Kappa_R6_Defs12
import Definitions.Def_IntMul_Kappa_K_Defs3
import Definitions.Def_IntMul_Kappa_K_Defs2
import Definitions.Def_IntMul_Kappa_K_Defs4

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: NLogN.Flat
/-!
# Flat code with jumps, and compilation of structured programs into it

Instructions carry absolute addresses. `ret` with an empty control stack halts.
`exec_flat`: a structured run of cost `c` is `c` flat steps.
-/

namespace NLogN

variable {S P : ℕ}

theorem Steps.one {I : List Sym} {code : ℕ → Instr S} {c c' : Cfg S}
    (h : fstep I code c = some c') : Steps I code c 1 c' := Steps.step h (Steps.refl c')

/-! ## Layout -/

/-! ## A concrete layout -/

end NLogN

end

section
-- Source module: NLogN.TM
/-!
# Running flat code on the platform's Turing machines

Tapes: `0` input, `1` output, `2` control stack (return addresses), `3 + i` stack `i`.
On every stack tape the head rests on the top symbol (on `▷` when empty), so `push` is two
steps, `pop` and tests are one step, and a call is two steps.  Each flat step is at most two
machine steps (`flat_tm`).
-/

namespace NLogN

open IntMul IntMul.Mach

variable {S L : ℕ}

/-! ## Encoding of configurations -/

end NLogN

namespace NLogN

open IntMul IntMul.Mach

variable {S L : ℕ}

/-! ## Partial runs -/

theorem Reach.one {Γ' : Type} [DecidableEq Γ'] {k : ℕ} {st : Γ'} {P : Prog Γ' k}
    {q q' : P.Q} {T : Tapes Γ' k} {w : Fin k → Γ' × Move}
    (h : P.δ q T.read = some (q', w)) : Reach st P q T 1 q' (T.write (fix st T.read w)) :=
  Reach.step h (Reach.refl _ _)

attribute [simp] tst_ne_tin tst_ne_tout tst_ne_tctl tin_ne_tout tin_ne_tctl tout_ne_tctl

/-! ## One flat step -/

end NLogN

end

section
-- Source module: NLogN.SSLoops
/-!
# Generic counted loops over item arrays
-/

namespace NLogN

open IntMul

variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt NS P}

theorem zsz_natCast_le_r6c {j k : ℕ} (h : j ≤ k) : zsz (j : ℤ) ≤ zsz (k : ℤ) :=
  zsz_mono_r6c (by simpa using h)

end NLogN

end

section
-- Source module: Solutions.ButterflyGuard
/-!
# §5.4 An explicit guard-width bound (and the numeric parts of Proposition 14)

1. The constants `E = 64(W+m+1)³`, `B = s+E`, `ν = min{j ≥ 1 : m^j ≥ B}`, `C1 = max{20, ν+3}`,
   `C0 = 128 m B²` for the complex network `m = 10⁶`, `W_c`, `s_c`: `m^10 < B < m^11`, `ν = 11`,
   `C1 = 20`.
2. The depth recurrence `A(e) ≤ s A(e/m) + E`, `A ≤ 8e` at leaves, gives `A ≤ 8 d B^{k+1}
   ≤ 8 B² d^{ν+1}`, and the final chain `8mB²d^{ν+2}+8d+t+9 ≤ … < 128mB²d^{ν+3} ≤ C0 d^{C1}`.
3. Dyadic growth: a value at arithmetic depth `ℓ` (add, sub, halve, negate, multiply by `i`)
   lies in `2^{-(p+ℓ)} ℤ[i]` with modulus `≤ 2^ℓ`; hence `p+Δ` fractional and `Δ+3` integer and
   sign bits represent it exactly.
4. The final truncation `Q_p` toward zero: `|Q_p z| ≤ |z|`, `|Q_p z - z| < √2 · 2^{-p}`.
5. The width bookkeeping of the proof of Proposition 14.
-/

namespace Butterfly

open Complex

/-! ## 1. The constants -/

/-! ## 2. Depth recurrence and the chain -/

/-! ## 3. Dyadic depth invariant -/

lemma DyGood.sub {p ℓ ℓ' : ℕ} {z w : ℂ} (hz : DyGood p ℓ z) (hw : DyGood p ℓ' w) :
    DyGood p (max ℓ ℓ' + 1) (z - w) := by
  rw [sub_eq_add_neg]; exact hz.add hw.neg

/-! ## 4. Final truncation toward zero -/

/-! ## 5. Width bookkeeping in the proof of Proposition 14 -/

end Butterfly

end

section
-- Source module: Solutions.KILBase
/-!
# KIL base: register programs on "managed" stacks

`encK s f` is the state `s` with the list of integers `f j` pushed on top of every stack `j`
(`f j = []` for unmanaged stacks).  All programs of the KIL files are specified on such states;
updates are `Function.update`s of `f`, which keeps the bookkeeping small.

`Sp p s t c` : the register program `p` is executable from `s` (`RS.ok`), ends in `t`, and costs
at most `c`.  `Sp.irun` turns it into an `IRuns` of the compiled item-language code.
-/

set_option linter.unusedSimpArgs false

namespace NLogN

open IntMul RS

namespace KIL

/-! ## Elementary statements -/

/-! ## Moving integers between stacks -/

/-! ## Counted loops through a family of managed states -/

/-! ## Expression side conditions on managed states -/

theorem zsz_nat_le {a b : ℕ} (h : a ≤ b) : zsz (a : ℤ) ≤ zsz (b : ℤ) := zsz_natCast_le_r6c h

end KIL

end NLogN

end

section
-- Source module: Solutions.KIL3Ops
/-!
# KIL3: generic stack operations on managed states

Element-wise loops used by the one-stack network: `dupK` (copy `n` integers to two stacks),
`dropK` (discard `n` integers), `zeroK` (push `n` zeros), `zipK` (pointwise addition mod 2 of two
stacks).  All are stated on managed states `encK s f`.
-/

set_option linter.unusedSimpArgs false

namespace NLogN.KIL

open IntMul RS AModel

/-! ## Dropping `n` integers -/

/-! ## Pushing `n` zeros -/

/-! ## Pointwise addition mod 2 -/

theorem one_le_of_zsz4 {Bb : ℕ} (hB : zsz ((2 * 2 : ℕ) : ℤ) ≤ Bb) : 1 ≤ Bb := by
  have := zsz_natCast_le' (show 1 ≤ 2 * 2 by norm_num)
  simp only [Nat.cast_one, zsz_one_r6c] at this
  omega

/-! ## IStmt forms -/

end NLogN.KIL

end

section
-- Source module: Solutions.KIL3Tab
/-!
# KIL3: a table of `W` streams on one stack

The `W` streams of the network are kept on stack `0`, one after the other (stream `0` on top):
`tab W F = F 0 ++ F 1 ++ ⋯ ++ F (W − 1)`, every stream of the same length `v`.

Operations (all `O(W · v)` item moves, plus the cost of the applied code):

* `applyC v w code`: run `code` (any stack-`0` program) on stream `w` in place
  (`applyC_runs`): the streams before `w` are parked on stack `15` and moved back.
* `copyC v w`: push a reversed copy of stream `w` on stack `16` (`copyC_sp`).
* `buildC v l`: push on stack `20` the (reversed) pointwise sum mod 2 of the streams `l`.
* `rebuildC W v T`: replace the table by the streams `w ↦ Σ_{w' ∈ T w} F w'` (`rebuildC_sp`).

Scratch stacks: `15` (park), `16` (copy), `17` (temp), `19` (zip out), `20` (new table),
`21` (loop counter).
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open IntMul RS AModel

/-! ## Tables -/

/-! ## Moves with literal counts -/

/-! ## Applying a stream code in place -/

/-! ## Cost unit -/

/-! ## Copying a stream -/

theorem TabB.one {W v Bb : ℕ} (h : TabB W v Bb) : 1 ≤ Bb := one_le_of_zsz4 h.four

/-! ## Accumulating a stream on stack `20` -/

/-! ## Building a summed stream, rebuilding the table -/

end NLogN.KIL

end

section
-- Source module: Solutions.KIL4StepH
/-!
# KIL4: the uniform level step `stepU`

A *shift template* `TSh m` fixes the active field `i`, the fraction `k/d` of the unit, its sign and
the rational controls `cs j = (p_j, q_j)` (control `j` is `p_j · q_j⁻¹ mod N`).  The template does
not mention the modulus `N`, the level or any volume.

`stepU m rX T` is one fixed program.  It reads

* `N` from `sQQ` (and `-N` from `sNQ`),
* `vol (P :: L :: A)` from the register `rX` (`rXs` or `rXb`),
* `vol B` from `rVB` and `vol Cs` from `rVC`,

builds the size parameters and the collapsed offset-table stages, computes every control
`p_j q_j⁻¹ mod N` at run time (`ctrlE`), and runs the uniform shift body.

`stepU_spec`: on the level layout `(hdLayout A B Cs m N).cons2 P L` it computes
`(T.eval N).arr`, the array action of the shift step the template denotes.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open IntMul RS AModel AModelL12

/-! ## Push-list hygiene -/

theorem RdOK.lt {r : Fin HS} (h : RdOK r) : r.val < 56 := by
  rcases h with h | h
  · rw [h]; decide
  · exact h.2

theorem zsz_le_of {v : ℤ} {M Bb : ℕ} (h0 : 0 ≤ v) (h : v ≤ M) (hM : zsz (M : ℤ) ≤ Bb) :
    zsz v ≤ Bb :=
  le_trans (zsz_mono_r6c (by rw [Int.natAbs_natCast]; omega)) hM

/-! ## Templates -/

variable {m : ℕ}

end NLogN.KIL

end

section
-- Source module: Solutions.KIL5Tab
/-!
# KIL5: the stream table with run-time stream length

KIL3's table operations (`applyC`, `copyC`, `accC`, `buildC`, `rebuildC`, KIL3Tab) carry the
stream length `v` and the offsets `w · v` as literals.  Here the counts are read from registers:

* `rV` (`42`) holds `v`, `rWV` (`43`) holds `W · v`;
* the offset `w · v` (`w < W` a fixed wire) is computed into the temporary register `rT` (`44`)
  by one multiplication (`push rT (w · rV)`) and popped afterwards.

The element loops `dupK`, `zipK`, `zeroK`, `dropK` with register counts are obtained from the
literal ones by the literal-to-register simulation (`Sp.sim`, KIL4Sim).

`applyCU_runs` is relative to an invariant: the stream code only has to be correct on states
`t` with `Inv G0 t` (every protected stack `r ≥ 22`, `r ≠ 44`, holds `G0 r`).  This is what the
uniform procedure needs: its child calls read the descriptor and the level registers from these
stacks.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false

namespace NLogN.KIL

open IntMul RS AModel

/-! ## Registers and the invariant -/

theorem RegS.gV {s : IState HS} {f : Fin HS → List ℤ} {W v : ℕ} (h : RegS s f W v) :
    ∃ L, (encK s f).G rV = .int (v : ℤ) :: L := by
  obtain ⟨L, hL⟩ := h.sV; exact ⟨L, by simp [h.fV, hL]⟩

/-! ## Moves and loops with register counts -/

/-! ## Applying a stream code in place -/

/-! ## Copying, accumulating and rebuilding with register counts -/

end NLogN.KIL

end

section
-- Source module: Solutions.KIL6Reg
/-!
# KIL6: register files

`regState F v D`: the managed state `F` with the natural `v i` pushed on every register
`i ∈ D`.  Assignment lists `asgL L` (each an `NE` expression) act on the valuation `v` only
(`Sp.asgs`); counted loops of assignment lists iterate the valuation map (`Sp.repA`).  `pushZs` /
`popDs` create and remove the register file.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KIL

open IntMul RS AModel AModelL12

theorem RegsIn.lt {F : Fin HS → List ℤ} {v : Fin HS → ℕ} {D : List (Fin HS)} {e : NE}
    (h : RegsIn F v D e) : e.RegsLt := fun j hj => (h j hj).1

/-! ## Assignment lists -/

/-! ## Creating and removing the file -/

end NLogN.KIL

end

section
-- Source module: Solutions.KFCFwdMain
/-!
# KFC: the self-contained fine-cost forward field move `fwdF`

`fwdF_spec`: on `t` with `ints xs ++ R` on stack `0` and `P, q, M, B` on stacks `1 … 4`,
`fwdF` ends in `t.upd 0 (ints (pull [P,q,M,B] [P,M,q,B] gS 0 xs) ++ R)` (all scratch stacks
restored) with cost `≤ cFwdF P q M B w = (2q+16)·kap w·V + cUL P + cUL q + cUL M + cUL B + 1000`,
`V = P·q·M·B`, `w` a bound on the bit size of the entries of `xs` only.
-/

set_option linter.unusedSimpArgs false
set_option linter.unnecessarySeqFocus false
set_option maxRecDepth 20000

namespace NLogN

open IntMul AModel

namespace KFC

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

/-! ## Prologue / epilogue of a unary counter pair -/

/-! ## The core: blocks, then copy the output back -/

/-! ## The program -/

theorem zsz_nat_le (n : ℕ) : zsz (n : ℤ) ≤ n :=
  zsz_le_of_lt (by simpa using Nat.lt_two_pow_self)

end KFC

end NLogN

end

section
-- Source module: Solutions.KFBGauss
/-!
# KFB: Gaussian-integer data on item stacks, linear-combination expressions

* `GI = ℤ × ℤ` (Gaussian integer `a + b i`), stored on a stack as the two items `a, b`
  (`gflat`).  `toC` is the embedding into `ℂ`; `gmul` the product.
* `lcE l`: the register expression `Σ c_t · top(r_t)` for coefficients `c_t ∈ {-1, 0, 1}`, built
  only from `add`, `neg`, `reg`, `lit` (a linear expression: cost `O(size · (B + 2))`).
  `lcE_eval`, `lcE_bnd` (all partial sums of `n ≤ 2^e` terms of size `≤ w` have size `≤ w + e`).
* `FSp.mvN`: the fine counted move with the count read from a register and its loop overhead
  bounded by the count itself (`≤ N (250 w + 1600) + 2000`, no `Bb`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFB

open IntMul RS AModel KIL KFD Complex

/-! ## Gaussian integers -/

theorem GB.sub {w : ℕ} {zs zs' : List GI} (h : GB w zs) (hs : ∀ z ∈ zs', z ∈ zs) : GB w zs' :=
  fun z hz => h z (hs z hz)

/-! ## Linear-combination expressions -/

/-! ## Fine moves with the loop overhead bounded by the count -/

end NLogN.KFB

end

section
-- Source module: Solutions.KFBQop
/-!
# KFB: the two-stream pass `qop` (fine cost)

On a Gaussian array viewed as consecutive blocks `[u ‖ v]` of two streams of `B1` entries each,
`qop Ms` applies the small `2 × 2` Gaussian matrix `M_p = Ms[p mod L]` (`L = |Ms|`) to block `p`:
`(u, v) ↦ (M₀₀ u + M₀₁ v, M₁₀ u + M₁₁ v)` entrywise.  With a single matrix this is a
selected-bit kernel on a field `[2]` (the `C` kernel (25) scaled by 2, a phase on the selected
half, a sign); with the period `[1, X]` it is a CNOT whose control is the field just before.

Per block: one move of the block to a scratch stack (reversal), the two streams distributed to
four register stacks (real/imaginary parts), one zip loop computing the outputs with linear
register expressions (`lcE`), the second output stream moved back in order.  Every entry is
touched `O(1)` times; loop counters are unary (`fcode`) with overhead linear in the counts.

Stacks: data `0`; scratch `qT = 33`, output accumulator `qA = 34`, `qO = 35`; stream registers
`36 … 39`; counters `30, 31`; counts `48 … 52` (`G`, `B1`, `2B1`, `4B1`, total items).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFB

open IntMul RS AModel KIL KFD

/-! ## Pushing a linear combination -/

/-! ## The zip loop -/

/-! ## One block -/

theorem Cnt.congr {s : IState HS} {f g : Fin HS → List ℤ} {B1 : ℕ} (h : Cnt s f B1)
    (h1 : g rB = f rB) (h2 : g rB2 = f rB2) (h3 : g rB4 = f rB4) : Cnt s g B1 :=
  ⟨by simp only [encK_G, h1]; exact h.b, by simp only [encK_G, h2]; exact h.b2,
    by simp only [encK_G, h3]; exact h.b4⟩

/-! ## A group of blocks, and the whole pass -/

/-! ## Fine compilability -/

end NLogN.KFB

end

section
-- Source module: Solutions.KFGPair
/-!
# KFG: a pointwise `2 × 2` scaled operation on two arbitrary role streams

On the data stack `pre ++ u ++ gap ++ v ++ rest` (Gaussian streams, `|u| = |v| = L`),
`pairP M` replaces `(u, v)` by `(M₀₀ u + M₀₁ v, M₁₀ u + M₁₁ v)` entrywise, with scaled
coefficients `c · 2^d`.  The prefix and the gap are parked on `qP`, `qQ`; the two streams are
distributed to the four register stacks and zipped (`zipRS`); the outputs are moved back.  Every
entry is touched `O(1)` times; the loop counters are unary (`fcode`).

* `pairP_fsp`: the program with its counts in registers (`rB = L`, `rB2 = 2L`, `rP = 2|pre|`,
  `rQ = 2|gap|`).
* `pairW M L i j`: the self-contained wrapper on roles `i < j` of a role-major array with role
  length `L` (`pairW_fsp`, list semantics `pairL`, `getD_pairL`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFG

open IntMul RS AModel KIL KFD KFB Complex

theorem PCnt.congr {s : IState HS} {f g : Fin HS → List ℤ} {L P Q : ℕ} (h : PCnt s f L P Q)
    (h1 : g rB = f rB) (h2 : g rB2 = f rB2) (h3 : g rP = f rP) (h4 : g rQ = f rQ) :
    PCnt s g L P Q :=
  ⟨by simp only [encK_G, h1]; exact h.b, by simp only [encK_G, h2]; exact h.b2,
    by simp only [encK_G, h3]; exact h.p, by simp only [encK_G, h4]; exact h.q⟩

end NLogN.KFG

end

section
-- Source module: Solutions.NetLabels
open Matrix Module

set_option linter.unusedSectionVars false

namespace NetLabels

variable {K : Type*} [Field K] {ι : Type*} [Fintype ι] [DecidableEq ι]

/-! ### (c) The bit-network form `I − J/9` on `K^h`. -/

/-! ### (d) Tensor products of labels (Kronecker Gram matrices). -/

/-- For an idempotent matrix, `rank = trace`. -/
theorem rank_eq_trace_of_idem (P : Matrix ι ι K) (hP : P * P = P) : (P.rank : K) = P.trace := by
  have hf : IsIdempotentElem (Matrix.toLin' P) := by
    unfold IsIdempotentElem
    rw [Module.End.mul_eq_comp, ← Matrix.toLin'_mul, hP]
  have := ((LinearMap.isProj_range_iff_isIdempotentElem _).2 hf).trace
  rw [Matrix.trace_toLin'_eq] at this
  rw [this]
  rfl

end NetLabels

end

section
-- Source module: Solutions.NetProp7Alg
/-!
# Prop. 7, part 2: the label algebra

The gate labels of table (6) are projections `P_U` onto tensor subspaces of `F^{⊗3}`,
`F = ℚ^h` with the form `G = I − J/9`. We work directly with their matrices:

* `piM S = ½ t_S (G t_S)ᵀ` is the `G`-orthogonal projection onto the triple line `⟨t_S⟩`
  (`piM_idem`, `trace_piM = 1`, and `piM S * piM T = 0` for neighbouring triples);
* in stage `j` (0-indexed) for the bank with fixed triples `S₁, S₂`, the projections
  `αM j` onto `P ⊗ F ⊗ Q`, `AM j` onto `A ⊗ F ⊗ Q` and `τM j t` onto
  `F^{⊗ j} ⊗ ⟨t⟩ ⊗ F^{⊗(2-j)}` are Kronecker products (`kr3`);
  `B ⊗ F ⊗ Q` has projection `AM − αM`.

The abstract relations (`SRel`) between `α, A, τ` give the rank of every edge difference of
table "Lemma 6" through `rank = trace` for idempotents. The per-wire chain identities
(`chainX`, `chainX0`, `chainY`, `chainC`, `chainS`) are the content of Lemma 6.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace NetProp7

open Matrix Finset NetLabels
open scoped Kronecker

/-! ## 1. Idempotent algebra -/

section Ring

variable {R : Type*} [Ring R]

lemma idem_one_sub {X : R} (hX : X * X = X) : (1 - X) * (1 - X) = 1 - X := by
  simp only [sub_mul, mul_sub, one_mul, mul_one, hX, sub_self, sub_zero]

lemma idem_sub {X Y : R} (hX : X * X = X) (hY : Y * Y = Y) (h1 : X * Y = Y) (h2 : Y * X = Y) :
    (X - Y) * (X - Y) = X - Y := by
  simp only [sub_mul, mul_sub, hX, hY, h1, h2, sub_self, sub_zero]

end Ring

/-! ## 2. Rank of idempotents -/

section Rank

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

lemma rk_idem {E : Matrix n n ℚ} (hE : E * E = E) : rk E = trace E :=
  rank_eq_trace_of_idem E hE

lemma rank_smul_ne {E : Matrix n n ℚ} {c : ℚ} (hc : c ≠ 0) : (c • E).rank = E.rank := by
  have : c • E = E * (c • (1 : Matrix n n ℚ)) := by rw [Matrix.mul_smul, mul_one]
  rw [this, rank_mul_eq_left_of_det_ne_zero]
  rw [det_smul, det_one, mul_one]
  exact pow_ne_zero _ hc

lemma rk_neg (E : Matrix n n ℚ) : rk (-E) = rk E := by
  unfold rk
  rw [show -E = (-1 : ℚ) • E by simp, rank_smul_ne (by norm_num)]

end Rank

/-! ## 3. Abstract stage relations and the edge ranks of Lemma 6 -/

section Stage

variable {n : Type*} [Fintype n] [DecidableEq n] {ι : Type*}

variable {α A : Matrix n n ℚ} {τ : ι → Matrix n n ℚ} {Nb : ι → ι → Prop} {h a : ℚ}

namespace SRel

variable (S : SRel α A τ Nb h a)
include S

lemma ββ : (A - α) * (A - α) = A - α := idem_sub S.AA S.αα S.Aα S.αA

lemma rk_β : rk (A - α) = a * h - h := by
  rw [rk_idem S.ββ, trace_sub, S.trA, S.trα]

lemma rk_α : rk α = h := by rw [rk_idem S.αα, S.trα]

lemma rk_one_sub_A : rk (1 - A) = Fintype.card n - a * h := by
  rw [rk_idem (idem_one_sub S.AA), trace_sub, trace_one, S.trA]

end SRel

namespace SRel

variable (S : SRel α A τ Nb h a)
include S

/-- **Central wire**: source `0`, gates at times 1, 3, 4, 6, sink `1`; total `m + 2h`. -/
lemma chainC (z : Matrix n n ℚ) :
    rk (labK α A z 1 - 0) + (rk (labK α A z 3 - labK α A z 1) +
      (rk (labK α A z 4 - labK α A z 3) + (rk (labK α A z 6 - labK α A z 4) +
        rk (1 - labK α A z 6)))) = Fintype.card n + 2 * h := by
  simp only [labK]
  rw [sub_zero, sub_sub_cancel, show A - α - A = -α by abel, rk_neg, S.rk_β, S.rk_α,
    S.rk_one_sub_A]
  ring

end SRel

end Stage

/-! ## 4. The concrete projections -/

section Concrete

variable {h : ℕ}

variable {T : Type*} (ind : T → Finset (Fin h))

/-! Stage boundaries (§3.3: the outgoing labels of stage `j` are the incoming labels of stage
`j + 1`), and the terminal labels. Here `S₁, S₂, S₃` are the triples of `a`. -/

end Concrete

end NetProp7

end

section
-- Source module: Solutions.KFLAddr
/-!
# KFL §17: `permRecs (rowAddAddr …)` as a triple map on the bit array

The Gaussian records (`R` entries, `2 (w+1)` bits per entry after `toBitsI`) of the rectangle
`rect N0 N1 N2 N3 L` form the bit array of the geometry `geoB` (`Q = 2^L`, `B = 2 R (w+1)`).
`bits_permRecs`: converting `permRecs rect (rowAddAddr px py) R zs` to bits gives
`rixT (geoB …) (Fpp px py)` of the bits of `zs`, where `Fpp px py` replaces slot `py` by
`y ⊕ (x ∧ selM f)` (`x` = slot `px`).  `Fpp_conj`: `Fpp px py` is the canonical row addition
`RAc` conjugated by at most two slot swaps.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFL

open IntMul RS KIL KFD KFB KFH AModel Butterfly

/-! ## Chunks of a list -/

/-! ## The bit records -/

/-! ## The geometry of the bit array -/

section Geom

variable {N0 N1 N2 N3 L R w : ℕ}

theorem geoB_pos (h0 : 1 ≤ N0) (h1 : 1 ≤ N1) (h2 : 1 ≤ N2) (h3 : 1 ≤ N3) (hR : 1 ≤ R) :
    (geoB N0 N1 N2 N3 L R w).Pos :=
  ⟨by simp [geoB], h0, h1, h2, h3, by simp only [geoB]; positivity⟩

end Geom

/-! ## The slot row addition as a triple map -/

/-! ## Records permuted by `rowAddAddr`, in bits -/

/-! ## Conjugation by slot swaps -/

end NLogN.KFL

end

section
-- Source module: Solutions.KFWSub
/-!
# KFW: literals read from registers (the uniformity meta-theorem for register programs)

A uniform register program `U` reads its run-time parameters from registers (tops of stacks).
`RS.sub σ U` replaces each register `i` with `σ i = some v` by the literal `v`; the result is
the (non-uniform) program with baked-in literals, for which a spec is usually already proved.

**`FSp.of_sub`**: if `FSp (U.sub σ) s t c`, the registers of `σ` hold their values in `s`
(`Agree σ s`) and `U` never writes them, then `FSp U s t (400 c)`.  Also `fok_of_sub`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFW

open IntMul RS KFD

theorem Agree.top {σ : Fin HS → Option ℤ} {s : IState HS} (h : Agree σ s) {i : Fin HS} {v : ℤ}
    (hi : σ i = some v) : s.top i = v := by
  obtain ⟨L, hL⟩ := h i v hi; exact IState.top_eq_r6c hL

theorem Agree.isInt {σ : Fin HS → Option ℤ} {s : IState HS} (h : Agree σ s) {i : Fin HS} {v : ℤ}
    (hi : σ i = some v) : s.IsInt i := by
  obtain ⟨L, hL⟩ := h i v hi; exact ⟨L, by rw [hL, IState.top_eq_r6c hL]⟩

section ExLemmas

variable (σ : Fin HS → Option ℤ) {s : IState HS}

theorem Ex.eval_sub (hs : Agree σ s) : ∀ e : Ex HS, (Ex.sub σ e).eval s = e.eval s
  | .reg i => by
    unfold Ex.sub
    rcases h : σ i with _ | v
    · rfl
    · simp only [Ex.eval]; exact (hs.top h).symm
  | .lit c => rfl
  | .add a b | .mul a b | .shl a b | .quo a b | .rem a b | .ndiv a b | .nmod a b => by
    simp only [Ex.sub, Ex.eval, Ex.eval_sub hs a, Ex.eval_sub hs b]
  | .neg a | .pow2 a => by simp only [Ex.sub, Ex.eval, Ex.eval_sub hs a]
  | .sel c x y => by simp only [Ex.sub, Ex.eval, Ex.eval_sub hs c, Ex.eval_sub hs x, Ex.eval_sub hs y]

end ExLemmas

end NLogN.KFW

end

section
-- Source module: Solutions.KFWBase
/-!
# KFW: header refinement, uniform leaves, parameters in the background

* `HRef p p' X`: `p'` is `p` with some (non-loop) pushes of literals `v` replaced by closed
  expressions of value `v`; `HRef.fsp`: `FSp p s t c → FSp p' s t (c + X)`.
* `RS.sub_id`: substituting registers a program never touches changes nothing.
* `FSp.uni`: `FSp O s t c`, `HRef O (U.sub σ) X`, the registers of `σ` hold their values and are
  not written ⇒ `FSp U s t (400 (c + X))` (and `fok U` from `fok O`).
* `encK_pushSt`, `agree_pushSt`, **`leafPush`**: a uniform leaf `withPushI pl (fcode U)` from the
  non-uniform spec of `O` on the background with the pushed parameters.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false

namespace NLogN.KFW

open IntMul RS KFD KIL

/-! ## Header refinement -/

/-- Literal pushes of the same value. -/
theorem HRef.lit (i : Fin HS) (v : ℤ) : HRef (.push i (.lit v)) (.push i (.lit v)) 0 := .refl _

/-! ## Substitution of untouched registers -/

/-! ## Uniform register programs -/

/-! ## Pushed parameters in the background -/

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

end NLogN.KFW

end

section
-- Source module: Solutions.KFWWrap
/-!
# KFW: a uniform program on one role

`wrapQ W w ρ ρE U`: swap role `w` to the front, run `U` on the first segment, level the other
roles by `2^e` (the shift read from `ρE`), swap back.  The role length is read from `ρ`.

**`rImplQ_onRole`**: the uniform analogue of `KFN.rImplI_onRole`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex P8Lift Butterfly

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

theorem WReg.zero {σ : Fin HS → Option ℤ} {ρ ρE : Fin HS} {L e : ℕ} (h : WReg σ ρ ρE L e) :
    σ 0 = none := h.off 0 (by decide)

variable {W m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ]
variable {Q : IState HS → Prop} {lo hi : ℕ}

end NLogN.KFW

end

section
-- Source module: Solutions.KFWFrame
/-!
# KFW: frames of run-time registers around uniform programs

* `σPush σ l`: the register assignment after pushing the values `l` (last push wins);
  `agree_pushSt'`: pushing keeps the background in agreement.
* `PushSeq σ pl vl c`: the pushes `pl` (expressions evaluated **sequentially**, each under the
  registers after the earlier pushes) push the values `vl`, at cost `≤ c`; `Sp.pushSeq`.
* **`sImplQ_push`**: push a frame, run a uniform `SImplQ` program on the extended background, pop.
* `sImplQ_call`, `sImplQ_ite`: procedure calls and register tests.
* `SImplQ.mono_dw`, `sImplQ_subOp`, `sImplQ_equiv`, `sImplQ_skip`: bookkeeping.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex P8Lift Butterfly

/-! ## Register assignments after pushes -/

theorem Agree.of_ext {σ σ' : Fin HS → Option ℤ} {s : IState HS} (h : Agree σ' s)
    (he : SExt σ σ') : Agree σ s := fun i v hv => h i v (he i v hv)

/-! ## Sequential pushes -/

theorem PushSeq.lt : ∀ {σ : Fin HS → Option ℤ} {pl : List (Fin HS × Ex HS)}
    {vl : List (Fin HS × ℤ)} {c : ℕ}, PushSeq σ pl vl c → ∀ p ∈ vl, p.1.val < 56
  | _, [], [], _, _, _, hp => by simp at hp
  | _, [], _ :: _, _, h, _, _ => absurd h (by simp [PushSeq])
  | _, _ :: _, [], _, h, _, _ => absurd h (by simp [PushSeq])
  | _, (i, e) :: l, (j, v) :: vl, _, h, p, hp => by
    obtain ⟨rfl, hi, _, _, _, _, _, hrest⟩ := h
    rcases List.mem_cons.1 hp with rfl | hp
    · exact hi
    · exact PushSeq.lt hrest p hp

/-! ## Frames around uniform programs -/

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
variable {Q : IState HS → Prop} {lo hi : ℕ}
variable {ι : Type*} [Fintype ι] [DecidableEq ι] {r : ℕ} {st : ι → ℕ} {n : ℕ}

end NLogN.KFW

end

section
-- Source module: Solutions.KFWStep1
/-!
# KFW: the uniform local steps of a node (gate, permutation)

A node of level `k + 1` (child level `k`) acts on `W` role streams of `n = Bn 2^t S₀` records,
bits `Fin mC × Fin (mC^k)` at the positions `posR K e k`, strides `stN K e k S₀`.
Its registers are described by **`NodeR σ K t S0 r H k e B Bn`** (the level frame and the node
frame `nodeVals`, everything `< 56`, the gate and phase scratch registers free).

* `stepQ_gate`: a gate of atoms (`gateU`), via `KFN.rImpl_gate` and `gatePG_href`;
* `stepQ_perm`: a role permutation (`swapsG`), via `KFN.rImpl_perm` and `swapsG_href`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex Butterfly

theorem sclean_of_lt {σ : Fin HS → Option ℤ} (h : ∀ i v, σ i = some v → i.val < 56) :
    SClean σ := by
  intro i hi hz
  obtain ⟨v, hv⟩ := Option.isSome_iff_exists.1 hi
  have := h i v hv
  simp only [zX, ExSt.all, List.mem_cons, List.not_mem_nil, or_false] at hz
  rcases hz with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> exact absurd this (by decide)

theorem NodeR.cl {σ : Fin HS → Option ℤ} {K t S0 r H k e B Bn : ℕ}
    (h : NodeR σ K t S0 r H k e B Bn) : SClean σ := sclean_of_lt h.lt

theorem NodeR.zero {σ : Fin HS → Option ℤ} {K t S0 r H k e B Bn : ℕ}
    (h : NodeR σ K t S0 r H k e B Bn) : σ 0 = none := h.off 0 (by decide)

end NLogN.KFW

end

section
-- Source module: Solutions.KFWStep2
/-!
# KFW: expressions over a register assignment, and the uniform phase step

* `ExV σ e v B`: on every background agreeing with `σ`, `e` is defined, evaluates to `v`, and
  all its values have at most `B` bits (constructors `ExV.reg`, `ExV.lit`, `ExV.add`, …);
  `ExC σ e v c`: the same with cost `≤ c`.  `pushSeq_cons`, `pushSeq_nil`: building `PushSeq`.
* **`stepQ_phase`**: a phase step `phase w k₀ k₁ a` on the node roles (`phC'`), via
  `rImplQ_onRole`, `sImplQ_push` (the constant `u mod 4` on `wU`), `sImplQ_phase` and
  `epsOK_tab`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex Butterfly

/-! ## Expressions over a register assignment -/

namespace ExV

variable {σ : Fin HS → Option ℤ} {B : ℕ}

theorem reg {i : Fin HS} {v : ℤ} (h : σ i = some v) (hB : zsz v ≤ B) : ExV σ (.reg i) v B :=
  fun t ht => ⟨ht.isInt h, ht.top h, by simp only [Ex.Bnd]; rw [ht.top h]; exact hB⟩

theorem lit {c : ℤ} (hB : zsz c ≤ B) : ExV σ (.lit c) c B := fun t _ => ⟨trivial, rfl, hB⟩

theorem add {a b : Ex HS} {x y : ℤ} (ha : ExV σ a x B) (hb : ExV σ b y B)
    (h : zsz (x + y) ≤ B) : ExV σ (.add a b) (x + y) B := fun t ht => by
  obtain ⟨a1, a2, a3⟩ := ha t ht
  obtain ⟨b1, b2, b3⟩ := hb t ht
  exact ⟨⟨a1, b1⟩, by simp only [Ex.eval, a2, b2], a3, b3, by rw [a2, b2]; exact h⟩

theorem mul {a b : Ex HS} {x y : ℤ} (ha : ExV σ a x B) (hb : ExV σ b y B)
    (h : zsz (x * y) ≤ B) : ExV σ (.mul a b) (x * y) B := fun t ht => by
  obtain ⟨a1, a2, a3⟩ := ha t ht
  obtain ⟨b1, b2, b3⟩ := hb t ht
  exact ⟨⟨a1, b1⟩, by simp only [Ex.eval, a2, b2], a3, b3, by rw [a2, b2]; exact h⟩

theorem neg {a : Ex HS} {x : ℤ} (ha : ExV σ a x B) : ExV σ (.neg a) (-x) B := fun t ht => by
  obtain ⟨a1, a2, a3⟩ := ha t ht
  exact ⟨a1, by simp only [Ex.eval, a2], a3⟩

theorem ndiv {a b : Ex HS} {x y : ℤ} (ha : ExV σ a x B) (hb : ExV σ b y B) (hx : 0 ≤ x)
    (hy : 0 < y) (h : zsz (x / y) ≤ B) : ExV σ (.ndiv a b) (x / y) B := fun t ht => by
  obtain ⟨a1, a2, a3⟩ := ha t ht
  obtain ⟨b1, b2, b3⟩ := hb t ht
  exact ⟨⟨a1, b1, by rw [a2]; exact hx, by rw [b2]; exact hy⟩, by simp only [Ex.eval, a2, b2],
    a3, b3, by rw [a2, b2]; exact h⟩

theorem nmod {a b : Ex HS} {x y : ℤ} (ha : ExV σ a x B) (hb : ExV σ b y B) (hx : 0 ≤ x)
    (hy : 0 < y) (h : zsz (x % y) ≤ B) : ExV σ (.nmod a b) (x % y) B := fun t ht => by
  obtain ⟨a1, a2, a3⟩ := ha t ht
  obtain ⟨b1, b2, b3⟩ := hb t ht
  exact ⟨⟨a1, b1, by rw [a2]; exact hx, by rw [b2]; exact hy⟩, by simp only [Ex.eval, a2, b2],
    a3, b3, by rw [a2, b2]; exact h⟩

theorem cost {e : Ex HS} {x : ℤ} (h : ExV σ e x B) : ExC σ e x (e.size * 10 ^ 7 * (B + 2) ^ 2) :=
  fun t ht => let ⟨a, b, c⟩ := h t ht; ⟨a, b, Ex.cost_le_r6c t B e c⟩

theorem ext {e : Ex HS} {x : ℤ} {σ' : Fin HS → Option ℤ} (h : ExV σ e x B) (hs : SExt σ σ') :
    ExV σ' e x B := fun t ht => h t (ht.of_ext hs)

end ExV

/-- `2^x` with a large exponent: the cost is linear in `x`. -/
theorem ExC.pow2 {σ : Fin HS → Option ℤ} {a : Ex HS} {x : ℤ} {B : ℕ} (ha : ExV σ a x B)
    (hx : 0 ≤ x) :
    ExC σ (.pow2 a) (2 ^ x.toNat) (a.size * 10 ^ 7 * (B + 2) ^ 2 + 2 * moveCost B +
      pow2Cost x.toNat + 2 * B + 100) := fun t ht => by
  obtain ⟨a1, a2, a3⟩ := ha t ht
  have c := Ex.cost_le_r6c t B a a3
  have z := Ex.zsz_eval_le t B a a3
  rw [a2] at z
  refine ⟨⟨a1, by rw [a2]; exact hx⟩, by simp only [Ex.eval, a2], ?_⟩
  simp only [Ex.cost, a2]
  unfold moveCost at *
  nlinarith

/-! ## The phase step -/

end NLogN.KFW

end

section
-- Source module: Solutions.KFWStep5
/-!
# KFW: the `±1` role diagonal step, and the node frame

* `posR_inj` (through `eqvL : Fin mC × Fin (mC^k) ≃ Fin (mC^{k+1})`), `slaws_node`.
* **`stepQ_fixG`**: a `±1` role diagonal as the phase steps `negSteps`.
* `nodeVL`, `σNode`: the node frame; **`nodeR_of_levR`**: the node frame over a level frame of
  level `k + 1` satisfies `NodeR`; **`pushSeq_node`**: `nodePush` pushes it (cost `cNodeF`).
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex Butterfly

theorem ExV.pow2 {σ : Fin HS → Option ℤ} {a : Ex HS} {x : ℤ} {B : ℕ} (ha : ExV σ a x B)
    (hx : 0 ≤ x) (hB : x.toNat + 1 ≤ B) : ExV σ (.pow2 a) (2 ^ x.toNat) B := fun t ht => by
  obtain ⟨a1, a2, a3⟩ := ha t ht
  exact ⟨⟨a1, by rw [a2]; exact hx⟩, by simp only [Ex.eval, a2], a3, by rw [a2]; exact hB⟩

/-! ## The node frame -/

end NLogN.KFW

end

section
-- Source module: Solutions.KFWLeaf
/-!
# KFW: substituted pushes and the uniform leaf (level `0`)

* `Ex.okBnd_sub`, `Ex.regs_sub_none`, `Ex.size_sub`, `ExV.sub`: literal substitution keeps
  definedness, values and bit bounds.
* **`href_sub_push`**: a push of an expression whose registers are all bound by `σ` is, after
  substitution, a header refinement of the push of its value.
* **`sImplQ_leafU`**: the leaf code `leafC` (`qopU [MC] eB1L eGL`) implements `tens Cm` on the
  single bit of level `0`, scale `ES 0 = 1`, width `+2`, from `KFN.sImpl_leaf`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex Butterfly

section Sub

variable (σ : Fin HS → Option ℤ)

theorem Ex.okBnd_sub {s : IState HS} (hs : Agree σ s) (B : ℕ) :
    ∀ e : Ex HS, e.ok s → e.Bnd s B → (Ex.sub σ e).ok s ∧ (Ex.sub σ e).Bnd s B
  | .reg i, h1, h2 => by
    unfold Ex.sub
    split
    · next v hv =>
      refine ⟨trivial, ?_⟩
      simp only [Ex.Bnd] at h2 ⊢; rwa [hs.top hv] at h2
    · exact ⟨h1, h2⟩
  | .lit c, h1, h2 => ⟨h1, h2⟩
  | .add a b, h1, h2 | .mul a b, h1, h2 => by
    have ha := Ex.okBnd_sub hs B a h1.1 h2.1
    have hb := Ex.okBnd_sub hs B b h1.2 h2.2.1
    refine ⟨⟨ha.1, hb.1⟩, ha.2, hb.2, ?_⟩
    rw [Ex.eval_sub σ hs a, Ex.eval_sub σ hs b]; exact h2.2.2
  | .shl a b, h1, h2 => by
    have ha := Ex.okBnd_sub hs B a h1.1 h2.1
    have hb := Ex.okBnd_sub hs B b h1.2.1 h2.2.1
    refine ⟨⟨ha.1, hb.1, by rw [Ex.eval_sub σ hs b]; exact h1.2.2⟩, ha.2, hb.2, ?_⟩
    rw [Ex.eval_sub σ hs a, Ex.eval_sub σ hs b]; exact h2.2.2
  | .quo a b, h1, h2 | .rem a b, h1, h2 => by
    have ha := Ex.okBnd_sub hs B a h1.1 h2.1
    have hb := Ex.okBnd_sub hs B b h1.2.1 h2.2
    exact ⟨⟨ha.1, hb.1, by rw [Ex.eval_sub σ hs b]; exact h1.2.2⟩, ha.2, hb.2⟩
  | .ndiv a b, h1, h2 | .nmod a b, h1, h2 => by
    have ha := Ex.okBnd_sub hs B a h1.1 h2.1
    have hb := Ex.okBnd_sub hs B b h1.2.1 h2.2.1
    refine ⟨⟨ha.1, hb.1, by rw [Ex.eval_sub σ hs a]; exact h1.2.2.1,
      by rw [Ex.eval_sub σ hs b]; exact h1.2.2.2⟩, ha.2, hb.2, ?_⟩
    rw [Ex.eval_sub σ hs a, Ex.eval_sub σ hs b]; exact h2.2.2
  | .neg a, h1, h2 => Ex.okBnd_sub hs B a h1 h2
  | .pow2 a, h1, h2 => by
    have ha := Ex.okBnd_sub hs B a h1.1 h2.1
    exact ⟨⟨ha.1, by rw [Ex.eval_sub σ hs a]; exact h1.2⟩, ha.2,
      by rw [Ex.eval_sub σ hs a]; exact h2.2⟩
  | .sel c x y, h1, h2 => by
    have hc := Ex.okBnd_sub hs B c h1.1 h2.1
    obtain ⟨h1a, h1b⟩ := h1
    obtain ⟨h2a, h2b⟩ := h2
    refine ⟨⟨hc.1, ?_⟩, hc.2, ?_⟩
    · show (if (Ex.sub σ c).eval s < 0 then _ else _)
      rw [Ex.eval_sub σ hs c]
      split_ifs at h1b ⊢ with hn
      · exact (Ex.okBnd_sub hs B x h1b (by simpa [hn] using h2b)).1
      · exact (Ex.okBnd_sub hs B y h1b (by simpa [hn] using h2b)).1
    · show (if (Ex.sub σ c).eval s < 0 then _ else _)
      rw [Ex.eval_sub σ hs c]
      split_ifs at h1b h2b ⊢ with hn
      · exact (Ex.okBnd_sub hs B x h1b h2b).2
      · exact (Ex.okBnd_sub hs B y h1b h2b).2

theorem ExV.sub {e : Ex HS} {v : ℤ} {B : ℕ} (he : ExV σ e v B) : ExV σ (Ex.sub σ e) v B :=
  fun t ht => by
    obtain ⟨a, b, c⟩ := he t ht
    obtain ⟨d, f⟩ := Ex.okBnd_sub σ ht B e a c
    exact ⟨d, by rw [Ex.eval_sub σ ht]; exact b, f⟩

end Sub

/-! ## The leaf -/

end NLogN.KFW

end

section
-- Source module: Solutions.KFWC1
/-!
# KFW C-layer tools: frames with shadowing, run specifications

* `ExV.of_regs`: an expression value only depends on the registers the expression reads.
* `NoRd`, **`pushSeq_of`**: a frame of pushes whose expressions are valued on a base assignment
  `σ0` and never read a register pushed earlier in the frame (registers may be shadowed).
* `RunQ σ U f g c`: from every background agreeing with `σ`, `U` runs from `encK s f` to
  `encK s g` within cost `c` (`f`, `g` fixed): frames (`runQ_push`), register tests
  (`runQ_ite`), calls, sequences.
* `recRep_uniq`, **`runQ_of_sImplQ`**: an `SImplQ` statement gives a `RunQ` with a fixed result.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option linter.unusedSectionVars false

namespace NLogN.KFW

open IntMul KIL KFD KFB KFG KFH KFN Complex Butterfly

/-! ## Expression values and frames -/

/-! ## Run specifications -/

section Run

variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

variable {σ : Fin HS → Option ℤ} {U V : IStmt HS Pp} {f g h : Fin HS → List ℤ} {c c' : ℕ}

theorem RunQ.seq (H1 : RunQ I iprog σ U f g c) (H2 : RunQ I iprog σ V g h c') :
    RunQ I iprog σ (.seq U V) f h (c + c') := fun s hs => (H1 s hs).seq_r6c (H2 s hs)

theorem RunQ.ext {σ' : Fin HS → Option ℤ} (H : RunQ I iprog σ U f g c) (he : SExt σ σ') :
    RunQ I iprog σ' U f g c := fun s hs => H s (hs.of_ext he)

end Run

/-! ## From `SImplQ` to a fixed run -/

end NLogN.KFW

end

section
-- Source module: Solutions.KFX2Rot
/-!
# KFX §2: register-driven table rotations (the lines (22) and the last bit)

* `pushSt_G_mem`, `pushOK_of`: pushed parameter lists built from `KFL.ESp` facts.
* `tabRot_runs`: a generic `withPushI pl (fcode U ; rotF)` where `U` pushes the rotation table.
* `tabGenU sgn b`: `KFL.tabGen` with the literals `P, Q, d0, d1, 2^ρ, f-1, 2^K` read from the
  registers `1, 2, 3, 5, 6, 7, 8` (`tabGenU_sub`: the literal instance is `RS.sub`).
* **`rotU_geo`**: one line `rixT g (rot2 Q (amt K ρ f l))` with parameters from expressions.
* `xorGenU`, **`xorU_geo`**: the last-bit step `rixT g (XLc K ρ f)`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option maxRecDepth 20000

namespace NLogN.KFX

open IntMul RS KIL KFD KFE KFB KFL KFW AModel Butterfly

/-! ## Pushed parameter lists -/

/-! ## A table generator followed by `rotF` -/

/-! ## The uniform table generator of a line -/

theorem notMem_zX {i : Fin HS} (h : i.val < 56) : i ∉ zX.all := by
  intro hz
  simp only [ExSt.all, zX, List.mem_cons, List.not_mem_nil, or_false] at hz
  rcases hz with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> exact absurd h (by decide)

/-! ## One line, register-driven -/

/-! ## The last-bit step, register-driven -/

end NLogN.KFX

end

section
-- Source module: Solutions.KFX4Core
/-!
# KFX §4: the register-driven Lemma 13 core

The fixed code `l13U q` is `KFL.l13code` with every size-dependent literal read from the
*master registers* (`MReg`): `w, 2·M·R` on `1, 6` (for `toBitsU`/`fromBitsU`), the swap flags on
`11, 12`, and `Q = 2^{fK}, B = R·2(w+1), 2^ρ, gx, N0, N1, N2, N3, A = zsz V, 2^K` on
`13, 15, 16, 17, 18, 19, 46, 47, 48, 49`, `f, K` on `36, 37`.  The slot swaps `preL px py` are
realized by two optional swaps (`optA`: swap `0` or `2` by the flag on `11`, `optB`: swap `1` by
the flag on `12`).  **`l13U_runs`** is `KFL.l13_runs` for this code.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option maxRecDepth 20000

namespace NLogN.KFX

open IntMul RS KIL KFD KFE KFB KFL KFW KFH AModel Butterfly

/-! ## Master registers -/

/-! ## Expression specifications from the masters -/

theorem ESp.ofAgree {σ : Fin HS → Option ℤ} {t : IState HS} (hA : Agree σ t) {r : Fin HS} {v : ℤ}
    (h : σ r = some v) (hr : r.val < 56) {Bb : ℕ} (hb : zsz v ≤ Bb) : ESp (.reg r) t Bb v := by
  refine ⟨fun i hi => ?_, hA.isInt h, ?_, hA.top h⟩
  · simp only [Ex.regs, List.mem_singleton] at hi; subst hi; exact notMem_zX hr
  · show zsz (t.top r) ≤ Bb; rw [hA.top h]; exact hb

/-! ## The expressions of the pieces -/

section Vals

variable {N0 N1 N2 N3 K f ρ R w : ℕ} {px py : Fin 3} {t : IState HS}

theorem PPos.geo (h : PPos N0 N1 N2 N3 K f ρ R) : (gB N0 N1 N2 N3 K f R w).Pos :=
  geoB_pos h.n0 h.n1 h.n2 h.n3 h.r

theorem gB_V (N0 N1 N2 N3 K f R w : ℕ) : (gB N0 N1 N2 N3 K f R w).V =
    N0 * 2 ^ (f * K) * N1 * 2 ^ (f * K) * N2 * 2 ^ (f * K) * (N3 * (R * (2 * (w + 1)))) := by
  simp only [gB, geoB, Geo.V, Geo.S0, Geo.S1, Geo.S2]; ring

/-- Every divisor of `V` has at most `zsz V + 3` bits. -/
theorem zdvd (hp : PPos N0 N1 N2 N3 K f ρ R) {a : ℕ}
    (h : a ∣ (gB N0 N1 N2 N3 K f R w).V) :
    zsz (a : ℤ) ≤ zsz ((gB N0 N1 N2 N3 K f R w).V : ℤ) + 3 :=
  le_trans (zsz_nat_le (Nat.le_of_dvd (hp.geo (w := w)).v h)) (by omega)

variable (hp : PPos N0 N1 N2 N3 K f ρ R) (hA : Agree (σMR N0 N1 N2 N3 K f ρ R w px py) t)
include hp hA

theorem sB : ESp (.reg mB) t (zsz ((gB N0 N1 N2 N3 K f R w).V : ℤ) + 3)
    ((R * (2 * (w + 1)) : ℕ) : ℤ) :=
  ESp.ofAgree hA rfl (by decide) (zdvd hp
    ⟨N0 * 2 ^ (f * K) * N1 * 2 ^ (f * K) * N2 * 2 ^ (f * K) * N3, by rw [gB_V]; ring⟩)

end Vals

end NLogN.KFX

/-! ## The code -/

namespace NLogN.KFX

open IntMul RS KIL KFD KFE KFB KFL KFW KFH AModel Butterfly

/-! ## Swap lists -/

end NLogN.KFX

end

section
-- Source module: Solutions.KFX5Head
/-!
# KFX §5: the header of the uniform row addition

From the row-addition parameters on the background stacks `36 … 45`
(`[mC^k, K, e, t, S0, B, r, H, i, j]`) the header computes the master registers `σMR` of
`l13U`: the third row `h ∉ {i, j}`, the sorted rows `s0 < s1 < s2`, the slots `px, py`, the
factors `N0 … N3` of the shape `shR`, `Q = 2^{fK}`, `2^K`, `2^ρ` (`ρ = e % K`), the swap flags,
`gx`, and (by a halving loop) `A = zsz V`.
-/

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
set_option maxRecDepth 20000

namespace NLogN.KFX

open IntMul RS KIL KFD KFE KFB KFL KFW KFH AModel Butterfly

/-! ## The sorted rows -/

/-! ## Expression combinators -/

section Comb

variable {u : IState HS} {Bb : ℕ}

theorem ESp.pow2 {a : Ex HS} {x : ℕ} (ha : ESp a u Bb (x : ℤ)) (hx : x + 1 ≤ Bb) :
    ESp (.pow2 a) u Bb ((2 ^ x : ℕ) : ℤ) := by
  refine ⟨ha.clean, ⟨ha.ok, by rw [ha.ev]; positivity⟩, ⟨ha.bnd, by rw [ha.ev]; simpa using hx⟩, ?_⟩
  simp only [Ex.eval, ha.ev]; simp

end Comb

/-! ## The parameter expressions -/

/-! ## Arithmetic of the rows -/

/-! ## The shape factors -/

/-! ## Specifications of the parameter expressions -/

end NLogN.KFX

end

section
-- Source module: Solutions.R6CxStep
/-!
# Round six, complex side: networks with slot-set children and temporaries (`Prop8IfaceH`)

Design decision 2 of `jain6/ARCH.md`. Compared with `P8Lift.Prop8IfaceR`:

* a child step `child w S neg` acts on a **slot set** `S ⊆ Fin m` of role `w` (all columns),
  with a **sign set** `neg`: with exact children it applies `C⁻¹` on the slots of `neg ∩ S`
  and `C` on the other slots of `S` (implemented as `(-i)^{|neg ∩ S||κ|} Z_N C^{⊗(S×κ)} Z_N`,
  one forward call of width `|S|`, by (17));
* roles are `Fin W ⊕ Fin T`: `W` data/scratch roles and `T` temporaries;
* correctness (**clean temporaries**): temporaries start at zero and are discarded, so only the
  data-to-data block of the denotation is constrained: it is block diagonal with `C^{⊗(Fin m × κ)}`
  on every role `inl _` (`DataCorrect`). This is Jain's tape model (a copy is a fresh zero
  stream, erased after use); `targetH` (dirty temporaries restored) implies it (`dataCorrect_of_targetH`);
* `hist`: the multiset of child widths `|S|` is `histMS h` (`n_w` children of width `w`),
  and every child width is `< m`.

Local steps are those of `P8Lift.RStep` (gates, row additions, phases, role permutations).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace IntMul.Kappa.R6.Cx

open Matrix Finset Complex Butterfly P8Lift

namespace HStep

variable {R : Type} {m : ℕ}

end HStep

/-! ## Slot-set families and the child semantics -/

/-! ## Denotations -/

section Den

variable {R : Type} [Fintype R] [DecidableEq R] {m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ]

namespace HStep

/-- With exact children a child step is the slot family on its wire. -/
theorem den_child_exact (w : R) (S neg : Finset (Fin m)) :
    (child w S neg : HStep R m).den (chEx (κ := κ)) = wireOp w (tensF (slotFam (κ := κ) S neg)) := by
  rw [den, signedOp_chEx]

end HStep

/-- Block replacement: a step list built block by block has the composite denotation. -/
lemma denListH_flatMap {ι : Type*} (ch : Finset (Fin m) → Op (Fin m × κ)) (L : List ι)
    (F : ι → List (HStep R m)) :
    denListH ch (L.flatMap F) = (L.map fun i => denListH ch (F i)).reverse.prod := by
  induction L with
  | nil => simp
  | cons i L ih =>
    rw [List.flatMap_cons, denListH_append, ih, List.map_cons, List.reverse_cons,
      List.prod_append, List.prod_singleton]

/-- Two block programs whose blocks have equal denotations have equal denotations
(e.g. single-slot kernel chunks replaced by merged chunks, `R6CxMerge`). -/
theorem denListH_flatMap_congr {ι : Type*} (ch : Finset (Fin m) → Op (Fin m × κ)) (L : List ι)
    (F G : ι → List (HStep R m)) (hFG : ∀ i ∈ L, denListH ch (F i) = denListH ch (G i)) :
    denListH ch (L.flatMap F) = denListH ch (L.flatMap G) := by
  rw [denListH_flatMap, denListH_flatMap, List.map_congr_left hFG]

/-- Child widths of a flatMap. -/
lemma widths_flatMap {ι : Type*} (L : List ι) (F : ι → List (HStep R m)) :
    (L.flatMap F).filterMap HStep.width = L.flatMap fun i => (F i).filterMap HStep.width := by
  induction L with
  | nil => rfl
  | cons i L ih => simp [List.flatMap_cons, List.filterMap_append, ih]

end Den

/-! ## The interface -/

namespace Prop8IfaceH

variable {W T m : ℕ} {h : List (ℕ × ℕ)}

end Prop8IfaceH

end IntMul.Kappa.R6.Cx

end

section
-- Source module: Solutions.R6IL2CMath
/-!
# Round six, compact controls (I2C): the value-level mechanism

Colkitt's compact dirty controls, uniform variant (see `jain6/compact/DESIGN.md`).  The state of
one record is `(t, u, y)` (the temporary `T`, the control `U`, the target slot `Y`); the source
slot `x` is a parameter.  Radices: `W = 2^K` (slot segments), `R = 2^G` (compact digits);
`n` low selected positions `j_s = ρ + s K`.

* `dgt W s x = x / W^s % W`; `digits_add`: digit-wise addition without carries;
  `eq_of_digits`: equal low digits and equal high part give equal numbers.
* `segSum tf ru rv rw w0 u v n = Σ_{s<n} w0 rw^s tf (u / ru^s) (v / rv^s)` (the register loop).
* The offsets `oA` (`Y += Σ 2 z_s t_s 2^{j_s}`), `oB` (`Y += Σ z_s (1 - 2 t_s) 2^{j_s}`), `oS`
  (packed selected bits), `oC` (`Σ (y_s xor z_s) R^s`), `oT` (the ideal toggle).
* The pull maps `rT, rU, rY`, the inverse phase `phInv` and the whole pull composite `Psi`.
* **`Psi_good`**: on a good state `Psi` is the ideal map (toggle the `n` low selected bits of `y`
  by those of `x`); `Psi_bij`-type facts are proved at rank level.
-/

set_option linter.unusedVariables false

namespace IntMul.Kappa.R6.IL2C

open Finset

/-! ## Digits -/

/-- Digit `s` of `x` in radix `W`. -/
def dgt (W s x : ℕ) : ℕ := x / W ^ s % W

/-! ## The register-loop sum -/

/-- `Σ_{s<n} w0 · rw^s · tf (u / ru^s) (v / rv^s)`. -/
def segSum (tf : ℤ → ℤ → ℤ) (ru rv rw w0 u v : ℤ) (n : ℕ) : ℤ :=
  ∑ s ∈ range n, w0 * rw ^ s * tf (u / ru ^ s) (v / rv ^ s)

/-! ## Parameters and the offsets -/

section Params

variable (K ρ G n : ℕ)

/-- Segment `s` of the slot `y` (the `K` bits at `ρ + s K`). -/
def seg (s y : ℕ) : ℕ := dgt (2 ^ K) s (y / 2 ^ ρ)

/-- Bit `ρ + s K` of `y`. -/
def ybit (s y : ℕ) : ℕ := seg K ρ s y % 2

/-- Digit `s` of a compact field. -/
def cdg (s w : ℕ) : ℕ := dgt (2 ^ G) s w

/-- `oA u t = Σ 2 z_s t_s 2^{ρ+sK}` (`z_s = cdg u s % 2`). -/
def oA (u t : ℕ) : ℤ :=
  segSum (fun a b => 2 * (a % 2) * (b % 2 ^ G)) (2 ^ G) (2 ^ G) (2 ^ K) (2 ^ ρ) u t n

/-- `oB u t = Σ z_s (1 - 2 t_s) 2^{ρ+sK}`. -/
def oB (u t : ℕ) : ℤ :=
  segSum (fun a b => (a % 2) * (1 - 2 * (b % 2 ^ G))) (2 ^ G) (2 ^ G) (2 ^ K) (2 ^ ρ) u t n

/-- `oS y = Σ ybit_s R^s` (packed selected bits). -/
def oS (y : ℕ) : ℤ := segSum (fun a _ => a % 2) (2 ^ K) 1 (2 ^ G) 1 ((y / 2 ^ ρ : ℕ) : ℤ) 0 n

/-- `oC u y = Σ (ybit_s xor z_s) R^s`. -/
def oC (u y : ℕ) : ℤ :=
  segSum (fun a b => (a + b) % 2) (2 ^ K) (2 ^ G) (2 ^ G) 1 ((y / 2 ^ ρ : ℕ) : ℤ) u n

/-- `oT x y = Σ x_s (1 - 2 y_s) 2^{ρ+sK}` (the ideal toggle). -/
def oT (x y : ℕ) : ℤ :=
  segSum (fun a b => (a % 2) * (1 - 2 * (b % 2))) (2 ^ K) (2 ^ K) (2 ^ K) (2 ^ ρ)
    ((x / 2 ^ ρ : ℕ) : ℤ) ((y / 2 ^ ρ : ℕ) : ℤ) n

end Params

/-! ## Closed forms of the offsets -/

/-! ## Segment-wise updates of a slot -/

/-! ## Modular pulls -/

/-- `((a - o) mod Q).toNat`. -/
def subM (Q : ℕ) (a : ℕ) (o : ℤ) : ℕ := (((a : ℤ) - o) % (Q : ℤ)).toNat

/-! ## States, the phases, the composites -/

/-- The state of one record: temporary `t`, control `u`, target slot `y`. -/
structure CS where
  t : ℕ
  u : ℕ
  y : ℕ

section Comp

variable (K ρ G n L : ℕ)

/-- The compact field size `R^n = 2^{nG}`. -/
abbrev Qc : ℕ := (2 ^ G) ^ n

/-- Pull of `T += o` is `T -= o`: `pT o` subtracts `o`. -/
def pT (o : ℤ) (c : CS) : CS := ⟨subM (Qc G n) c.t o, c.u, c.y⟩
def pU (o : ℤ) (c : CS) : CS := ⟨c.t, subM (Qc G n) c.u o, c.y⟩
def pY (o : ℤ) (c : CS) : CS := ⟨c.t, c.u, subM (2 ^ L) c.y o⟩

/-- The pull of one phase (`Y += oA; T += oS Y; Y += oB; T -= oC`). -/
def phInv (c : CS) : CS :=
  let c1 := pT G n (-(oC K ρ G n c.u c.y)) c
  let c2 := pY L (oB K ρ G n c1.u c1.t) c1
  let c3 := pT G n (oS K ρ G n c2.y) c2
  pY L (oA K ρ G n c3.u c3.t) c3

/-- The phase itself (push). -/
def phFw (c : CS) : CS :=
  let c1 := pY L (-(oA K ρ G n c.u c.t)) c
  let c2 := pT G n (-(oS K ρ G n c1.y)) c1
  let c3 := pY L (-(oB K ρ G n c2.u c2.t)) c2
  pT G n (oC K ρ G n c3.u c3.y) c3

/-- **The pull of the whole program** (load `U += sel x`, phase, unload, phase): apply the
pulls of the ten steps from the last to the first. -/
def Psi (x : ℕ) (c : CS) : CS :=
  phInv K ρ G n L (pU G n (oS K ρ G n x) (phInv K ρ G n L (pU G n (-(oS K ρ G n x)) c)))

/-- The program itself. -/
def Sfw (x : ℕ) (c : CS) : CS :=
  pU G n (oS K ρ G n x) (phFw K ρ G n L (pU G n (-(oS K ρ G n x)) (phFw K ρ G n L c)))

/-- The ideal map (toggle the `n` low selected bits of `y` by those of `x`). -/
def Tl (x y : ℕ) : ℕ := ((y : ℤ) + oT K ρ n x y).toNat

def TlS (x : ℕ) (c : CS) : CS := ⟨c.t, c.u, Tl K ρ n x c.y⟩

/-- The box. -/
def Box (c : CS) : Prop := c.t < Qc G n ∧ c.u < Qc G n ∧ c.y < 2 ^ L

/-- Good states. -/
def Good (c : CS) : Prop :=
  ∀ s < n, cdg G s c.t + 2 ≤ 2 ^ G ∧ cdg G s c.u + 2 ≤ 2 ^ G ∧ 1 ≤ seg K ρ s c.y / 2 ∧
    seg K ρ s c.y / 2 + 2 ^ G + 1 ≤ 2 ^ (K - 1)

end Comp

/-! ## Exactness on good states -/

end IntMul.Kappa.R6.IL2C

end

section
-- Source module: Solutions.R6IL2CIdx
/-!
# Round six, compact controls (I2C): rank maps

* `rix_flR`: a reindexing of the bit array that acts record-wise is a reindexing of the records.
* `rotP`, `rot_flR`: the table rotation (`KFC.rotF`) of a field `(Q, S)` on records.
* `swP`, `sw_flR`: the Lemma 12 swap of two fields of the same size on records.
* Fields `(Q, S)` nested in each other: `gc`/`sc` commute (`fld_*`).
* `Lay`: the five fields `T, U, X, Y, Bk` of a record index; `cs m`, `xv m`, `setCS`;
  each step of the program is `m ↦ setCS (F (xv m) (cs m)) m` (`stepP`), and steps compose.
-/

set_option linter.unusedVariables false
set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.IL2C

open NLogN NLogN.KFL AModel AModelL12

/-! ## Record-wise reindexing -/

/-! ## Fields with a record factor -/

/-! ## Rotations on records -/

/-- The pull of the rotation of field `(Q, S)` by the table `as` (indexed by the prefix). -/
def rotP (Q S : ℕ) (as : ℕ → ℕ) (m : ℕ) : ℕ := sc Q S ((gc Q S m + Q - as (m / (Q * S))) % Q) m

/-! ## Swaps on records -/

/-- The pull of the swap of the fields `(F, S1)` (upper) and `(F, S2)` (lower). -/
def swP (F S1 S2 m : ℕ) : ℕ := sc F S1 (gc F S2 m) (sc F S2 (gc F S1 m) m)

/-! ## Nested fields -/

/-! ## The layout of a record index -/

/-- The five fields of a record index: `T, U` (size `QC`), `X, Y` (size `QL`), `Bk` (size `QC`). -/
structure Lay where
  QC : ℕ
  QL : ℕ
  sT : ℕ
  sU : ℕ
  sX : ℕ
  sY : ℕ
  sB : ℕ
  M : ℕ

/-- `T > U > {X, Y} > Bk` (record order, most significant first), all nested. -/
structure Lay.OK (l : Lay) : Prop where
  qc : 0 < l.QC
  ql : 0 < l.QL
  pB : 0 < l.sB
  kTU : ∃ k, 0 < k ∧ l.sT = l.sU * l.QC * k
  kUX : ∃ k, 0 < k ∧ l.sU = l.sX * l.QL * k
  kUY : ∃ k, 0 < k ∧ l.sU = l.sY * l.QL * k
  kXB : ∃ k, 0 < k ∧ l.sX = l.sB * l.QC * k
  kYB : ∃ k, 0 < k ∧ l.sY = l.sB * l.QC * k
  kXY : (∃ k, 0 < k ∧ l.sX = l.sY * l.QL * k) ∨ (∃ k, 0 < k ∧ l.sY = l.sX * l.QL * k)
  kM : ∃ k, 0 < k ∧ l.M = l.sT * l.QC * k

namespace Lay

variable {l : Lay}

/-- The state `(t, u, y)` of record `m`. -/
def cs (l : Lay) (m : ℕ) : CS := ⟨gc l.QC l.sT m, gc l.QC l.sU m, gc l.QL l.sY m⟩

/-- The source slot of record `m`. -/
def xv (l : Lay) (m : ℕ) : ℕ := gc l.QL l.sX m

/-- Record `m` with the state `c`. -/
def set (l : Lay) (c : CS) (m : ℕ) : ℕ := sc l.QC l.sT c.t (sc l.QC l.sU c.u (sc l.QL l.sY c.y m))

/-- The box of states. -/
def BoxL (l : Lay) (c : CS) : Prop := c.t < l.QC ∧ c.u < l.QC ∧ c.y < l.QL

/-- A step of the program as a record pull. -/
def stepP (l : Lay) (F : ℕ → CS → CS) (m : ℕ) : ℕ := l.set (F (l.xv m) (l.cs m)) m

/-! ### Single fields as states -/

/-! ### Rotations as steps -/

/-! ### Fields read through the swaps -/

end Lay

/-! ## Digits of unreduced field values -/

end IntMul.Kappa.R6.IL2C

end