κ-improvement development, part 9: array model and networks

-- OpenAI-preprint / κ-improvement development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_K_Defs8

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.GlueProp14
/-!
# Glue 1: Proposition 14 unconditionally (through `complexIface`)

`ButterflyProp14.prop14_output` takes an implementation `Cimpl` of `C^{⊗D}` on the `D` selected
bits together with a proof `Cimpl = tens Cm`.  Here we *build* that implementation from the
recursive program `recOp` of an arbitrary `Prop8Iface` (the network recursion of §5.1), cutting
the `D` selected bits into consecutive pieces of sizes `u · m^k` given by the base-`m` digits of
`D` (piece `k` = the depth-`k` program with leaf width `u = k`-th digit), embedding each piece on
its block of bits and multiplying (`tens_blocks`, `embed_tens`).

* `cRec I D` : the operator computed by the pieces; `cRec_eq` : `cRec I D = tens Cm` (`2 ≤ m`).
* `cRecC D := cRec complexIface.toIface D` (`W_c` roles, `m = 100³`, `s_c` children).
* **`prop14_unconditional`**: for the concrete layer `[P] × [2^K]^D × [S]` (bit `ρ` of every
  chunk), the procedure `Q_p(b^D S_D · C-layer(cRecC) · S_D z)` equals `Q_p(H0^{⊗D} z)`, every
  output coefficient lies in the unit disk and is within `√2·2^{-p}` of the exact layer.
* **`prop14_unconditional_sel`**: the same for an arbitrary selected-bit structure `Sb` on any
  shape with any finite index type `ι` (the C-layer is `cRecC` transported along `ι ≃ Fin |ι|`).
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace GlueP14

open Matrix Finset Butterfly AModel

/-! ## 1. Interval blocks -/

/-- The block of selected bits `[off, off + sz)`. -/
def blk (D off sz : ℕ) : Finset (Fin D) := univ.filter fun j => off ≤ (j : ℕ) ∧ (j : ℕ) < off + sz

lemma mem_blk {D off sz : ℕ} {j : Fin D} : j ∈ blk D off sz ↔ off ≤ (j : ℕ) ∧ (j : ℕ) < off + sz := by
  simp [blk]

lemma card_blk {D off sz : ℕ} (h : off + sz ≤ D) : (blk D off sz).card = sz := by
  have hmap : (blk D off sz).map Fin.valEmbedding = Finset.Ico off (off + sz) := by
    ext x
    simp only [Finset.mem_map, mem_blk, Fin.valEmbedding_apply, Finset.mem_Ico]
    constructor
    · rintro ⟨j, hj, rfl⟩; exact hj
    · intro hx; exact ⟨⟨x, by omega⟩, hx, rfl⟩
  rw [← Finset.card_map Fin.valEmbedding, hmap, Nat.card_Ico]; omega

/-! ## 2. Pieces -/

/-- Total number of selected bits of a piece list `(u, k)` (piece size `u · m^k`). -/
def tot (m : ℕ) : List (ℕ × ℕ) → ℕ
  | [] => 0
  | (u, k) :: ps => u * m ^ k + tot m ps

/-- The blocks of a piece list starting at offset `off`. -/
def blocks (D m : ℕ) : ℕ → List (ℕ × ℕ) → List (Finset (Fin D))
  | _, [] => []
  | off, (u, k) :: ps => blk D off (u * m ^ k) :: blocks D m (off + u * m ^ k) ps

variable {W m s : ℕ} [NeZero W] (I : Prop8Iface W m s)

/-- One piece: the depth-`k` recursive program with leaf width `u`, embedded on its block. -/
noncomputable def pieceOp (D off u k : ℕ) : Op (Fin D) :=
  if h : off + u * m ^ k ≤ D then
    Butterfly.embed (blk D off (u * m ^ k))
      (Fintype.equivOfCardEq ((card_Lvl u m k).trans
        ((card_blk h).symm.trans (Fintype.card_coe _).symm))) (recOp I u k)
  else 1

/-- All pieces of a piece list, from offset `off`. -/
noncomputable def pieceList (D : ℕ) : ℕ → List (ℕ × ℕ) → List (Op (Fin D))
  | _, [] => []
  | off, (u, k) :: ps => pieceOp I D off u k :: pieceList D (off + u * m ^ k) ps

/-! ## 3. Base-`m` digit pieces -/

/-- Pieces `(digit_k, k)` for the first `f` base-`m` digits of `D`, starting at level `k`. -/
def digitPieces (m : ℕ) : ℕ → ℕ → ℕ → List (ℕ × ℕ)
  | 0, _, _ => []
  | f + 1, D, k => (D % m, k) :: digitPieces m f (D / m) (k + 1)

/-- **The recursive implementation of the `C`-layer on `D` selected bits**: the pieces given by
the base-`m` digits of `D`, each the recursive network program of its depth. -/
noncomputable def cRec (D : ℕ) : Op (Fin D) := (pieceList I D 0 (digitPieces m D D 0)).prod

/-! ## 4. The complex network instance -/

/-- The C-layer implementation through the complex network (`complexIface`, `m = 100³`). -/
noncomputable def cRecC (D : ℕ) : Op (Fin D) := cRec P8Lift.complexIface.toIface D

/-! ## 5. Arbitrary selected-bit structures -/

section General

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

/-- Transport an operator on `Fin |ι|` bits to `ι` bits. -/
def reidx (e : ι ≃ Fin (Fintype.card ι)) (T : Op (Fin (Fintype.card ι))) : Op ι :=
  fun x y => T (x ∘ e.symm) (y ∘ e.symm)

/-- The C-layer implementation on `ι` selected bits. -/
noncomputable def cRecι : Op ι := reidx (Fintype.equivFin ι) (cRecC (Fintype.card ι))

variable {sh : Shape} {r : ℕ}

/-- The layer procedure for an arbitrary selected-bit structure. -/
noncomputable def prop14ProcG (Sb : SelBits sh ι) (p : ℕ) (Cimpl : Op ι) (xs : List (Fin r → ℂ)) :
    List (Fin r → ℂ) :=
  QpArr p ((selOp Sb SD (selOp Sb Cimpl (selOp Sb SD xs))).map ((cb ^ Fintype.card ι) • ·))

end General

end GlueP14

end

section
-- Source module: Solutions.SynthNorm
/-!
# §6 The coefficient norm on `R_r = ℂ[y]/(y^r+1)`, monomials, and truncation

A *coefficient model* of `R` is a `ℂ`-linear injective coefficient map `co : R → (Fin r → ℂ)`
with `co 1 = e₀` and `co (y z) = cyc (co z)`, where `cyc` is the negacyclic shift
(`(y z)_0 = -z_{r-1}`, `(y z)_j = z_{j-1}`). The norm of `z` is the sup norm `‖co z‖`.
(`SynthModel.lean` constructs the model on `AdjoinRoot (X^r + 1)`.)

* `norm_co_yp`: every power `y^e` (`e : ℤ`) is an isometry.
* `co_pow_mul` (**monomial split-and-merge**): for `0 ≤ s ≤ r`,
  `(y^s z)_j = z_{j-s}` for `j ≥ s` and `-z_{j+r-s}` otherwise (the tail moved in front and
  negated); with `y^{er+s} = (-1)^e y^s` this is the paper's implementation of `J_E`.
