Round-six κ development, definitions part 5

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

import Definitions.Def_IntMul_Kappa_R6_Defs4
import Mathlib
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_KappaJainData

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

section
-- Source module: Solutions.R6BitNBObst
/-!
# Round six, bit side: the label route `prop11H_labels` admits **no saving**

`prop11H_labels` (R6BitProp11) derives `C.OK` from `EdgesOK`, `LabOK`, `ScalarOK`: every gate
touches wires with *equal* frame labels, and every role ends at label `swapMat`. This file proves
that these hypotheses force the total child width to be at least `W m`:

* the `H × D` block `hdB` of a frame matrix is subadditive in rank under products
  (`rank_hdB_mul_le`), vanishes on lower triangular Bruhat factors and on `1`, and has rank `m`
  on `swapMat`;
* an edge `E₁ σ E₂` therefore has `rank hdB ≤ #transpositions ≤ Σ run widths`
  (`rank_hdB_edgeMat_le`);
* along each role wire the labels go from `1` to `swapMat`, so each of the `W` (distinct, by
  `ScalarOK`) role wires carries edges of total width `≥ m` (`widths_sum_ge`).

Consequently `histMoment C.hist m τ ≥ W` for every `0 < τ ≤ 1` (`labels_no_saving`): the
hypotheses of `prop11H_labels` are **jointly inconsistent** (`prop11H_labels_vacuous`), and in
particular no network with the histogram `Jain.bitR6` (rank sum `W m − 1344189`) satisfies them
(`no_bitR6_labels`).

The real two-stage network escapes this because its data outputs are sums of terms at
*different* frames (`B = F x + E y`, fixed by the copy correction `T F = E`), which the
single-label invariant cannot express. See `R6BitNBFormal` for the replacement calculus.
-/

set_option linter.unusedSectionVars false

namespace IntMul.Kappa.R6.Bit

open AModel AModelFac Matrix

/-! ## Blocks of `2m × 2m` matrices -/

section Blocks

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

/-- The `H × D` (upper right) block. -/
def hdB (M : Matrix (Fin (m + m)) (Fin (m + m)) K) : Matrix (Fin m) (Fin m) K :=
  fun i j => M (Fin.castAdd m i) (Fin.natAdd m j)

/-- The `H × H` block. -/
def hhB (M : Matrix (Fin (m + m)) (Fin (m + m)) K) : Matrix (Fin m) (Fin m) K :=
  fun i j => M (Fin.castAdd m i) (Fin.castAdd m j)

/-- The `D × D` block. -/
def ddB (M : Matrix (Fin (m + m)) (Fin (m + m)) K) : Matrix (Fin m) (Fin m) K :=
  fun i j => M (Fin.natAdd m i) (Fin.natAdd m j)

end Blocks

/-! ## Edges and label paths -/

section Paths

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

/-- Number of transpositions of an edge. -/
def pivCnt (e : Edge m) : ℕ := (e.runs.flatMap (runPiv m)).length

variable {q : ℕ} [Fact q.Prime]

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

/-- Total transposition count of the edges acting on wire `w`. -/
def edgeCnt : List (Instr Wr R m) → Wr → ℕ
  | [], _ => 0
  | .gate _ _ :: l, w => edgeCnt l w
  | .edge w' e :: l, w => (if w' = w then pivCnt e else 0) + edgeCnt l w

end Paths

/-! ## The bound -/

namespace QHNet

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

end QHNet

end IntMul.Kappa.R6.Bit

end

section
-- Source module: Solutions.R6BitNBPrime
/-!
# Round six, bit network: good primes

Finitely many rationals have denominators coprime to every power of every prime `q > q₀`, and the
nonzero ones are units mod `q ^ f`. Consequently a finite set of edges with `EdgeQ` data
is `EdgeOK (q ^ f)` for all large primes `q` and all `f`.
-/

namespace IntMul.Kappa.R6.Bit.NB

open Matrix Finset AModelFac

/-- All entries of finitely many matrices. -/
noncomputable def entriesOf {ι κ : Type*} [Fintype ι] [Fintype κ] (S : Finset (Matrix ι κ ℚ)) :
    Finset ℚ := by
  classical
  exact S.biUnion fun A => Finset.univ.image fun p : ι × κ => A p.1 p.2

end IntMul.Kappa.R6.Bit.NB

end