* `eq_sum_co`: `z = ∑_k z_k y^k`; `norm_co_mul_le`: `‖uv‖ ≤ r ‖u‖ ‖v‖`.
* `norm_co_Fm_le`, `norm_co_Fp_le`: the transforms are contractions.
* `QpR`: coefficientwise truncation; (26) `norm_co_QpR_sub_lt`, `norm_co_QpR_le`;
  `QpR_yp`: `Q_p (y^E z) = y^E Q_p z` (truncation toward zero is odd, `J_E` a signed permutation).
-/

set_option linter.unusedSectionVars false

namespace Synth

open Finset Butterfly

variable {R : Type*} [CommRing R] [Algebra ℂ R]

/-! ## 1. The negacyclic shift -/

/-- Coefficients of `y z` from those of `z`. -/
def cyc {r : ℕ} (v : Fin r → ℂ) (j : Fin r) : ℂ :=
  if h : (j : ℕ) = 0 then -v ⟨r - 1, by have := j.isLt; omega⟩
  else v ⟨j - 1, by have := j.isLt; omega⟩

/-- A coefficient model of `R` for the unit `y`, with `r` coefficients. -/
structure CoeffModel (y : Rˣ) (r : ℕ) where
  pos : 0 < r
  co : R →ₗ[ℂ] (Fin r → ℂ)
  inj : Function.Injective co
  co_one : co 1 = Pi.single (⟨0, pos⟩ : Fin r) 1
  co_y : ∀ z, co ((y : R) * z) = cyc (co z)

variable {y : Rˣ} {r : ℕ} (C : CoeffModel y r)

/-! ## 2. Isometries -/

/-! ## 3. Expansion and products -/

/-! ## 4. The transforms are contractions -/

variable {D : ℕ}

/-! ## 5. Truncation `Q_p` on records -/

/-- `Q_p` on a record: truncate every real and imaginary coefficient part toward zero. -/
noncomputable def QpR (p : ℕ) (z : R) : R := ∑ k : Fin r, Qp p (C.co z k) • (y : R) ^ (k : ℕ)

end Synth

end

section
-- Source module: Solutions.GlueError
/-!
# Glue 2b: Lemma 16 error bound, with the approximation hypotheses discharged by Proposition 14

Records live in a commutative `ℂ`-algebra `R` with a coefficient model `C` (`R_r` is one,
`rrModel`); the size of a record is the sup of its coefficient moduli.

* `CArr C N`: arrays of `N` records with the sup-of-coefficients metric (pulled back by `C.co`).
* A *round* (§6.1) on any selected-bit structure `Sb` with twiddle exponents `Ex`: the exact round
  `exactR = J_E ∘ H0^{⊗}` (`= roundL`, `roundL_eq`) and the computed round
  `compR = J_E ∘ Q_p ∘ H0^{⊗}`.
* **`layerQ_eq_prop14`**: the computed (truncated) layer *is* the output of Proposition 14's
  procedure with the recursive complex-network `C`-layer (`prop14ProcG … cRecι`), read
  coefficientwise; **`paper_layerQ_eq_prop14`**: on the chunk rounds of the paper layout it is
  `prop14Proc` on `layerSel (2^A) K D (2^B) ρ` with `cRecC D` (via `paper_round_layerH`).
* The three hypotheses of `Synth.error_chain` hold for the rounds (`round_contract`,
  `round_disk`, `comp_disk`, `comp_err`; `η = √2·2^{-p}`), so
* **`lemma16_error`**: the computed procedure (rounds `h = ℓ-1, …, 0`) differs from the exact one
  by less than `ℓ √2 2^{-p}` in every coefficient of every record, and stays in the unit disk;
* **`lemma16_error_Fm`**: at every valid address `v`, the computed record is within
  `ℓ √2 2^{-p}` of `(F^- z)(rev (coord v))` (combining with `synth_forward_list`), and
  **`lemma16_error_paper`** the same on the paper's layout `L`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace GlueError

open Finset Butterfly AModel Synth GlueLayout GlueP14

variable {R : Type*} [CommRing R] [Algebra ℂ R] {y : Rˣ} {r : ℕ}

/-! ## 1. Arrays of records with the coefficient metric -/

/-- Arrays of `N` records. -/
def CArr (_C : CoeffModel y r) (N : ℕ) : Type _ := Fin N → R

variable (C : CoeffModel y r)

instance instACGCArr (N : ℕ) : AddCommGroup (CArr C N) := Pi.addCommGroup

/-- The coefficient map of an array. -/
def coHom (N : ℕ) : CArr C N →+ (Fin N → Fin r → ℂ) where
  toFun u j := C.co ((u : Fin N → R) j)
  map_zero' := by funext j; exact map_zero C.co
  map_add' u v := by funext j; exact map_add C.co _ _

/-- The sup-of-coefficients seminorm on arrays. -/
noncomputable instance instSNCArr (N : ℕ) : SeminormedAddCommGroup (CArr C N) :=
  SeminormedAddCommGroup.induced _ _ (coHom C N)

variable {C}

/-- Read a list as an array. -/
def toA (C : CoeffModel y r) (N : ℕ) (xs : List R) : CArr C N := fun j => xs.getD j 0

/-- Write an array as a list. -/
def ofA {N : ℕ} (u : CArr C N) : List R := List.ofFn (n := N) fun j => (u : Fin N → R) j

/-- The unit disk of arrays. -/
def disk (C : CoeffModel y r) (N : ℕ) : Set (CArr C N) :=
  {u | ∀ j, ‖C.co ((u : Fin N → R) j)‖ ≤ 1}

/-! ## 2. Rounds -/

variable {D : ℕ} {sh : Shape} {ι : Type} [Fintype ι] [DecidableEq ι]

/-- The recordwise monomial `J_E`, `E = Ex j` at index `j`. -/
noncomputable def twL (y : Rˣ) (sh : Shape) (Ex : ℕ → ℤ) (zs : List R) : List R :=
  (List.range (vol sh)).map fun j => yp y (Ex j) * zs.getD j 0

/-- The exact round `J_E ∘ H0^{⊗}`. -/
noncomputable def exactR (y : Rˣ) (Sb : SelBits sh ι) (Ex : ℕ → ℤ) (xs : List R) : List R :=
  twL y sh Ex (selOp Sb (Butterfly.tens H0) xs)

/-- The computed layer: `H0^{⊗}` then `Q_p` on every record. -/
noncomputable def layerQ (C : CoeffModel y r) (p : ℕ) (Sb : SelBits sh ι) (xs : List R) :
    List R :=
  (selOp Sb (Butterfly.tens H0) xs).map (QpR C p)

/-- The computed round `J_E ∘ Q_p ∘ H0^{⊗}`. -/
noncomputable def compR (C : CoeffModel y r) (p : ℕ) (Sb : SelBits sh ι) (Ex : ℕ → ℤ)
    (xs : List R) : List R :=
  twL y sh Ex (layerQ C p Sb xs)

/-- The twiddle exponents of round `h` of `roundL`. -/
noncomputable def roundEx {a : Fin D → ℕ} (L : CoordLayout sh a) (ℓ h : ℕ)
    (P : Finset (Fin D)) : ℕ → ℤ :=
  fun j => ((roundAxes P).map fun i => twE ℓ h (L.coord (decode sh j) i)).sum

/-! ### The computed layer is Proposition 14's procedure -/

/-! ### Contraction, disk, truncation error -/

section Maps

variable (C) (p : ℕ) (Sb : SelBits sh ι) (Ex : ℕ → ℤ)

/-- The exact round on arrays. -/
noncomputable def Emap (u : CArr C (vol sh)) : CArr C (vol sh) := toA C (vol sh) (exactR y Sb Ex (ofA u))

/-- The computed round on arrays. -/
noncomputable def Amap (u : CArr C (vol sh)) : CArr C (vol sh) :=
  toA C (vol sh) (compR C p Sb Ex (ofA u))

variable {C}

end Maps

/-! ## 3. Procedures and Lemma 16 -/

/-- Rounds `n-1, …, 0` of a family of list maps. -/
def runDown {α : Type*} (F : ℕ → α → α) : ℕ → α → α
  | 0, x => x
  | n + 1, x => runDown F n (F n x)

/-- **The computed procedure of Lemma 16**: rounds `h = n-1, …, 0`, each `J_E ∘ Q_p ∘ H0^{⊗}`
(the layer computed by Proposition 14's procedure, `layerQ_eq_prop14`). -/
noncomputable def procQ (C : CoeffModel y r) (p : ℕ) {a : Fin D → ℕ} (L : CoordLayout sh a)
    (ℓ : ℕ) (P : ℕ → Finset (Fin D)) (Sb : (h : ℕ) → SelBits sh {i // i ∈ P h}) :
    ℕ → List R → List R :=
  runDown fun h => compR C p (Sb h) (roundEx L ℓ h (P h))

/-! ## 4. The paper's layout -/

section Paper

variable (D ℓ K : ℕ) [NeZero D] (long : Fin D → Bool)

end Paper

end GlueError

end

section
-- Source module: Solutions.ResampleParams
/-!
# §9.1–9.2 Fixed rational choice and sizes

* `constants_ok`: the layer and dimension conditions of (38), `margins_ok`: the seven margins
  of (45) with `min gᵢ = 2⁻¹⁸¹ = 2κ`.
* Axis lengths `t_i ∈ {r/2, r}` with `∏ t_i = T`, last axis `r` (`axExp_sum`, `axLen_prod`,
  `axExp_last`), `p/(12d) ≤ ℓ ≤ p/(3d)` (`ell_bounds`), `24n ≤ T p < 48 n` (`Tp_bounds`).
* Source lengths: `(1-2η)t_i < s_i ≤ (1-η)t_i` ⇒ `S > T/2` (`S_gt_half`), `θ_i > η`
  (`theta_gt_eta`), `α⁴θ_i > p` (`alpha4_theta_gt_p`), `γ < 28 d² √b` (`gamma_bound`);
  existence of pairwise coprime odd `s_i` (`sources_exist`, from `RCop.coprime_params`).
* Radix digits (§9.2.3): `2q - 2 < S` (`degree_lt_S`) and `c_j < 2^{3b}` (`coeff_lt`).
-/

open Finset

namespace IntMul.OpenAI.RP

/-! ### (38) and (45) -/

/-! ### Axis lengths of the padded box -/

/-- `ℓ = ⌈L/d⌉`. -/
def ell (L d : ℕ) : ℕ := (L + d - 1) / d

/-! ### Source lengths, resampling margins -/

/-! ### §9.2.3 radix-digit polynomials -/

end IntMul.OpenAI.RP

end

section
-- Source module: Solutions.ResampleCost
/-!
# §9.8 The complete time bound

* `Ncost`: the normalized cost of Table 1 (cost divided by `V = T p`),
  `dK + pK^{τ-1} + ℓ d^{λ'} + d²(1+ℓ^τ) + d p^{1/2+δ} α + d p^δ + log₂(rp) + p^δ + 1`.
* `Ncost_le`: under the pointwise parameter bounds of §9.2.1
  (`p^ε/12 ≤ d ≤ p^ε`, `p^{εc}/24 ≤ K ≤ p^{εc}`, `ℓ ≤ p/(3d)`, `α ≤ 4 p^{1/4+ε/2}`),
  `Ncost ≤ 50 p^{1-2κ}` with `κ = 2⁻¹⁸²`.
* `concrete_d_bounds`, `concrete_K_bounds`, `concrete_alpha_bound`: the floors/ceilings
  `d = ⌊b^ε⌋`, `K = ⌊d^c⌋`, `α = ⌈(12d²b)^{1/4}⌉` satisfy these bounds with `p = 6b`.
* `kappaBound_of_table`: a correct multitape machine whose time on length `n ≥ n₀` is at most
  `C₀ (V(n) · Ncost(n) + n)` with `V ≤ 48n`, `p = 6 lg n` and parameters obeying the pointwise
  bounds satisfies the campaign statement `KappaBound (2⁻¹⁸²)`, i.e. time `O(n (lg n)^{1-κ})`.
-/

open Real

namespace IntMul.OpenAI.RCost

noncomputable section

def τ : ℝ := 1 - 1 / 2 ^ 50
def δ : ℝ := 1 / 16
def c : ℝ := 1 / 2 ^ 56
def lam' : ℝ := 1 - 1 / 2 ^ 54
def ε : ℝ := 1 / 2 ^ 75
def κ : ℝ := 1 / 2 ^ 182
/-- The common exponent `1 - 2κ`. -/
def es : ℝ := 1 - 2 * κ

/-- Normalized Table 1 cost (all rows after division by `T p`). -/
def Ncost (p d K ℓ α : ℝ) : ℝ :=
  d * K + p * K ^ (τ - 1) + ℓ * d ^ lam' + d ^ 2 * (1 + ℓ ^ τ) + d * p ^ (1 / 2 + δ) * α +
    d * p ^ δ + (ℓ + Real.logb 2 p) + p ^ δ + 1

/-! ### The concrete parameters of §9.2.1 satisfy the pointwise bounds -/

/-! ### Connection to the campaign statement -/

end

end IntMul.OpenAI.RCost

end

section
-- Source module: Solutions.GlueParams
/-!
# Glue 3: explicit parameters `n ↦ (b, L, T, d, K, ℓ, α, p)` of §9.2 and the threshold `n₀`

For an input length `n` (§9.2.1):
* `b = lg n` (`bP`), `p = 6b` (`pP`), `d = ⌊b^ε⌋` (`dP`), `K = ⌊d^c⌋` (`KP`),
  `α = ⌈(12 d² b)^{1/4}⌉` (`αP`);
* `L` (`LP`) = the least `L` with `4n ≤ 2^L b`, `T = 2^L` (`TP`), so `4n ≤ T b < 8n`;
* `ℓ = ⌈L/d⌉` (`ℓP`, `RP.ell`), `r = 2^ℓ` (`rP`), bit volume `V = T p` (`VP`), `γ = 2dα²` (`γP`).

The threshold is `n₀ = 2^{b₀}` with `b₀ = 2^{2^{132}}` (`n0`, `b0`); for `n ≥ n₀` we have
`b ≥ b₀` (`b_ge`), and `params_ok` proves every pointwise condition used in §8–9:
`b^ε ≥ 2`, `d^c ≥ 2`, `1 ≤ d ≤ b`, `b/2 ≤ L < b`, `24n ≤ Tp ≤ 48n`, `p/(12d) ≤ ℓ ≤ p/(3d)`,
`64d²(256d²)! ≤ r`, `2 | r`, `2dp² < TL`, `b ≥ 8192`, `T < 2^b`, `12 d² b ≤ α⁴`,
`γ ≤ b/4`, the bounds of `kappaBound_of_table` on `d, K, ℓ, α`, and the existence of the
pairwise coprime odd source lengths (`RP.sources_exist`).

**`kappaBound_of_machine`**: the only hypotheses left are about the machine `M`
(correct for all `n ≥ 1`; time `≤ C₀ (V · Ncost + n)` for `n ≥ n₀` with these parameters).
-/

open Real

namespace IntMul.OpenAI.Glue

open RCost

noncomputable section

/-! ## 1. The parameter map -/

/-- `b₀ = 2^{2^{132}}`, written as the ceiling of the real number `2^{2^{132}}` (an integer)
so that the kernel never tries to evaluate the tower. -/
def b0 : ℕ := ⌈(2 : ℝ) ^ ((2 : ℝ) ^ 132)⌉₊
/-- `n₀ = 2^{b₀}`. -/
def n0 : ℕ := 2 ^ b0

/-- `b = lg n`. -/
def bP (n : ℕ) : ℕ := IntMul.lg n
/-- `p = 6b`. -/
def pP (n : ℕ) : ℕ := 6 * bP n
/-- `d = ⌊b^ε⌋`. -/
def dP (n : ℕ) : ℕ := ⌊(bP n : ℝ) ^ IntMul.OpenAI.RCost.ε⌋₊
/-- `K = ⌊d^c⌋`. -/
def KP (n : ℕ) : ℕ := ⌊(dP n : ℝ) ^ c⌋₊
/-- `α = ⌈(12 d² b)^{1/4}⌉`. -/
def αP (n : ℕ) : ℕ := ⌈(12 * (dP n : ℝ) ^ 2 * bP n) ^ ((1 : ℝ) / 4)⌉₊

lemma bP_pos (n : ℕ) : 1 ≤ bP n := le_max_right _ _

lemma LP_exists (n : ℕ) : ∃ L : ℕ, 4 * n ≤ 2 ^ L * bP n := ⟨4 * n, by
  have h1 := bP_pos n
  have h2 : 4 * n < 2 ^ (4 * n) := Nat.lt_two_pow_self
  nlinarith⟩

/-- `L`: least exponent with `4n ≤ 2^L b`. -/
def LP (n : ℕ) : ℕ := Nat.find (LP_exists n)
/-- `T = 2^L`. -/
def TP (n : ℕ) : ℕ := 2 ^ LP n
/-- `ℓ = ⌈L/d⌉`. -/
def ℓP (n : ℕ) : ℕ := RP.ell (LP n) (dP n)
/-- `r = 2^ℓ`. -/
def rP (n : ℕ) : ℕ := 2 ^ ℓP n
/-- Bit volume `V = T p`. -/
def VP (n : ℕ) : ℝ := (TP n : ℝ) * (pP n : ℝ)
/-- `γ = 2 d α²`. -/
def γP (n : ℕ) : ℝ := 2 * (dP n : ℝ) * (αP n : ℝ) ^ 2

/-! ## 2. Elementary inequalities -/

/-! ## 3. Consequences of `n ≥ n₀` -/

/-! ## 4. All parameter conditions for `n ≥ n₀` -/

/-! ## 5. The final reduction -/

end

end IntMul.OpenAI.Glue

end

section
-- Source module: Solutions.SynthConv
/-!
# §7.1 The normalized convolution interface (Proposition 18)

* `conv`: multidimensional cyclic convolution on the box `∏ ℤ/2^{a_i}` with values in `R`.
* `Fm_conv` (**convolution theorem**): `F^-(f ∗ g) = M (F^- f)(F^- g)`.
* `normalization`: `M F^+((F^- f)(F^- g)/r) = (f ∗ g)/(rM) = M_r(f, g)` on the box.
* `norm_Mr_le`: `M_r` is a bilinear contraction, `‖M_r(f,g)‖_∞ ≤ ‖f‖_∞ ‖g‖_∞`;
  `Mr_sub_left` (bilinearity) and `norm_Mr_sub_left`.
* `pointwise_pull`: a pointwise product commutes with any record permutation (`LB`).
* `prop18_error`: from the forward errors `< δ`, the product-truncation error `< η` and the
  opposite procedure's error `< δ`, the opposite output is within `3δ + η` of `T₊ z*`;
  `prop18_scaled` multiplies by `M`, `prop18_constant` is `M(3δ+η) = √2 M (3ℓ+1) 2^{-p}`, and
  `prop18_disk` is the closing disk argument.
  (The forward and opposite error bounds are hypotheses: they are Lemma 16's outputs, which rest
  on Proposition 14 and hence on the Proposition 8 interface `Prop8Iface`.)
-/

set_option linter.unusedSectionVars false

namespace Synth

open Finset Butterfly

variable {R : Type*} [CommRing R] [Algebra ℂ R] (y : Rˣ) {D : ℕ}

/-! ## 1. Cyclic convolution and the convolution theorem -/

/-- Cyclic sum of addresses `(k + m) mod t`. -/
def wrap (a : Fin D → ℕ) (k m : Fin D → ℕ) : Fin D → ℕ := fun i => (k i + m i) % 2 ^ a i

/-- Cyclic convolution in the displayed axes. -/
noncomputable def conv (a : Fin D → ℕ) (f g : (Fin D → ℕ) → R) (x : Fin D → ℕ) : R :=
  ∑ k ∈ box a, ∑ m ∈ box a, if wrap a k m = x then f k * g m else 0

variable {y}

/-- `M_r(f, g) = (f ∗ g)/(rM)`. -/
noncomputable def Mr (r : ℕ) (a : Fin D → ℕ) (f g : (Fin D → ℕ) → R) (x : Fin D → ℕ) : R :=
  ((r * Mv a : ℕ) : ℂ)⁻¹ • conv a f g x

/-! ## 2. `M_r` is a bilinear contraction -/

section Model

variable {r : ℕ} (C : CoeffModel y r)

end Model

/-! ## 3. The error estimate -/

end Synth

end

section
-- Source module: Solutions.GlueProp18
/-!
# Glue 2c: the opposite procedure on the tape and Proposition 18's error, unconditionally

* §1–2 `roundLI` (one opposite round on the tape: inverse twiddle `J_{-E}`, then the layer
  `H0^{⊗}`), `procLI` (rounds `h = 0, …, n-1`), `fn_procLI` and **`synth_opposite_list`**
  (`procLI` implements `F^+ B^{-1}`: at address `v` it returns `F^+(w ∘ rev)(coord v)`).
* §3 a generic error chain for list procedures (`chain_lists`, via `Synth.error_chain`) and the
  computed opposite procedure `procQI` (each round `Q_p ∘ H0^{⊗} ∘ J_{-E}`, the layer computed by
  Proposition 14's procedure as in `GlueError.layerQ_eq_prop14`): **`opp_error`**.
* §4 **`prop18_error_full`**: forward transforms of two disk arrays (computed by `procQ`),
  normalized pointwise product `P(x,z) = x z / r`, truncation `Q_p`, computed opposite transform:
  the result is within `(3ℓ + 1) √2 2^{-p}` of `M⁻¹ M_r(f, g)` (every coefficient, every valid
  address), where `M_r(f,g) = (f ∗ g)/(rM)` is the normalized cyclic convolution — all
  approximation hypotheses of `Synth.prop18_error` discharged; **`prop18_scaled_full`** after the
  exact scaling by `M`.
-/

set_option linter.unusedSectionVars false
set_option linter.unusedSimpArgs false

namespace GlueProp18

open Finset Butterfly AModel Synth GlueLayout GlueP14 GlueError

variable {R : Type*} [CommRing R] [Algebra ℂ R] (y : Rˣ) {D : ℕ}

/-! ## 1. Inverse twiddles and butterflies -/

/-- The inverse twiddle of axis `i` at slot `h`. -/
noncomputable def twidI (ℓ h : ℕ) (i : Fin D) (z : Arr R D) (x : Fin D → ℕ) : R :=
  yp y (-twE ℓ h (x i)) * z x

/-- All inverse twiddles of a list of axes. -/
noncomputable def twidIAll (ℓ h : ℕ) (l : List (Fin D)) (z : Arr R D) (x : Fin D → ℕ) : R :=
  yp y (-(l.map fun i => twE ℓ h (x i)).sum) * z x

/-! ## 2. The opposite procedure on the tape -/

variable {sh : Shape} {a : Fin D → ℕ} (L : CoordLayout sh a)

/-- One opposite round on the tape: `J_{-E}`, then the layer `H0^{⊗}`. -/
noncomputable def roundLI (ℓ h : ℕ) (P : Finset (Fin D)) (Sb : SelBits sh {i // i ∈ P})
    (xs : List R) : List R :=
  selOp Sb (Butterfly.tens H0) (twL y sh (fun j => -roundEx L ℓ h P j) xs)

/-- The opposite procedure: rounds `h = 0, 1, …, n-1`. -/
noncomputable def procLI (ℓ : ℕ) (P : ℕ → Finset (Fin D))
    (Sb : (h : ℕ) → SelBits sh {i // i ∈ P h}) : ℕ → List R → List R
  | 0, xs => xs
  | n + 1, xs => roundLI y L ℓ n (P n) (Sb n) (procLI ℓ P Sb n xs)

/-! ## 3. Generic error chains for list procedures; the computed opposite procedure -/

variable {r : ℕ} {C : CoeffModel y r}

/-- The computed opposite round `Q_p ∘ H0^{⊗} ∘ J_{-E}`. -/
noncomputable def compRI (C : CoeffModel y r) (p : ℕ) {ι : Type} [Fintype ι] [DecidableEq ι]
    (Sb : SelBits sh ι) (Ex : ℕ → ℤ) (xs : List R) : List R :=
  layerQ C p Sb (twL y sh (fun j => -Ex j) xs)

/-- The computed opposite procedure (rounds `h = 0, …, n-1`). -/
noncomputable def procQI (C : CoeffModel y r) (p : ℕ) (ℓ : ℕ) (P : ℕ → Finset (Fin D))
    (Sb : (h : ℕ) → SelBits sh {i // i ∈ P h}) (n : ℕ) (xs : List R) : List R :=
  (List.range n).foldl (fun u k => compRI y C p (Sb k) (roundEx L ℓ k (P k)) u) xs

section OppMaps

variable {ι : Type} [Fintype ι] [DecidableEq ι] (Sb : SelBits sh ι) (Ex : ℕ → ℤ)

end OppMaps

/-! ## 4. Proposition 18 -/

section Prop18

/-- The normalized pointwise product `P(x, z) = x z / r` on arrays. -/
noncomputable def PP (C : CoeffModel y r) {N : ℕ} (x z : CArr C N) : CArr C N :=
  fun j => ((r : ℂ)⁻¹) • ((x : Fin N → R) j * (z : Fin N → R) j)

/-- `Q_p` on every record of an array. -/
noncomputable def QQ (C : CoeffModel y r) (p : ℕ) {N : ℕ} (w : CArr C N) : CArr C N :=
  fun j => QpR C p ((w : Fin N → R) j)

variable {ℓ : ℕ} {Sb : (h : ℕ) → SelBits sh {i // i ∈ partAxes a h}}

end Prop18

/-! ## 5. Proposition 18 on the paper's layout -/

section Paper

end Paper

end GlueProp18

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]

end Ring

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

section Rank

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

/-- Rank of a rational matrix, as a rational number. -/
noncomputable abbrev rk (E : Matrix n n ℚ) : ℚ := (E.rank : ℚ)

end Rank

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

section Stage

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

/-- Relations between the stage projections: `α` onto `P ⊗ F ⊗ Q`, `A` onto `A ⊗ F ⊗ Q`,
`τ t` onto the slot-`j` triple line; `Nb` the neighbour relation; `a = dim A`, `h = dim F`. -/
structure SRel (α A : Matrix n n ℚ) (τ : ι → Matrix n n ℚ) (Nb : ι → ι → Prop) (h a : ℚ) :
    Prop where
  αα : α * α = α
  AA : A * A = A
  Aα : A * α = α
  αA : α * A = α
  ττ : ∀ t, τ t * τ t = τ t
  τα : ∀ t, Commute (τ t) α
  τA : ∀ t, Commute (τ t) A
  nb : ∀ s t, Nb s t → τ s * τ t = 0
  trα : trace α = h
  trA : trace A = a * h
  trατ : ∀ t, trace (α * τ t) = 1
  trAτ : ∀ t, trace (A * τ t) = a

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

namespace SRel

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

end SRel

/-- The label of the gate at time `k` of table (6), with `τ` the gate's triple projection
(`B ⊗ ⟨t⟩`, `B ⊗ F`, `(B ⊗ F) ⊥ (P ⊗ ⟨t⟩)`, `A ⊗ F`, `B ⊗ F`, `(B ⊗ F) ⊥ (P ⊗ t^⊥)`,
`A ⊗ F`, `A ⊗ F`, all tensored with `Q`). -/
def labK (α A τ : Matrix n n ℚ) : ℕ → Matrix n n ℚ
  | 0 => (A - α) * τ
  | 1 => A - α
  | 2 => A - α + α * τ
  | 3 => A
  | 4 => A - α
  | 5 => A - α * τ
  | _ => A

namespace SRel

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

end SRel

end Stage

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

section Concrete

variable {h : ℕ}

/-- Index set of `F^{⊗3}`. -/
abbrev Cube (h : ℕ) := Fin h × Fin h × Fin h

/-- The `G`-orthogonal projection onto the triple line `⟨t_S⟩`: `½ t_S (G t_S)ᵀ`. -/
noncomputable def piM (S : Finset (Fin h)) : Matrix (Fin h) (Fin h) ℚ :=
  (2 : ℚ)⁻¹ • vecMulVec (NetLabels.ind ℚ S) (bitGram ℚ h *ᵥ NetLabels.ind ℚ S)

/-- Triple Kronecker product on `Fin h × (Fin h × Fin h)`. -/
def kr3 (X Y Z : Matrix (Fin h) (Fin h) ℚ) : Matrix (Cube h) (Cube h) ℚ := X ⊗ₖ (Y ⊗ₖ Z)

/-- `P ⊗ F ⊗ Q` at stage `j` (0-indexed) for the bank with fixed triples `S₁, S₂`. -/
noncomputable def αM (j : Fin 3) (S₁ S₂ : Finset (Fin h)) : Matrix (Cube h) (Cube h) ℚ :=
  if j = 0 then kr3 1 (piM S₁) (piM S₂) else if j = 1 then kr3 (piM S₁) 1 (piM S₂)
  else kr3 (piM S₁) (piM S₂) 1

/-- `A ⊗ F ⊗ Q` at stage `j`. -/
noncomputable def AM (j : Fin 3) (S₁ S₂ : Finset (Fin h)) : Matrix (Cube h) (Cube h) ℚ :=
  if j = 0 then kr3 1 (piM S₁) (piM S₂) else if j = 1 then kr3 1 1 (piM S₂) else kr3 1 1 1

/-- `⟨t⟩` in slot `j`. -/
noncomputable def τM (j : Fin 3) (S : Finset (Fin h)) : Matrix (Cube h) (Cube h) ℚ :=
  if j = 0 then kr3 (piM S) 1 1 else if j = 1 then kr3 1 (piM S) 1 else kr3 1 1 (piM S)

/-- The pure-tensor line `U_a = ⟨t_{a₁} ⊗ t_{a₂} ⊗ t_{a₃}⟩`. -/
noncomputable def uM (S₁ S₂ S₃ : Finset (Fin h)) : Matrix (Cube h) (Cube h) ℚ :=
  kr3 (piM S₁) (piM S₂) (piM S₃)

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`. -/

section Boundary

variable (S₁ S₂ S₃ : Finset (Fin h))

end Boundary

end Concrete

end NetProp7

end

section
-- Source module: Solutions.NetProp7Sum
/-!
# Prop. 7, part 5: the labelled network and its rank sum

Labels of table (6) on the gates of `named7` (`labG`), terminal labels `MinL`, `MoutL`
(sources `X_a ↦ −P_{U_a}`, otherwise `0`; sinks `Y_a ↦ P_{U_a^⊥} = 1 − P_{U_a}`, otherwise `1`),
and the per-wire rank sums (Lemma 6):
`X_a ↦ m`, `Y_a ↦ m − 1`, side wire `↦ m`, central wire `↦ m + 2h`.
-/

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

namespace NetProp7

open Matrix Finset AModel NetScalar NetLabels
open scoped Kronecker

variable {h : ℕ} {T : Type*} [Fintype T] [DecidableEq T] (ind : T → Finset (Fin h))

/-- Physical time of row `r` at stage `j` (reversed at stage 2). -/
def time (j : Fin 3) (r : Fin 8) : ℕ := if j = 1 then 7 - r.val else r.val

/-- Triple projection of a gate name's triple (`0` for the central gates). -/
noncomputable def τo (j : Fin 3) : Option T → Matrix (Cube h) (Cube h) ℚ
  | none => 0
  | some t => τM j (ind t)

/-- **Gate labels (table (6))**, by gate name. -/
noncomputable def labG : NetScalar.GName T → Matrix (Cube h) (Cube h) ℚ
  | (j, p, (r, o)) => labK (αM j (ind p.1) (ind p.2)) (AM j (ind p.1) (ind p.2)) (τo ind j o)
      (NetProp7.time j r)

/-- The labelled gates. -/
noncomputable def gatesL : List (NGate (NetScalar.Wr ind) (ZMod 2) (Matrix (Cube h) (Cube h) ℚ)) :=
  NetScalar.labelled (labG ind) (named7 ind)

/-- `P_{U_a}`. -/
noncomputable def uA (a : T × T × T) : Matrix (Cube h) (Cube h) ℚ :=
  uM (ind a.1) (ind a.2.1) (ind a.2.2)

/-- Source labels: `X_a ↦ −P_{U_a}`, all other sources `0`. -/
noncomputable def MinL : NetScalar.Wr ind → Matrix (Cube h) (Cube h) ℚ
  | Sum.inl a => -NetProp7.uA ind a
  | Sum.inr _ => 0

/-- Sink labels: `Y_a ↦ 1 − P_{U_a}`, all other sinks `1`. -/
noncomputable def MoutL : NetScalar.Wr ind → Matrix (Cube h) (Cube h) ℚ
  | Sum.inl _ => 1
  | Sum.inr (Sum.inl a) => 1 - NetProp7.uA ind a
  | Sum.inr (Sum.inr _) => 1

variable (hcard : ∀ t, (ind t).card = 3)
include hcard

omit hcard in
/-- The wire count `W = 2v³ + 3v² (z + h)`. -/
lemma card_Wr : (Fintype.card (NetScalar.Wr ind) : ℚ) = 2 * (Fintype.card T : ℚ) ^ 3 +
    3 * (Fintype.card T : ℚ) ^ 2 * ((Fintype.card (NetScalar.Nb ind) : ℚ) + h) := by
  simp only [Fintype.card_sum, Fintype.card_prod, Fintype.card_fin]
  push_cast
  ring

end NetProp7

end

section
-- Source module: Solutions.NetProp7Circuit
/-!
# Prop. 7, part 6: the rational interface as a `QCircuit`

Reindex the wires `Wr ind ≃ Fin W` (`W = |Wr ind|`) and the label space
`Fin h × Fin h × Fin h ≃ Fin (h ^ 3)` (`m = h³`) to obtain `bitQC ind : QCircuit (ZMod 2) m W`.
`prop7_interface`: every gate is OK, the scalar circuit routes `w ↦ ρ w`,
`M_sink(ρ w) − M_source(w) = 1`, and the rational rank sum is `W m − N + 2L`.
-/

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

namespace NetProp7

open Matrix Finset AModel NetScalar AModelRat AModelFac

variable {h : ℕ}

/-- `Fin h × Fin h × Fin h ≃ Fin (h ^ 3)`. -/
def cubeEquiv (h : ℕ) : Cube h ≃ Fin (h ^ 3) :=
  ((Equiv.refl (Fin h)).prodCongr finProdFinEquiv).trans
    (finProdFinEquiv.trans (finCongr (by ring)))

/-- Reindexing of labels to `QMat (h ^ 3)`. -/
noncomputable def φC (h : ℕ) : Matrix (Cube h) (Cube h) ℚ →+ QMat (h ^ 3) :=
  (Matrix.reindexLinearEquiv ℚ ℚ (cubeEquiv h) (cubeEquiv h)).toLinearMap.toAddMonoidHom

variable {T : Type*} [Fintype T] [DecidableEq T] (ind : T → Finset (Fin h))

/-- The wire equivalence. -/
noncomputable def eW : NetScalar.Wr ind ≃ Fin (Fintype.card (NetScalar.Wr ind)) := Fintype.equivFin _

/-- **The bit network of Prop. 7 as a circuit with rational labels.** -/
noncomputable def bitQC : QCircuit (ZMod 2) (h ^ 3) (Fintype.card (NetScalar.Wr ind)) where
  gates := (gatesL ind).map (trG (NetProp7.eW ind) (φC h))
  Min w := φC h (MinL ind ((NetProp7.eW ind).symm w))
  Mout w := φC h (MoutL ind ((NetProp7.eW ind).symm w))
  ρ w := NetProp7.eW ind (NetScalar.ρ ind ((NetProp7.eW ind).symm w))

variable (hcard : ∀ t, (ind t).card = 3) (hinj : Function.Injective ind)
include hcard hinj

end NetProp7

end

section
-- Source module: Solutions.NetProp7Num
/-!
# Prop. 7, part 7: the concrete bit network (`h = 100`) and Prop. 11

`T₀` = card-3 subsets of `Fin 100` (`v = 161700`), each with `z_b = 3·C(97,2) = 13968`
neighbours, `W_b = 177176569091445000000` wires, `m = 10⁶`, and the rank sum
`s_b = W_b m − N + 2L_b = 177176569088785861287000000`.
With `τ = 1 − 2^{−50}`: `s_b / W_b < m^τ` (`hs_bit`), since `m^τ ≥ m (1 − 20·2^{−50})`
(`log m < 20`). Then `prop7_prop11` applies `AModelRat.prop11_ratLabels`.
-/

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

namespace NetProp7

open Matrix Finset AModel NetScalar AModelRat AModelFac

/-! ## 1. Counting -/

/-- Neighbours of a triple: `#{U : |U| = 3, |S ∩ U| = 1} = 3 · C(n − 3, 2)`. -/
lemma count_nb {n : ℕ} (S : Finset (Fin n)) (hS : S.card = 3) :
    (univ.filter fun U : Finset (Fin n) => U.card = 3 ∧ (S ∩ U).card = 1).card =
      3 * (n - 3).choose 2 := by
  have hc : (S ×ˢ powersetCard 2 Sᶜ).card = 3 * (n - 3).choose 2 := by
    rw [card_product, card_powersetCard, card_compl, hS, Fintype.card_fin]
  rw [← hc]
  symm
  apply Finset.card_bij (fun x _ => insert x.1 x.2)
  · rintro ⟨x, D⟩ hx
    simp only [mem_product, mem_powersetCard] at hx
    obtain ⟨hxS, hDS, hD⟩ := hx
    have hxD : x ∉ D := fun h => (Finset.mem_compl.1 (hDS h)) hxS
    simp only [mem_filter, mem_univ, true_and]
    refine ⟨by rw [card_insert_of_notMem hxD, hD], ?_⟩
    rw [Finset.card_eq_one]
    refine ⟨x, ?_⟩
    ext y
    simp only [mem_inter, mem_insert, mem_singleton]
    constructor
    · rintro ⟨hy, rfl | hy'⟩
      · rfl
      · exact absurd hy (Finset.mem_compl.1 (hDS hy'))
    · rintro rfl; exact ⟨hxS, Or.inl rfl⟩
  · rintro ⟨x, D⟩ hx ⟨x', D'⟩ hx' e
    simp only [mem_product, mem_powersetCard] at hx hx'
    have key : ∀ (x : Fin n) (D : Finset (Fin n)), x ∈ S → D ⊆ Sᶜ →
        S ∩ insert x D = {x} ∧ insert x D \ S = D := by
      intro x D hxS hDS
      constructor
      · ext y
        simp only [mem_inter, mem_insert, mem_singleton]
        constructor
        · rintro ⟨hy, rfl | hy'⟩
          · rfl
          · exact absurd hy (Finset.mem_compl.1 (hDS hy'))
        · rintro rfl; exact ⟨hxS, Or.inl rfl⟩
      · ext y
        simp only [mem_sdiff, mem_insert]
        constructor
        · rintro ⟨rfl | hy, hyS⟩
          · exact absurd hxS hyS
          · exact hy
        · intro hy; exact ⟨Or.inr hy, Finset.mem_compl.1 (hDS hy)⟩
    have k1 := key x D hx.1 hx.2.1
    have k2 := key x' D' hx'.1 hx'.2.1
    simp only at e
    rw [e] at k1
    have hxx : x = x' := by
      have := k1.1.symm.trans k2.1
      exact Finset.singleton_injective this
    have hDD : D = D' := k1.2.symm.trans k2.2
    rw [hxx, hDD]
  · intro U hU
    simp only [mem_filter, mem_univ, true_and] at hU
    obtain ⟨hU3, hU1⟩ := hU
    obtain ⟨x, hx⟩ := Finset.card_eq_one.1 hU1
    have hxSU : x ∈ S ∩ U := by rw [hx]; exact mem_singleton_self x
    rw [mem_inter] at hxSU
    refine ⟨(x, U \ S), ?_, ?_⟩
    · simp only [mem_product, mem_powersetCard]
      refine ⟨hxSU.1, fun y hy => Finset.mem_compl.2 (Finset.mem_sdiff.1 hy).2, ?_⟩
      have := Finset.card_sdiff_add_card_inter U S
      rw [Finset.inter_comm, hU1, hU3] at this
      omega
    · ext y
      simp only [mem_insert, mem_sdiff]
      constructor
      · rintro (rfl | ⟨hy, -⟩)
        · exact hxSU.2
        · exact hy
      · intro hy
        by_cases hyS : y ∈ S
        · left
          have : y ∈ S ∩ U := mem_inter.2 ⟨hyS, hy⟩
          rw [hx] at this
          exact mem_singleton.1 this
        · exact Or.inr ⟨hy, hyS⟩

/-- The triples of `Fin 100`. -/
abbrev T₀ := {S : Finset (Fin 100) // S.card = 3}

/-- The indicator map of the triple family. -/
def ind₀ : NetProp7.T₀ → Finset (Fin 100) := Subtype.val

lemma card_T₀ : Fintype.card NetProp7.T₀ = 161700 := by
  rw [Fintype.card_finset_len, Fintype.card_fin, Nat.choose_eq_descFactorial_div_factorial]
  norm_num [Nat.descFactorial, Nat.factorial]

lemma card_nbr (S : NetProp7.T₀) :
    Fintype.card {U : NetProp7.T₀ // (NetProp7.ind₀ S ∩ NetProp7.ind₀ U).card = 1} = 13968 := by
  show Fintype.card {U : NetProp7.T₀ // (S.1 ∩ U.1).card = 1} = 13968
  rw [Fintype.card_congr (Equiv.subtypeSubtypeEquivSubtypeInter
    (fun U : Finset (Fin 100) => U.card = 3) (fun U => (S.1 ∩ U).card = 1)),
    Fintype.card_subtype, count_nb S.1 S.2, Nat.choose_eq_descFactorial_div_factorial]
  norm_num [Nat.descFactorial, Nat.factorial]

lemma card_Nb₀ : Fintype.card (NetScalar.Nb NetProp7.ind₀) = 161700 * 13968 := by
  rw [Fintype.card_subtype, Finset.card_filter, Fintype.sum_prod_type]
  have : ∀ S : NetProp7.T₀, (∑ U : NetProp7.T₀, if (NetProp7.ind₀ (S, U).1 ∩ NetProp7.ind₀ (S, U).2).card = 1 then 1 else 0) =
      13968 := by
    intro S
    rw [← card_nbr S, Fintype.card_subtype, Finset.card_filter]
  simp only [this, Finset.sum_const, Finset.card_univ, NetProp7.card_T₀, smul_eq_mul]

/-! ## 2. The numbers -/

lemma card_Wr₀ : Fintype.card (NetScalar.Wr NetProp7.ind₀) = 177176569091445000000 := by
  have := card_Wr NetProp7.ind₀
  rw [NetProp7.card_T₀, NetProp7.card_Nb₀] at this
  have h2 : (Fintype.card (NetScalar.Wr NetProp7.ind₀) : ℚ) = ((177176569091445000000 : ℕ) : ℚ) := by
    rw [this]; norm_num
  exact Nat.cast_injective h2

instance : NeZero (Fintype.card (NetScalar.Wr NetProp7.ind₀)) := ⟨by rw [NetProp7.card_Wr₀]; norm_num⟩

/-! ## 3. Proposition 7 and Proposition 11 for the bit network -/

end NetProp7

end

section
-- Source module: Solutions.ResampleTensor
/-!
# §8.2 Lemma 20: tensor interface, padded box, linewise implementation

* `lemma20_tensor`: tensoring the one-dimensional identities (33) gives (35),
  `R F_s = 2^γ B₀ Q F_t A` with `γ = 2dα²`, `R = ⊗ P_{s_i}`, `Q = ⊗ P_{t_i}`, `‖A‖, ‖B₀‖ ≤ 1`.
* `axisOp` / `tensOpI`: the padded box keeps its full shape; applying the padded line kernels of
  the axes one at a time (in any order) equals the tensor kernel (`axis_fold_eq_tensOp`), and
  with zero padding outside `∏ [0, s_i)` this is exactly the tensor map `A`
  (`tensOp_pad_eq_tens`).
* `approx_iterate`: `d` contraction stages with errors `< E` each give error `< d E`.
* cost bookkeeping: `∑_i (T/t_i)·(t_i X) = d T X`, line count `∑ T/t_i ≤ 2dT/r`.
-/

open Finset Complex

namespace IntMul.OpenAI.RT

variable {d : ℕ}

/-! ### Kernel tensor (copied from the base thread's `Thm41.lean`, renamed) -/

noncomputable def tens {s t : Fin d → ℕ} [∀ i, NeZero (s i)]
    (M : (i : Fin d) → ZMod (t i) → ZMod (s i) → ℂ) (u : ((i : Fin d) → ZMod (s i)) → ℂ) : ((i : Fin d) → ZMod (t i)) → ℂ :=
  fun k => ∑ j, (∏ i, M i (k i) (j i)) * u j

lemma tens_add {s t : Fin d → ℕ} [∀ i, NeZero (s i)]
    (M : (i : Fin d) → ZMod (t i) → ZMod (s i) → ℂ) (u v : ((i : Fin d) → ZMod (s i)) → ℂ) :
    IntMul.OpenAI.RT.tens M (u + v) = IntMul.OpenAI.RT.tens M u + IntMul.OpenAI.RT.tens M v := by
  ext k; simp only [IntMul.OpenAI.RT.tens, Pi.add_apply, mul_add, Finset.sum_add_distrib]

lemma tens_smul' {s t : Fin d → ℕ} [∀ i, NeZero (s i)] (c : ℂ)
    (M : (i : Fin d) → ZMod (t i) → ZMod (s i) → ℂ) (u : ((i : Fin d) → ZMod (s i)) → ℂ) :
    IntMul.OpenAI.RT.tens M (c • u) = c • IntMul.OpenAI.RT.tens M u := by
  ext k; simp only [IntMul.OpenAI.RT.tens, Pi.smul_apply, smul_eq_mul, Finset.mul_sum]
  refine Finset.sum_congr rfl (fun j _ => ?_); ring

noncomputable def tensCLM {s t : Fin d → ℕ} [∀ i, NeZero (s i)] [∀ i, NeZero (t i)]
    (M : (i : Fin d) → ZMod (t i) → ZMod (s i) → ℂ) :
    (((i : Fin d) → ZMod (s i)) → ℂ) →L[ℂ] (((i : Fin d) → ZMod (t i)) → ℂ) :=
  LinearMap.toContinuousLinearMap ⟨⟨IntMul.OpenAI.RT.tens M, tens_add M⟩, fun c u => tens_smul' c M u⟩

@[simp] lemma tensCLM_apply {s t : Fin d → ℕ} [∀ i, NeZero (s i)] [∀ i, NeZero (t i)]
    (M : (i : Fin d) → ZMod (t i) → ZMod (s i) → ℂ) (u) : tensCLM M u = IntMul.OpenAI.RT.tens M u := rfl

/-! ### Multidimensional transforms and the retained permutations -/

/-- Normalized multidimensional transform `F_s` (negative sign). -/
noncomputable def dftM (s : Fin d → ℕ) [∀ i, NeZero (s i)] (u : ((i : Fin d) → ZMod (s i)) → ℂ) :
    ((i : Fin d) → ZMod (s i)) → ℂ :=
  fun k => (∏ i, (s i : ℂ))⁻¹ * ∑ j, (∏ i, (ZMod.stdAddChar (-(j i * k i)) : ℂ)) * u j

/-- `R = ⊗ P_{s_i}`: `(R w)_k = w_{(t_i k_i)_i}`. -/
def Rperm (s t : Fin d → ℕ) (w : ((i : Fin d) → ZMod (s i)) → ℂ) :
    ((i : Fin d) → ZMod (s i)) → ℂ :=
  fun k => w (fun i => (t i : ZMod (s i)) * k i)

/-! ### The padded box: axis maps applied one at a time -/

section padded
variable {n : Fin d → ℕ}

end padded

/-! ### Errors and costs of the linewise implementation -/

end IntMul.OpenAI.RT

end

section
-- Source module: Solutions.ResampleChirp
/-!
# §8.3 Lemma 21: chirp identity (36) and permutation cancellation (37)

* `chirp_periodic`: `a_j = exp(-π i Σ s_i j_i²/t_i)` has period `t_i` in coordinate `i`
  (each `t_i` even).
* `lemma21_chirp` (36): `Q F_t u = ā · (a ∗ (ā · u)) / T`.
* `lemma21_cancel` (37): `R F_s⁺ ((R F_s u)·(R F_s v)) = (u ∗ v)/S²` for `t_i` units mod `s_i`.
* `conj_dftM`: conjugating input and output of `F_s` gives `F_s⁺` (also after `R`).
* `chirp_phase_numerator` (§9.5): the chirp phase is `exp(2πi N/(2r))` with
  `N = -s j² (r/t)`.
-/

open Finset Complex Real

namespace IntMul.OpenAI.RC

open IntMul.OpenAI.RT

variable {d : ℕ}

/-! ### One-dimensional chirp factor -/

/-! ### Multidimensional chirp and identity (36) -/

/-! ### Permutation cancellation (37) -/

section cancel
variable (s : Fin d → ℕ) [∀ i, NeZero (s i)]

/-- `e(t, a) = ∏ᵢ exp(2πi tᵢ aᵢ / sᵢ)` (from the base thread's `Conv.lean`). -/
noncomputable def ee (t a : Π i, ZMod (s i)) : ℂ := ∏ i, ZMod.stdAddChar (t i * a i)

/-- Normalized positive-sign transform `F_s⁺`. -/
noncomputable def dftP (u : ((i : Fin d) → ZMod (s i)) → ℂ) : ((i : Fin d) → ZMod (s i)) → ℂ :=
  fun k => (∏ i, (s i : ℂ))⁻¹ * ∑ j, (∏ i, (ZMod.stdAddChar (j i * k i) : ℂ)) * u j

/-- Cyclic convolution on `∏ ℤ/s_i`. -/
def cconv (u v : ((i : Fin d) → ZMod (s i)) → ℂ) : ((i : Fin d) → ZMod (s i)) → ℂ :=
  fun j => ∑ k, u k * v (j - k)

variable (t : Fin d → ℕ)

/-- `(R⁻¹ w)_j = w_{(t_i⁻¹ j_i)}`. -/
noncomputable def Rinv (w : ((i : Fin d) → ZMod (s i)) → ℂ) : ((i : Fin d) → ZMod (s i)) → ℂ :=
  fun j => w (fun i => (t i : ZMod (s i))⁻¹ * j i)

/-- The unit dilation used by `R`, as an equivalence of index sets. -/
noncomputable def dil (hcop : ∀ i, Nat.Coprime (s i) (t i)) :
    ((i : Fin d) → ZMod (s i)) ≃ ((i : Fin d) → ZMod (s i)) :=
  Equiv.piCongrRight (fun i =>
    { toFun := fun x => (t i : ZMod (s i)) * x
      invFun := fun x => (t i : ZMod (s i))⁻¹ * x
      left_inv := fun x => by
        simp only [← mul_assoc]
        rw [ZMod.inv_mul_of_unit _ ((ZMod.isUnit_iff_coprime _ _).2 (hcop i).symm), one_mul]
      right_inv := fun x => by
        simp only [← mul_assoc]
        rw [ZMod.coe_mul_inv_eq_one _ (hcop i).symm, one_mul] })

end cancel

/-! ### §9.5: chirp phase numerators modulo `2r` -/

end IntMul.OpenAI.RC

end