inductive LGate

def LGate.compile : LGate → List Rot
  | .X q        => (xGate q).flatten
  | .Y q        => (yGate q).flatten
  | .Z q        => (zGate q).flatten
  | .H q        => (hGate q).flatten
  | .S q        => (sGate q).flatten
  | .Sdg q      => (sDag q).flatten
  | .T q        => (tGate q).flatten
  | .Tdg q      => (tDag q).flatten
  | .CNOT c t   => (cnotGate c t).flatten
  | .CCZ a b c  => (cczGate a b c).flatten
  | .CCX a b c  => (hGate c).flatten ++ (cczGate a b c).flatten ++ (hGate c).flatten

def compileNaive (gs : List LGate) : List Rot

def compileScheduled (gs : List LGate) : RotProg

theorem compileScheduled_denote (n : Nat) (gs : List LGate)
    (h : ∀ r ∈ compileNaive gs,
          sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ n) :
    RotProg.denote n (compileScheduled gs) = seqDenote n (compileNaive gs)

theorem compileScheduled_countPi8 (gs : List LGate) :
    countPi8 (compileScheduled gs)
      = (compileNaive gs).countP (fun r => r.angle == RAngle.piEighth)

theorem compileScheduled_depth_le (gs : List LGate) :
    rotDepth (compileScheduled gs) ≤ (compileNaive gs).length

def demoCircuit : List LGate

example : ∀ r ∈ compileNaive demoCircuit,
    sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ 2

example : (compileNaive demoCircuit).length = 5

example : rotDepth (compileScheduled demoCircuit) = 2

example : countPi8 (compileScheduled demoCircuit) = 2

example : RotProg.wf (compileScheduled demoCircuit) = true

example : (compileNaive [.CCX 0 1 2]).length = 13

example : rotDepth (compileScheduled [.CCX 0 1 2]) = 5

example : countPi8 (compileScheduled [.CCX 0 1 2]) = 7

example : rotDepth (compileScheduled [.CCX 0 1 2, .CCX 3 4 5]) = 5

example : countPi8 (compileScheduled [.CCX 0 1 2, .CCX 3 4 5]) = 14

def sort3 (a b c : Nat) : Nat × Nat × Nat

def gateRots : Gate → List Rot
  | .I          => []
  | .X q        => [⟨false, .piHalf, [⟨q, .x⟩]⟩]
  | .CX c t     => (cnotGate c t).flatten
  | .CCX a b t  =>
      (hGate t).flatten
        ++ (cczGate (sort3 a b t).1 (sort3 a b t).2.1 (sort3 a b t).2.2).flatten
        ++ (hGate t).flatten
  | .seq g h    => gateRots g ++ gateRots h

def gateRotSchedule (g : Gate) : RotProg

def opsOK : Gate → Bool
  | .I          => true
  | .X _        => true
  | .CX c t     => decide (c ≠ t)
  | .CCX a b t  => decide (a ≠ b) && decide (a ≠ t) && decide (b ≠ t)
  | .seq g h    => opsOK g && opsOK h

theorem gateRots_countPi8 (g : Gate) :
    (gateRots g).countP (fun r => r.angle == RAngle.piEighth) = Gate.tcount g

theorem gateRots_length (g : Gate) :
    (gateRots g).length
      = countX g + 3 * countCNOT g + 13 * countToffoli g

private theorem hGate_bounded (q : Nat) :
    ∀ r ∈ (hGate q).flatten,
      sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ q + 1

private theorem cnotGate_bounded (c t : Nat) (h : c ≠ t) :
    ∀ r ∈ (cnotGate c t).flatten,
      sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ max (c + 1) (t + 1)

private theorem cczGate_bounded (x y z : Nat) (hxy : x < y) (hyz : y < z) :
    ∀ r ∈ (cczGate x y z).flatten,
      sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ z + 1

theorem sort3_spec (a b t : Nat) (hab : a ≠ b) (hat : a ≠ t)
    (hbt : b ≠ t) :
    (sort3 a b t).1 < (sort3 a b t).2.1
      ∧ (sort3 a b t).2.1 < (sort3 a b t).2.2
      ∧ (sort3 a b t).2.2 + 1 ≤ max (max (a + 1) (b + 1)) (t + 1)

theorem gateRots_bounded (g : Gate) (hops : opsOK g = true) :
    ∀ r ∈ gateRots g,
      sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ width g

theorem gateRotSchedule_denote (n : Nat) (g : Gate)
    (hops : opsOK g = true) (hw : width g ≤ n) :
    RotProg.denote n (gateRotSchedule g) = seqDenote n (gateRots g)

theorem gateRotSchedule_countPi8 (g : Gate) :
    countPi8 (gateRotSchedule g) = Gate.tcount g

theorem gateRotSchedule_depth_le (g : Gate) :
    rotDepth (gateRotSchedule g) ≤ (gateRots g).length

example :  -- a MAJ-style fragment: CX;CX;CCX = 3+3+13 rotations, 7 of them T
    (gateRots (.seq (.CX 2 1) (.seq (.CX 2 0) (.CCX 0 1 2)))).length = 19

example :
    countPi8 (gateRotSchedule (.seq (.CX 2 1) (.seq (.CX 2 0) (.CCX 0 1 2)))) = 7

example :  -- operands distinct, fits in 3 qubits: the semantic theorem applies
    opsOK (.seq (.CX 2 1) (.seq (.CX 2 0) (.CCX 0 1 2))) = true
      ∧ width (.seq (.CX 2 1) (.seq (.CX 2 0) (.CCX 0 1 2))) ≤ 3

example :  -- CCX with operands in ANY order compiles (CCZ symmetric, sort₃)
    countPi8 (gateRotSchedule (.CCX 5 2 4)) = 7

def rot1 (neg : Bool) (a : RAngle) (k : PKind) (q : Nat) : RotProg

def tGate (q : Nat) : RotProg

def tDag  (q : Nat) : RotProg

def sGate (q : Nat) : RotProg

def sDag  (q : Nat) : RotProg

def zGate (q : Nat) : RotProg

def xGate (q : Nat) : RotProg

def yGate (q : Nat) : RotProg

def hGate (q : Nat) : RotProg

def mk2 (c : Nat) (kc : PKind) (t : Nat) (kt : PKind) : PauliProduct

def cnotGate (c t : Nat) : RotProg

def cczGate (a b c : Nat) : RotProg

def cczLayer (a b c : Nat) : RotProg

example : RotProg.wf (tGate 3) = true

example : RotProg.wf (hGate 0) = true

example : RotProg.wf (cnotGate 0 1) = true

example : RotProg.wf (cnotGate 5 2) = true

example : RotProg.wf (cczGate 0 1 2) = true

example : RotProg.wf (cczLayer 0 1 2) = true

example : countPi8 (tGate 0) = 1

example : countPi8 (hGate 0) = 0

example : countPi8 (cnotGate 0 1) = 0

example : countPi8 (cczGate 0 1 2) = 7

example : rotDepth (cczGate 0 1 2) = 7

example : rotDepth (cczLayer 0 1 2) = 1

example : countPi8 (cczLayer 0 1 2) = 7

def rotsBoundedB (n : Nat) (rs : List Rot) : Bool

theorem rotsBoundedB_cons {n : Nat} {r : Rot} {rs : List Rot}
    (h : rotsBoundedB n (r :: rs) = true) :
    (sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ n)
      ∧ rotsBoundedB n rs = true

theorem rotsBoundedB_cons_intro {n : Nat} {r : Rot} {rs : List Rot}
    (hr : sortedStrict r.axis = true) (hw : PauliProduct.width r.axis ≤ n)
    (h : rotsBoundedB n rs = true) : rotsBoundedB n (r :: rs) = true

inductive RuleApp

def applyHead : RuleApp → List Rot → Option (List Rot)
  | .swap _, r :: s :: rest =>
      if commF s.axis r.axis then some (s :: r :: rest) else none
  | .push _, r :: s :: rest =>
      if r.angle == .piQuarter && !(commF r.axis s.axis)
      then some (r.pushedBy s :: r :: rest) else none
  | .pushHalf _, r :: s :: rest =>
      if r.angle == .piHalf && !(commF r.axis s.axis)
      then some (Rot.pushedByHalf s :: r :: rest) else none
  | .cancel _, r :: s :: rest =>
      if s == r.inv then some rest else none
  | .merge _, r :: s :: rest =>

def applyRule (a : RuleApp) : List Rot → Option (List Rot)

def applyTrace : List RuleApp → List Rot → Option (List Rot)
  | [], rs => some rs
  | a :: t, rs => (applyRule a rs).bind (applyTrace t)

private theorem denote_merge_rot (n : Nat) (r : Rot) {b : RAngle}
    (hb : r.angle.doubled = some b) :
    Rot.denote n r * Rot.denote n r
      = Rot.denote n { r with angle

private theorem rotOf_two_pi {d : Type*} [DecidableEq d]
    (M : Matrix d d ℂ) : rotOf (2 * Real.pi) M = 1

private theorem rotOf_neg_two_pi {d : Type*} [DecidableEq d]
    (M : Matrix d d ℂ) : rotOf (-(2 * Real.pi)) M = 1

private theorem denote_merge_pi (n : Nat) (r : Rot) (hr : r.angle = .pi) :
    Rot.denote n r * Rot.denote n r = 1

theorem applyHead_sound (n : Nat) (a : RuleApp) (rs rs' : List Rot)
    (hb : rotsBoundedB n rs = true)
    (h : applyHead a rs = some rs') :
    seqDenote n rs = seqDenote n rs' ∧ rotsBoundedB n rs' = true

theorem applyRule_go_sound (n : Nat) (a : RuleApp) :
    ∀ (k : Nat) (rs rs' : List Rot),
      rotsBoundedB n rs = true →
      applyRule.go a k rs = some rs' →
      seqDenote n rs = seqDenote n rs' ∧ rotsBoundedB n rs' = true
  | 0, rs, rs', hb, h => applyHead_sound n a rs rs' hb h
  | k + 1, r :: rs, rs', hb, h =>

theorem applyRule_sound (n : Nat) (a : RuleApp) (rs rs' : List Rot)
    (hb : rotsBoundedB n rs = true)
    (h : applyRule a rs = some rs') :
    seqDenote n rs = seqDenote n rs' ∧ rotsBoundedB n rs' = true

theorem applyTrace_sound (n : Nat) :
    ∀ (t : List RuleApp) (rs rs' : List Rot),
      rotsBoundedB n rs = true →
      applyTrace t rs = some rs' →
      seqDenote n rs = seqDenote n rs' ∧ rotsBoundedB n rs' = true
  | [], rs, rs', hb, h =>

theorem gateRots_boundedB (g : FormalRV.Framework.Gate) (n : Nat)
    (hops : opsOK g = true) (hw : Resource.width g ≤ n) :
    rotsBoundedB n (gateRots g) = true

theorem optimized_schedule_applyNat (n : Nat) (g : FormalRV.Framework.Gate)
    (hops : opsOK g = true) (hw : Resource.width g ≤ n)
    (t : List RuleApp) (rs' : List Rot)
    (hcheck : applyTrace t (gateRots g) = some rs') :
    RotProg.denote n (scheduleList rs')
      = gphase g • applyMat n g

theorem optimized_scheduleK_applyNat (K n : Nat) (hK : 1 ≤ K)
    (g : FormalRV.Framework.Gate)
    (hops : opsOK g = true) (hw : Resource.width g ≤ n)
    (t : List RuleApp) (rs' : List Rot)
    (hcheck : applyTrace t (gateRots g) = some rs') :
    RotProg.denote n (scheduleListK K rs') = gphase g • applyMat n g
      ∧ layersLE K (scheduleListK K rs') = true

theorem rotOf_neg_axis (θ : ℝ) (M : Matrix m m ℂ) :
    rotOf θ (-M) = rotOf (-θ) M

theorem rot_quarter_push_neg {M N : Matrix m m ℂ} (hM : M * M = 1)
    (hMN : M * N = -(N * M)) (φ : ℝ) :
    rotOf (-(Real.pi / 4)) M * rotOf φ N
      = rotOf φ (Complex.I • (M * N)) * rotOf (-(Real.pi / 4)) M

theorem rot_half_push {M N : Matrix m m ℂ}
    (hMN : M * N = -(N * M)) (φ : ℝ) :
    rotOf φ N * rotOf (Real.pi / 2) M
      = rotOf (Real.pi / 2) M * rotOf (-φ) N

theorem rot_half_push_neg {M N : Matrix m m ℂ}
    (hMN : M * N = -(N * M)) (φ : ℝ) :
    rotOf φ N * rotOf (-(Real.pi / 2)) M
      = rotOf (-(Real.pi / 2)) M * rotOf (-φ) N

def Rot.pushedBy (r s : Rot) : Rot

def Rot.pushedByHalf (s : Rot) : Rot

private theorem theta_xor_true (ne : Bool) (a : RAngle)
    (ax ax' : PauliProduct) :
    Rot.theta ⟨ne ^^ true, a, ax'⟩ = -(Rot.theta ⟨ne, a, ax⟩)

private theorem theta_xor_false (ne : Bool) (a : RAngle)
    (ax ax' : PauliProduct) :
    Rot.theta ⟨ne ^^ false, a, ax'⟩ = Rot.theta ⟨ne, a, ax⟩

theorem axisMat_anticomm_of_not_commF (n : Nat) {P Q : PauliProduct}
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (h : commF P Q = false) :
    axisMat n P * axisMat n Q = -(axisMat n Q * axisMat n P)

theorem Rot.denote_push_delay (n : Nat) (r s : Rot)
    (hr : r.angle = .piQuarter)
    (hsr : sortedStrict r.axis = true)
    (hwr : PauliProduct.width r.axis ≤ n)
    (hss : sortedStrict s.axis = true)
    (hac : commF r.axis s.axis = false) :
    Rot.denote n s * Rot.denote n r
      = Rot.denote n r * Rot.denote n (r.pushedBy s)

theorem Rot.denote_push_half_delay (n : Nat) (r s : Rot)
    (hr : r.angle = .piHalf)
    (hsr : sortedStrict r.axis = true)
    (hwr : PauliProduct.width r.axis ≤ n)
    (hac : commF r.axis s.axis = false) :
    Rot.denote n s * Rot.denote n r
      = Rot.denote n r * Rot.denote n (Rot.pushedByHalf s)

private theorem layer_singleton (n : Nat) (x : Rot) :
    RotLayer.denote n [x] = Rot.denote n x

theorem denote_push_adjacent (n : Nat) (r s : Rot) (p : RotProg)
    (hr : r.angle = .piQuarter)
    (hsr : sortedStrict r.axis = true)
    (hwr : PauliProduct.width r.axis ≤ n)
    (hss : sortedStrict s.axis = true)
    (hac : commF r.axis s.axis = false) :
    RotProg.denote n ([r] :: [s] :: p)
      = RotProg.denote n ([r.pushedBy s] :: [r] :: p)

theorem denote_push_half_adjacent (n : Nat) (r s : Rot) (p : RotProg)
    (hr : r.angle = .piHalf)
    (hsr : sortedStrict r.axis = true)
    (hwr : PauliProduct.width r.axis ≤ n)
    (hac : commF r.axis s.axis = false) :
    RotProg.denote n ([r] :: [s] :: p)
      = RotProg.denote n ([Rot.pushedByHalf s] :: [r] :: p)

theorem denote_swap_adjacent (n : Nat) (r s : Rot) (p : RotProg)
    (hss : sortedStrict s.axis = true)
    (hws : PauliProduct.width s.axis ≤ n)
    (hc : commF s.axis r.axis = true) :
    RotProg.denote n ([r] :: [s] :: p)
      = RotProg.denote n ([s] :: [r] :: p)

theorem countAngle_push_adjacent (a : RAngle) (r s : Rot) (p : RotProg) :
    countAngle a ([r.pushedBy s] :: [r] :: p)
      = countAngle a ([r] :: [s] :: p)

theorem countPi8_push_adjacent (r s : Rot) (p : RotProg) :
    countPi8 ([r.pushedBy s] :: [r] :: p) = countPi8 ([r] :: [s] :: p)

theorem countRot_push_adjacent (r s : Rot) (p : RotProg) :
    countRot ([r.pushedBy s] :: [r] :: p) = countRot ([r] :: [s] :: p)

theorem rotDepth_push_adjacent (r s : Rot) (p : RotProg) :
    rotDepth ([r.pushedBy s] :: [r] :: p) = rotDepth ([r] :: [s] :: p)

example :
    (Rot.pushedBy ⟨false, .piQuarter, [⟨0, .z⟩]⟩
        ⟨false, .piEighth, [⟨0, .x⟩]⟩)
      = ⟨true, .piEighth, [⟨0, .y⟩]⟩

example :
    (Rot.pushedBy ⟨false, .piQuarter, [⟨0, .z⟩]⟩
        ⟨false, .piEighth, [⟨0, .y⟩]⟩)
      = ⟨false, .piEighth, [⟨0, .x⟩]⟩

example :
    (Rot.pushedBy ⟨false, .piQuarter, [⟨0, .z⟩, ⟨1, .z⟩]⟩
        ⟨false, .piEighth, [⟨0, .x⟩]⟩)
      = ⟨true, .piEighth, [⟨0, .y⟩, ⟨1, .z⟩]⟩

def csDagRots (t : Nat) : List Rot

def aqftLadderLow : Nat → List Rot
  | 0     => []
  | t + 1 => csDagRots t ++ (hGate t).flatten ++ aqftLadderLow t

def swapRots (i j : Nat) : List Rot

def bitRevRots (n : Nat) : List Rot

def aqft2Rots : Nat → List Rot
  | 0     => []
  | n + 1 => bitRevRots (n + 1) ++ ((hGate n).flatten ++ aqftLadderLow n)

def aqft2Schedule (n : Nat) : RotProg

private theorem swapRots_countPi8 (i j : Nat) :
    (swapRots i j).countP (fun r => r.angle == RAngle.piEighth) = 0

private theorem flatMap_countPi8_zero (f : Nat → List Rot)
    (hf : ∀ i, (f i).countP (fun r => r.angle == RAngle.piEighth) = 0) :
    ∀ l : List Nat,
      (l.flatMap f).countP (fun r => r.angle == RAngle.piEighth) = 0
  | [] => rfl
  | i :: t =>

theorem bitRevRots_countPi8 (n : Nat) :
    (bitRevRots n).countP (fun r => r.angle == RAngle.piEighth) = 0

theorem aqftLadderLow_countPi8 (t : Nat) :
    (aqftLadderLow t).countP (fun r => r.angle == RAngle.piEighth) = 3 * t

theorem aqft2Schedule_countPi8 (n : Nat) :
    countPi8 (aqft2Schedule (n + 1)) = 3 * n

theorem aqft2Schedule_denote (W n : Nat)
    (h : ∀ r ∈ aqft2Rots n,
          sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ W) :
    RotProg.denote W (aqft2Schedule n) = seqDenote W (aqft2Rots n)

def hLayerRots (k : Nat) : List Rot

def qpeRots (k : Nat) (oracle : List Rot) : List Rot

def qpeSchedule (k : Nat) (oracle : List Rot) : RotProg

theorem hLayerRots_countPi8 (k : Nat) :
    (hLayerRots k).countP (fun r => r.angle == RAngle.piEighth) = 0

theorem qpeSchedule_gate_countPi8 (n : Nat) (g : Gate) :
    countPi8 (qpeSchedule (n + 1) (gateRots g)) = Gate.tcount g + 3 * n

theorem qpeSchedule_denote (W k : Nat) (oracle : List Rot)
    (h : ∀ r ∈ qpeRots k oracle,
          sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ W) :
    RotProg.denote W (qpeSchedule k oracle) = seqDenote W (qpeRots k oracle)

example : (aqft2Rots 3).length = 24

example : countPi8 (aqft2Schedule 3) = 6

example : ∀ r ∈ aqft2Rots 3,
    sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ 3

example : RotProg.wf (aqft2Schedule 3) = true

example : countPi8 (qpeSchedule 2 (gateRots (.CCX 2 3 4))) = 10

example : ∀ r ∈ qpeRots 2 (gateRots (.CCX 2 3 4)),
    sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ 5

def dropPiL (L : RotLayer) : RotLayer

def dropPi (p : RotProg) : RotProg

theorem dropPiL_denote (n : Nat) (L : RotLayer) :
    RotLayer.denote n L
      = ((-1 : ℂ) ^ countAngleL .pi L) • RotLayer.denote n (dropPiL L)

theorem dropPi_denote (n : Nat) (p : RotProg) :
    RotProg.denote n p
      = ((-1 : ℂ) ^ countAngle .pi p) • RotProg.denote n (dropPi p)

theorem countAngleL_dropPiL (a : RAngle) (ha : a ≠ .pi) (L : RotLayer) :
    countAngleL a (dropPiL L) = countAngleL a L

theorem countAngle_dropPi (a : RAngle) (ha : a ≠ .pi) (p : RotProg) :
    countAngle a (dropPi p) = countAngle a p

theorem countPi8_dropPi (p : RotProg) : countPi8 (dropPi p) = countPi8 p

theorem depth_dropPi (p : RotProg) : rotDepth (dropPi p) = rotDepth p

private theorem all_filter_of_all {α} (q f : α → Bool) (l : List α)
    (h : l.all f = true) : (l.filter q).all f = true

private theorem layerComm_filter (q : Rot → Bool) (L : RotLayer)
    (h : layerComm L = true) : layerComm (L.filter q) = true

theorem dropPiL_wf (L : RotLayer) (h : RotLayer.wf L = true) :
    RotLayer.wf (dropPiL L) = true

theorem dropPi_wf (p : RotProg) (h : RotProg.wf p = true) :
    RotProg.wf (dropPi p) = true

theorem Rot.denote_inv_mul (n : Nat) (r : Rot) :
    Rot.denote n r.inv * Rot.denote n r = 1

theorem denote_cancel_adjacent (n : Nat) (r : Rot) (p : RotProg) :
    RotProg.denote n ([r] :: [r.inv] :: p) = RotProg.denote n p

theorem countRot_cancel_pair (r : Rot) (p : RotProg) :
    countRot ([r] :: [r.inv] :: p) = countRot p + 2

theorem depth_cancel_pair (r : Rot) (p : RotProg) :
    rotDepth ([r] :: [r.inv] :: p) = rotDepth p + 2

def RAngle.doubled : RAngle → Option RAngle
  | .pi        => none
  | .piHalf    => some .pi
  | .piQuarter => some .piHalf
  | .piEighth  => some .piQuarter

theorem RAngle.doubled_val {a b : RAngle} (h : a.doubled = some b) :
    b.val = 2 * a.val

theorem denote_double_adjacent (n : Nat) (r : Rot) {b : RAngle}
    (hb : r.angle.doubled = some b) (p : RotProg) :
    RotProg.denote n ([r] :: [r] :: p)
      = RotProg.denote n ([{ r with angle

theorem denote_pi_sq_adjacent (n : Nat) (r : Rot) (h : r.angle = .pi)
    (p : RotProg) :
    RotProg.denote n ([r] :: [r] :: p) = RotProg.denote n p

example :  -- dropping a π rotation keeps the T-count
    countPi8 (dropPi [[⟨false, .pi, [⟨0, .z⟩]⟩], [⟨false, .piEighth, [⟨1, .z⟩]⟩]])
      = 1

example :  -- two T's about Z[0] fuse into one S
    RAngle.doubled .piEighth = some .piQuarter

def passes (r : Rot) (L : RotLayer) : Bool

def passesAll (r : Rot) (p : RotProg) : Bool

def insertASAP (r : Rot) : RotProg → RotProg
  | [] => [[r]]
  | L :: rest =>
      if passes r L && passesAll r rest
      then (L ++ [r]) :: rest
      else L :: insertASAP r rest

def scheduleList (rs : List Rot) : RotProg

noncomputable def seqDenote (n : Nat) : List Rot → Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ
  | []      => 1
  | r :: rs => seqDenote n rs * Rot.denote n r

theorem denote_singletons (n : Nat) (rs : List Rot) :
    RotProg.denote n (rs.map (fun r => [r])) = seqDenote n rs

def RotsBounded (n : Nat) (p : RotProg) : Prop

theorem commute_denote_layer (n : Nat) (r : Rot) (L : RotLayer)
    (hb : ∀ s ∈ L, sortedStrict s.axis = true ∧ PauliProduct.width s.axis ≤ n)
    (hp : passes r L = true) :
    Commute (Rot.denote n r) (RotLayer.denote n L)

theorem commute_denote_prog (n : Nat) (r : Rot) (p : RotProg)
    (hb : RotsBounded n p) (hp : passesAll r p = true) :
    Commute (Rot.denote n r) (RotProg.denote n p)

theorem insertASAP_denote (n : Nat) (r : Rot) (p : RotProg)
    (hb : RotsBounded n p) :
    RotProg.denote n (insertASAP r p) = Rot.denote n r * RotProg.denote n p

theorem insertASAP_bounded (n : Nat) (r : Rot)
    (hr : sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ n)
    (p : RotProg) (hb : RotsBounded n p) : RotsBounded n (insertASAP r p)

private theorem scheduleList_denote_aux (n : Nat) (rs : List Rot) (acc : RotProg)
    (hrs : ∀ r ∈ rs, sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ n)
    (hacc : RotsBounded n acc) :
    RotProg.denote n (rs.foldl (fun a r => insertASAP r a) acc)
      = seqDenote n rs * RotProg.denote n acc

theorem scheduleList_denote (n : Nat) (rs : List Rot)
    (hrs : ∀ r ∈ rs, sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ n) :
    RotProg.denote n (scheduleList rs) = seqDenote n rs

theorem insertASAP_countAngle (a : RAngle) (r : Rot) (p : RotProg) :
    countAngle a (insertASAP r p)
      = countAngle a p + (if r.angle == a then 1 else 0)

theorem scheduleList_countAngle (a : RAngle) (rs : List Rot) :
    countAngle a (scheduleList rs) = rs.countP (fun r => r.angle == a)

theorem scheduleList_countPi8 (rs : List Rot) :
    countPi8 (scheduleList rs) = rs.countP (fun r => r.angle == RAngle.piEighth)

theorem insertASAP_depth_le (r : Rot) (p : RotProg) :
    rotDepth (insertASAP r p) ≤ rotDepth p + 1

theorem scheduleList_depth_le (rs : List Rot) :
    rotDepth (scheduleList rs) ≤ rs.length

example : scheduleList ((cczGate 0 1 2).flatten) = cczLayer 0 1 2

example : rotDepth (scheduleList ((cnotGate 0 1).flatten)) = 1

example : rotDepth (scheduleList
    [⟨false, .piEighth, [⟨0, .x⟩]⟩, ⟨false, .piEighth, [⟨0, .z⟩]⟩]) = 2

example : rotDepth (scheduleList
    ((cczGate 0 1 2).flatten ++ (cczGate 3 4 5).flatten)) = 1

def insertASAPK (K : Nat) (r : Rot) : RotProg → RotProg
  | [] => [[r]]
  | L :: rest =>
      if decide (L.length < K) && passes r L && passesAll r rest
      then (L ++ [r]) :: rest
      else L :: insertASAPK K r rest

def scheduleListK (K : Nat) (rs : List Rot) : RotProg

theorem insertASAPK_denote (K : Nat) (n : Nat) (r : Rot) (p : RotProg)
    (hb : RotsBounded n p) :
    RotProg.denote n (insertASAPK K r p)
      = Rot.denote n r * RotProg.denote n p

theorem insertASAPK_bounded (K n : Nat) (r : Rot)
    (hr : sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ n)
    (p : RotProg) (hb : RotsBounded n p) :
    RotsBounded n (insertASAPK K r p)

private theorem scheduleListK_denote_aux (K n : Nat) :
    ∀ (rs : List Rot) (acc : RotProg),
      (∀ r ∈ rs, sortedStrict r.axis = true
        ∧ PauliProduct.width r.axis ≤ n) →
      RotsBounded n acc →
      RotProg.denote n (rs.foldl (fun a r => insertASAPK K r a) acc)
        = seqDenote n rs * RotProg.denote n acc
  | [], acc, _, _ =>

theorem scheduleListK_denote (K n : Nat) (rs : List Rot)
    (hrs : ∀ r ∈ rs, sortedStrict r.axis = true
      ∧ PauliProduct.width r.axis ≤ n) :
    RotProg.denote n (scheduleListK K rs) = seqDenote n rs

def layersLE (K : Nat) (p : RotProg) : Bool

theorem insertASAPK_layers (K : Nat) (hK : 1 ≤ K) (r : Rot) (p : RotProg)
    (hp : layersLE K p = true) :
    layersLE K (insertASAPK K r p) = true

theorem scheduleListK_layers (K : Nat) (hK : 1 ≤ K) (rs : List Rot) :
    layersLE K (scheduleListK K rs) = true

theorem insertASAPK_countAngle (K : Nat) (a : RAngle) (r : Rot)
    (p : RotProg) :
    countAngle a (insertASAPK K r p)
      = countAngle a p + (if r.angle == a then 1 else 0)

private theorem foldl_countAngle (K : Nat) (a : RAngle) :
    ∀ (rs : List Rot) (acc : RotProg),
      countAngle a (rs.foldl (fun acc r => insertASAPK K r acc) acc)
        = countAngle a acc + rs.countP (fun r => r.angle == a)
  | [], acc => by simp
  | r :: rs, acc =>

theorem scheduleListK_countAngle (K : Nat) (a : RAngle) (rs : List Rot) :
    countAngle a (scheduleListK K rs)
      = rs.countP (fun r => r.angle == a)

theorem scheduleListK_countPi8 (K : Nat) (rs : List Rot) :
    countPi8 (scheduleListK K rs)
      = rs.countP (fun r => r.angle == RAngle.piEighth)

theorem countRot_eq_sum (p : RotProg) :
    countRot p = (p.map List.length).sum

theorem countRot_le_K_mul_depth (K : Nat) (p : RotProg)
    (hv : layersLE K p = true) :
    countRot p ≤ K * rotDepth p

theorem scheduleListK_depth_le (K : Nat) (rs : List Rot) :
    rotDepth (scheduleListK K rs) ≤ rs.length

theorem countRot_insertASAPK (K : Nat) (r : Rot) (p : RotProg) :
    countRot (insertASAPK K r p) = countRot p + 1

theorem countRot_scheduleListK (K : Nat) (rs : List Rot) :
    countRot (scheduleListK K rs) = rs.length

def packed (K : Nat) : RotProg → Bool
  | [] => true
  | [L] => decide (1 ≤ L.length) && decide (L.length ≤ K)
  | L :: rest => decide (L.length = K) && packed K rest

theorem insertASAPK_mem (K : Nat) (r : Rot) :
    ∀ (p : RotProg) (L : RotLayer) (s : Rot),
      L ∈ insertASAPK K r p → s ∈ L →
      (∃ L' ∈ p, s ∈ L') ∨ s = r

theorem insertASAPK_ne_nil (K : Nat) (r : Rot) :
    ∀ (p : RotProg), insertASAPK K r p ≠ []
  | [] => by simp [insertASAPK]
  | L :: rest =>

theorem insertASAPK_packed (K : Nat) (hK : 1 ≤ K) (r : Rot) :
    ∀ (acc : RotProg),
      (∀ L ∈ acc, ∀ s ∈ L, commF s.axis r.axis = true) →
      packed K acc = true →
      packed K (insertASAPK K r acc) = true

theorem packed_depth (K : Nat) (hK : 1 ≤ K) :
    ∀ (p : RotProg), packed K p = true →
      rotDepth p = (countRot p + K - 1) / K

def allCommB : List Rot → Bool
  | [] => true
  | r :: t => t.all (fun s => commF r.axis s.axis) && allCommB t

private theorem foldl_packed (K : Nat) (hK : 1 ≤ K) :
    ∀ (rs : List Rot) (acc : RotProg),
      allCommB rs = true →
      (∀ L ∈ acc, ∀ s ∈ L, ∀ r' ∈ rs, commF s.axis r'.axis = true) →
      packed K acc = true →
      packed K (rs.foldl (fun a r => insertASAPK K r a) acc) = true
  | [], _, _, _, hp => hp
  | r :: rs, acc, hcomm, hsub, hp =>

theorem scheduleListK_depth_eq (K : Nat) (hK : 1 ≤ K) (rs : List Rot)
    (hcomm : allCommB rs = true) :
    rotDepth (scheduleListK K rs) = (rs.length + K - 1) / K

theorem scheduleListK_optimal (K : Nat) (hK : 1 ≤ K) (rs : List Rot)
    (hcomm : allCommB rs = true)
    (q : RotProg) (hqv : layersLE K q = true)
    (hqc : countRot q = rs.length) :
    rotDepth (scheduleListK K rs) ≤ rotDepth q

theorem yMat_mulVec (n t : Nat) (ht : t < n) (v : Fin (2 ^ n) → ℂ)
    (i : Fin (2 ^ n)) :
    ((axisMat n [(⟨t, .y⟩ : PFactor)]).mulVec v) i
      = (if ((flipT n t ht i : Fin (2 ^ n)) : Nat).testBit t
          then -Complex.I else Complex.I) * v (flipT n t ht i)

theorem mulVec_yn_tensorHigh (n : Nat) (α β : ℂ) (ψ : Fin (2 ^ n) → ℂ) :
    (axisMat (n + 1) [(⟨n, .y⟩ : PFactor)]).mulVec (tensorHigh n α β ψ)
      = tensorHigh n (-Complex.I * β) (Complex.I * α) ψ

theorem axisMat_snoc_split (n : Nat) (P : PauliProduct) (f : PFactor)
    (hw : ∀ g ∈ P, g.qubit < f.qubit) :
    axisMat n (P ++ [f]) = axisMat n P * axisMat n [f]

theorem mulVec_joint_tensorHigh (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (α β : ℂ) (ψ : Fin (2 ^ n) → ℂ) :
    (axisMat (n + 1) (P ++ [⟨n, .z⟩])).mulVec (tensorHigh n α β ψ)
      = tensorHigh n α (-β) ((axisMat n P).mulVec ψ)

def lowBits3 (m : Nat) (M : Fin (2 ^ (m + 3))) : Fin (2 ^ m)

noncomputable def tensorTriple (m : Nat) (f : Bool → Bool → Bool → ℂ)
    (ψ : Fin (2 ^ m) → ℂ) : Fin (2 ^ (m + 3)) → ℂ

theorem tensorTriple_vec_add (m : Nat) (f : Bool → Bool → Bool → ℂ)
    (ψ φ : Fin (2 ^ m) → ℂ) :
    tensorTriple m f (ψ + φ)
      = tensorTriple m f ψ + tensorTriple m f φ

theorem tensorTriple_vec_smul (m : Nat) (f : Bool → Bool → Bool → ℂ)
    (c : ℂ) (ψ : Fin (2 ^ m) → ℂ) :
    tensorTriple m f (c • ψ) = c • tensorTriple m f ψ

theorem tensorTriple_f_add (m : Nat) (f g : Bool → Bool → Bool → ℂ)
    (ψ : Fin (2 ^ m) → ℂ) :
    tensorTriple m (fun a b c => f a b c + g a b c) ψ
      = tensorTriple m f ψ + tensorTriple m g ψ

theorem tensorTriple_f_smul (m : Nat) (c : ℂ) (f : Bool → Bool → Bool → ℂ)
    (ψ : Fin (2 ^ m) → ℂ) :
    tensorTriple m (fun a b d => c * f a b d) ψ
      = c • tensorTriple m f ψ

theorem lowBits3_testBit (m : Nat) (M : Fin (2 ^ (m + 3))) (q : Nat)
    (hq : q < m) :
    ((lowBits3 m M : Fin (2 ^ m)) : Nat).testBit q = (M : Nat).testBit q

theorem lowBits3_flip (m : Nat) (M : Fin (2 ^ (m + 3))) (i : Nat)
    (hi : m ≤ i) (hi3 : i < m + 3) :
    lowBits3 m (flipT (m + 3) i (by omega) M) = lowBits3 m M

theorem mulVec_zd_tensorTriple (m d : Nat) (hd : d < m)
    (f : Bool → Bool → Bool → ℂ) (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨d, .z⟩ : PFactor)]).mulVec (tensorTriple m f ψ)
      = tensorTriple m f ((axisMat m [(⟨d, .z⟩ : PFactor)]).mulVec ψ)

theorem mulVec_za_tensorTriple (m : Nat) (i : Fin 3)
    (f : Bool → Bool → Bool → ℂ) (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨m + (i : Nat), .z⟩ : PFactor)]).mulVec
        (tensorTriple m f ψ)
      = tensorTriple m
          (fun y₁ y₂ y₃ =>
            (if (match (i : Nat) with | 0 => y₁ | 1 => y₂ | _ => y₃)
             then (-1 : ℂ) else 1) * f y₁ y₂ y₃) ψ

theorem mulVec_xa_tensorTriple (m : Nat) (i : Fin 3)
    (f : Bool → Bool → Bool → ℂ) (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨m + (i : Nat), .x⟩ : PFactor)]).mulVec
        (tensorTriple m f ψ)
      = tensorTriple m
          (fun y₁ y₂ y₃ =>
            match (i : Nat) with
            | 0 => f (!y₁) y₂ y₃
            | 1 => f y₁ (!y₂) y₃
            | _ => f y₁ y₂ (!y₃)) ψ

theorem mulVec_joint_tt (m d : Nat) (hd : d < m) (i : Fin 3)
    (f : Bool → Bool → Bool → ℂ) (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨d, .z⟩ : PFactor), ⟨m + (i : Nat), .z⟩]).mulVec
        (tensorTriple m f ψ)
      = tensorTriple m
          (fun y₁ y₂ y₃ =>
            (if (match (i : Nat) with | 0 => y₁ | 1 => y₂ | _ => y₃)
             then (-1 : ℂ) else 1) * f y₁ y₂ y₃)
          ((axisMat m [(⟨d, .z⟩ : PFactor)]).mulVec ψ)

theorem mulVec_za0_tt (m : Nat) (f : Bool → Bool → Bool → ℂ)
    (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨m, .z⟩ : PFactor)]).mulVec (tensorTriple m f ψ)
      = tensorTriple m
          (fun y₁ y₂ y₃ => (if y₁ then (-1 : ℂ) else 1) * f y₁ y₂ y₃) ψ

theorem mulVec_za1_tt (m : Nat) (f : Bool → Bool → Bool → ℂ)
    (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨m + 1, .z⟩ : PFactor)]).mulVec (tensorTriple m f ψ)
      = tensorTriple m
          (fun y₁ y₂ y₃ => (if y₂ then (-1 : ℂ) else 1) * f y₁ y₂ y₃) ψ

theorem mulVec_za2_tt (m : Nat) (f : Bool → Bool → Bool → ℂ)
    (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨m + 2, .z⟩ : PFactor)]).mulVec (tensorTriple m f ψ)
      = tensorTriple m
          (fun y₁ y₂ y₃ => (if y₃ then (-1 : ℂ) else 1) * f y₁ y₂ y₃) ψ

theorem mulVec_xa0_tt (m : Nat) (f : Bool → Bool → Bool → ℂ)
    (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨m, .x⟩ : PFactor)]).mulVec (tensorTriple m f ψ)
      = tensorTriple m (fun y₁ y₂ y₃ => f (!y₁) y₂ y₃) ψ

theorem mulVec_xa1_tt (m : Nat) (f : Bool → Bool → Bool → ℂ)
    (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨m + 1, .x⟩ : PFactor)]).mulVec (tensorTriple m f ψ)
      = tensorTriple m (fun y₁ y₂ y₃ => f y₁ (!y₂) y₃) ψ

theorem mulVec_xa2_tt (m : Nat) (f : Bool → Bool → Bool → ℂ)
    (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨m + 2, .x⟩ : PFactor)]).mulVec (tensorTriple m f ψ)
      = tensorTriple m (fun y₁ y₂ y₃ => f y₁ y₂ (!y₃)) ψ

noncomputable def twf (t y : Bool) : ℂ

theorem mulVec_dest1_tt (m : Nat) (t₂ t₃ : Bool)
    (f : Bool → Bool → Bool → ℂ) (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) ((⟨m, .x⟩ : PFactor)
        :: ((if t₂ then [(⟨m + 1, .z⟩ : PFactor)] else [])
            ++ (if t₃ then [(⟨m + 2, .z⟩ : PFactor)] else [])))).mulVec
        (tensorTriple m f ψ)
      = tensorTriple m
          (fun y₁ y₂ y₃ => twf t₂ y₂ * twf t₃ y₃ * f (!y₁) y₂ y₃) ψ

theorem mulVec_dest2_tt (m : Nat) (t₁ t₃ : Bool)
    (f : Bool → Bool → Bool → ℂ) (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) ((if t₁ then [(⟨m, .z⟩ : PFactor)] else [])
        ++ ((⟨m + 1, .x⟩ : PFactor)
            :: (if t₃ then [(⟨m + 2, .z⟩ : PFactor)] else [])))).mulVec
        (tensorTriple m f ψ)
      = tensorTriple m
          (fun y₁ y₂ y₃ => twf t₁ y₁ * twf t₃ y₃ * f y₁ (!y₂) y₃) ψ

theorem mulVec_dest3_tt (m : Nat) (t₁ t₂ : Bool)
    (f : Bool → Bool → Bool → ℂ) (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) ((if t₁ then [(⟨m, .z⟩ : PFactor)] else [])
        ++ ((if t₂ then [(⟨m + 1, .z⟩ : PFactor)] else [])
            ++ [(⟨m + 2, .x⟩ : PFactor)]))).mulVec
        (tensorTriple m f ψ)
      = tensorTriple m
          (fun y₁ y₂ y₃ => twf t₁ y₁ * twf t₂ y₂ * f y₁ y₂ (!y₃)) ψ

theorem mulVec_joint1_tt (m d : Nat) (hd : d < m)
    (f : Bool → Bool → Bool → ℂ) (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨d, .z⟩ : PFactor), ⟨m, .z⟩]).mulVec
        (tensorTriple m f ψ)
      = tensorTriple m
          (fun y₁ y₂ y₃ => (if y₁ then (-1 : ℂ) else 1) * f y₁ y₂ y₃)
          ((axisMat m [(⟨d, .z⟩ : PFactor)]).mulVec ψ)

theorem mulVec_joint2_tt (m d : Nat) (hd : d < m)
    (f : Bool → Bool → Bool → ℂ) (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨d, .z⟩ : PFactor), ⟨m + 1, .z⟩]).mulVec
        (tensorTriple m f ψ)
      = tensorTriple m
          (fun y₁ y₂ y₃ => (if y₂ then (-1 : ℂ) else 1) * f y₁ y₂ y₃)
          ((axisMat m [(⟨d, .z⟩ : PFactor)]).mulVec ψ)

theorem mulVec_joint3_tt (m d : Nat) (hd : d < m)
    (f : Bool → Bool → Bool → ℂ) (ψ : Fin (2 ^ m) → ℂ) :
    (axisMat (m + 3) [(⟨d, .z⟩ : PFactor), ⟨m + 2, .z⟩]).mulVec
        (tensorTriple m f ψ)
      = tensorTriple m
          (fun y₁ y₂ y₃ => (if y₃ then (-1 : ℂ) else 1) * f y₁ y₂ y₃)
          ((axisMat m [(⟨d, .z⟩ : PFactor)]).mulVec ψ)

theorem mulVec_corr_tt (m d : Nat) (hd : d < m) (p : Bool)
    (f : Bool → Bool → Bool → ℂ) (ψ : Fin (2 ^ m) → ℂ) :
    ((if p then axisMat (m + 3) [(⟨d, .z⟩ : PFactor)] else 1)).mulVec
        (tensorTriple m f ψ)
      = tensorTriple m f
          ((if p then axisMat m [(⟨d, .z⟩ : PFactor)] else 1).mulVec ψ)

theorem corr_entry (m d : Nat) (p : Bool) (hd : d < m)
    (v : Fin (2 ^ m) → ℂ) (j : Fin (2 ^ m)) :
    ((if p then axisMat m [(⟨d, .z⟩ : PFactor)] else 1).mulVec v) j
      = (if p && (j : Nat).testBit d then (-1 : ℂ) else 1) * v j

noncomputable def cczF : Bool → Bool → Bool → ℂ

noncomputable def cczCollapse (m₁ m₂ m₃ b₁ b₂ b₃ : Bool) :
    Bool → Bool → Bool → ℂ

noncomputable def cczSign (m₁ m₂ m₃ b₁ b₂ b₃ : Bool) : ℂ

theorem tw_xor (a b : Bool) :
    (if (a ^^ b) then (-1 : ℂ) else 1)
      = (if a then (-1 : ℂ) else 1) * (if b then (-1 : ℂ) else 1)

theorem tw_sq (c : Bool) :
    (if c then (-1 : ℂ) else 1) ^ 2 = 1

theorem tw_cube (c : Bool) :
    (if c then (-1 : ℂ) else 1) ^ 3 = (if c then (-1 : ℂ) else 1)

theorem tw_pow_four (c : Bool) :
    (if c then (-1 : ℂ) else 1) ^ 4 = 1

theorem cczBlock_branch (m d₁ d₂ d₃ : Nat)
    (h₁ : d₁ < m) (h₂ : d₂ < m) (h₃ : d₃ < m)
    (m₁ m₂ m₃ b₁ b₂ b₃ : Bool) (ψ : Fin (2 ^ m) → ℂ) :
    (if b₃ ^^ (m₁ && m₂) then axisMat (m + 3) [(⟨d₃, .z⟩ : PFactor)]
        else 1).mulVec
      ((if b₂ ^^ (m₁ && m₃) then axisMat (m + 3) [(⟨d₂, .z⟩ : PFactor)]
          else 1).mulVec
        ((if b₁ ^^ (m₂ && m₃) then axisMat (m + 3) [(⟨d₁, .z⟩ : PFactor)]
            else 1).mulVec
          ((projHalf (axisMat (m + 3)
              ((if m₂ then [(⟨m, .z⟩ : PFactor)] else [])
                ++ ((if m₁ then [(⟨m + 1, .z⟩ : PFactor)] else [])

def cczBlock (d₁ d₂ d₃ a c : Nat) : PPMProg

theorem cczBlock_magicCCZ (d₁ d₂ d₃ a c : Nat) :
    countMagicCCZ (cczBlock d₁ d₂ d₃ a c) = 1

theorem cczBlock_magicT (d₁ d₂ d₃ a c : Nat) :
    countMagicT (cczBlock d₁ d₂ d₃ a c) = 0

theorem cczBlock_meas (d₁ d₂ d₃ a c : Nat) :
    countMeas (cczBlock d₁ d₂ d₃ a c) = 6

theorem cczBlock_cwidth (d₁ d₂ d₃ a c : Nat) :
    PPMProg.cwidth (cczBlock d₁ d₂ d₃ a c) = 6

theorem cczRoute7T_magicT (x y z a c : Nat) :
    countMagicT (lowerFlat a c (cczGate x y z).flatten) = 7

theorem ccz_route_tradeoff (x y z a c d₁ d₂ d₃ a' c' : Nat) :
    countMagicT (lowerFlat a c (cczGate x y z).flatten) = 7
      ∧ countMagicCCZ (lowerFlat a c (cczGate x y z).flatten) = 0
      ∧ countMagicT (cczBlock d₁ d₂ d₃ a' c') = 0
      ∧ countMagicCCZ (cczBlock d₁ d₂ d₃ a' c') = 1

def isCCZRots : List Rot → Option (Nat × Nat × Nat)
  | [⟨false, .piEighth, [⟨x₁, .z⟩]⟩,
     ⟨false, .piEighth, [⟨y₁, .z⟩]⟩,
     ⟨false, .piEighth, [⟨z₁, .z⟩]⟩,
     ⟨true,  .piEighth, [⟨x₂, .z⟩, ⟨y₂, .z⟩]⟩,
     ⟨true,  .piEighth, [⟨x₃, .z⟩, ⟨z₂, .z⟩]⟩,
     ⟨true,  .piEighth, [⟨y₃, .z⟩, ⟨z₃, .z⟩]⟩,
     ⟨false, .piEighth, [⟨x₄, .z⟩, ⟨y₄, .z⟩, ⟨z₄, .z⟩]⟩] =>
      if x₁ = x₂ ∧ x₁ = x₃ ∧ x₁ = x₄ ∧ y₁ = y₂ ∧ y₁ = y₃ ∧ y₁ = y₄
          ∧ z₁ = z₂ ∧ z₁ = z₃ ∧ z₁ = z₄ ∧ x₁ < y₁ ∧ y₁ < z₁
      then some (x₁, y₁, z₁) else none
  | _ => none

theorem isCCZRots_sound (rs : List Rot) (x y z : Nat)
    (h : isCCZRots rs = some (x, y, z)) :
    rs = (cczGate x y z).flatten ∧ x < y ∧ y < z

theorem isCCZRots_complete (x y z : Nat) (hxy : x < y) (hyz : y < z) :
    isCCZRots (cczGate x y z).flatten = some (x, y, z)

theorem tensorHigh_vec_add (n : Nat) (α β : ℂ) (φ φ' : Fin (2 ^ n) → ℂ) :
    tensorHigh n α β (φ + φ')
      = tensorHigh n α β φ + tensorHigh n α β φ'

theorem tensorHigh_vec_smul (n : Nat) (α β c : ℂ) (φ : Fin (2 ^ n) → ℂ) :
    tensorHigh n α β (c • φ) = c • tensorHigh n α β φ

theorem mulVec_yq_tensorHigh (n q : Nat) (hq : q < n) (α β : ℂ)
    (ψ : Fin (2 ^ n) → ℂ) :
    (axisMat (n + 1) [(⟨q, .y⟩ : PFactor)]).mulVec (tensorHigh n α β ψ)
      = tensorHigh n α β ((axisMat n [(⟨q, .y⟩ : PFactor)]).mulVec ψ)

theorem mulVec_axis_tensorHigh' (n : Nat) :
    ∀ (P : PauliProduct), sortedStrict P = true →
      PauliProduct.width P ≤ n →
      ∀ (α β : ℂ) (ψ : Fin (2 ^ n) → ℂ),
        (axisMat (n + 1) P).mulVec (tensorHigh n α β ψ)
          = tensorHigh n α β ((axisMat n P).mulVec ψ)
  | [], _, _, α, β, ψ =>

def stmtLow (n : Nat) : PPMStmt → Bool
  | .measure _ P => sortedStrict P && decide (PauliProduct.width P ≤ n)
  | .measureSel _ _ Pt Pe =>
      sortedStrict Pt && decide (PauliProduct.width Pt ≤ n)
        && sortedStrict Pe && decide (PauliProduct.width Pe ≤ n)
  | .measureSel2 _ _ _ P00 P01 P10 P11 =>
      sortedStrict P00 && decide (PauliProduct.width P00 ≤ n)
        && sortedStrict P01 && decide (PauliProduct.width P01 ≤ n)
        && sortedStrict P10 && decide (PauliProduct.width P10 ≤ n)
        && sortedStrict P11 && decide (PauliProduct.width P11 ≤ n)
  | .frame P => sortedStrict P && decide (PauliProduct.width P ≤ n)
  | .correct _ thn els =>

theorem stmtDenote_tensorHigh (n : Nat) (outs : List Bool) (b : Bool)
    (st : PPMStmt) (hst : stmtLow n st = true) (α β : ℂ)
    (ψ : Fin (2 ^ n) → ℂ) :
    (stmtDenote (n + 1) outs b st).mulVec (tensorHigh n α β ψ)
      = tensorHigh n α β ((stmtDenote n outs b st).mulVec ψ)

theorem progDenote_tensorHigh (n : Nat) (ω : Nat → Bool) :
    ∀ (p : PPMProg) (outs : List Bool),
      (∀ st ∈ p, stmtLow n st = true) →
      ∀ (α β : ℂ) (ψ : Fin (2 ^ n) → ℂ),
        (progDenote (n + 1) ω outs p).mulVec (tensorHigh n α β ψ)
          = tensorHigh n α β ((progDenote n ω outs p).mulVec ψ)
  | [], outs, _, α, β, ψ =>

theorem kinds_hGate (q : Nat) :
    ∀ r ∈ (hGate q).flatten, ∀ f ∈ r.axis,
      f.kind = PKind.z ∨ f.kind = PKind.x

theorem kinds_mk2 (c t : Nat) (kc kt : PKind)
    (hc : kc = PKind.z ∨ kc = PKind.x) (ht : kt = PKind.z ∨ kt = PKind.x) :
    ∀ f ∈ mk2 c kc t kt, f.kind = PKind.z ∨ f.kind = PKind.x

theorem kinds_cnot (c t : Nat) :
    ∀ r ∈ (cnotGate c t).flatten, ∀ f ∈ r.axis,
      f.kind = PKind.z ∨ f.kind = PKind.x

theorem kinds_ccz (a b c : Nat) :
    ∀ r ∈ (cczGate a b c).flatten, ∀ f ∈ r.axis,
      f.kind = PKind.z ∨ f.kind = PKind.x

theorem gateRots_kinds (g : FormalRV.Framework.Gate) :
    ∀ r ∈ gateRots g, ∀ f ∈ r.axis,
      f.kind = PKind.z ∨ f.kind = PKind.x

theorem lowerGate_denote (m : Nat) (g : FormalRV.Framework.Gate)
    (hops : opsOK g = true) (hw : width g ≤ m)
    (ω : Nat → Bool) (outs : List Bool) (ψ : Fin (2 ^ m) → ℂ) :
    (progDenote (ampsWidth m (ancAmps (gateRots g))) ω outs
        (lowerFlat m outs.length (gateRots g))).mulVec
      (stateOver (ancAmps (gateRots g)) (ancAmps (gateRots g)) m ψ)
    = (branchScalar ω (gateRots g) outs.length * gphase g)
        • stateOver (ancAmps (gateRots g))
            (ancOutAmps ω (gateRots g) outs.length) m
            ((applyMat m g).mulVec ψ)

theorem kinds_csDag (t : Nat) :
    ∀ r ∈ csDagRots t, ∀ f ∈ r.axis,
      f.kind = PKind.z ∨ f.kind = PKind.x

theorem kinds_swap (i j : Nat) :
    ∀ r ∈ swapRots i j, ∀ f ∈ r.axis,
      f.kind = PKind.z ∨ f.kind = PKind.x

theorem kinds_bitRev (k : Nat) :
    ∀ r ∈ bitRevRots k, ∀ f ∈ r.axis,
      f.kind = PKind.z ∨ f.kind = PKind.x

theorem kinds_ladderLow :
    ∀ (t : Nat), ∀ r ∈ aqftLadderLow t, ∀ f ∈ r.axis,
      f.kind = PKind.z ∨ f.kind = PKind.x
  | 0, r, hr => by cases hr
  | t + 1, r, hr =>

theorem kinds_hLayer (k : Nat) :
    ∀ r ∈ hLayerRots k, ∀ f ∈ r.axis,
      f.kind = PKind.z ∨ f.kind = PKind.x

theorem kinds_aqft2 :
    ∀ (k : Nat), ∀ r ∈ aqft2Rots k, ∀ f ∈ r.axis,
      f.kind = PKind.z ∨ f.kind = PKind.x
  | 0, r, hr => by cases hr
  | k + 1, r, hr =>

theorem kinds_qpe (k : Nat) (oracle : List Rot)
    (horacle : ∀ r ∈ oracle, ∀ f ∈ r.axis,
      f.kind = PKind.z ∨ f.kind = PKind.x) :
    ∀ r ∈ qpeRots k oracle, ∀ f ∈ r.axis,
      f.kind = PKind.z ∨ f.kind = PKind.x

theorem lowerShorQPE_denote (n k : Nat) (oracleG : FormalRV.Framework.Gate)
    (hops : opsOK oracleG = true) (hw : width oracleG ≤ n)
    (hk : k + 1 ≤ n)
    (hb : ∀ r ∈ qpeRots (k + 1) (gateRots oracleG),
        sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ n)
    (ω : Nat → Bool) (outs : List Bool) (ψ : Fin (2 ^ n) → ℂ) :
    (progDenote
        (ampsWidth n (ancAmps (qpeRots (k + 1) (gateRots oracleG)))) ω outs
        (lowerFlat n outs.length (qpeRots (k + 1) (gateRots oracleG)))).mulVec
      (stateOver (ancAmps (qpeRots (k + 1) (gateRots oracleG)))
        (ancAmps (qpeRots (k + 1) (gateRots oracleG))) n ψ)
    = (branchScalar ω (qpeRots (k + 1) (gateRots oracleG)) outs.length

def ampsWidth (m : Nat) : List ℂ → Nat
  | [] => m
  | _ :: as => ampsWidth (m + 1) as

noncomputable def stateOver :
    (skel : List ℂ) → (amps : List ℂ) → (m : Nat) → (Fin (2 ^ m) → ℂ)
      → (Fin (2 ^ ampsWidth m skel) → ℂ)
  | [], _, _, ψ => ψ
  | _ :: skel, [], m, ψ => stateOver skel [] (m + 1) (tensorHigh m 1 0 ψ)
  | _ :: skel, b :: bs, m, ψ =>
      stateOver skel bs (m + 1) (tensorHigh m 1 b ψ)

theorem ampsWidth_le (as : List ℂ) : ∀ (m : Nat), m ≤ ampsWidth m as

theorem stateOver_smul (skel : List ℂ) :
    ∀ (bs : List ℂ) (m : Nat) (c : ℂ) (ψ : Fin (2 ^ m) → ℂ),
      stateOver skel bs m (c • ψ) = c • stateOver skel bs m ψ

theorem stmtLow_mono (n n' : Nat) (h : n ≤ n') (st : PPMStmt)
    (hst : stmtLow n st = true) : stmtLow n' st = true

theorem progDenote_stateOver (skel : List ℂ) :
    ∀ (bs : List ℂ) (m : Nat) (p : PPMProg),
      (∀ st ∈ p, stmtLow m st = true) →
      ∀ (ω : Nat → Bool) (outs : List Bool) (ψ : Fin (2 ^ m) → ℂ),
        (progDenote (ampsWidth m skel) ω outs p).mulVec (stateOver skel bs m ψ)
          = stateOver skel bs m ((progDenote m ω outs p).mulVec ψ)

def extendTrace (ω : Nat → Bool) : List Bool → Nat → List Bool
  | outs, 0 => outs
  | outs, k + 1 => extendTrace ω (outs ++ [ω outs.length]) k

theorem extendTrace_length (ω : Nat → Bool) :
    ∀ (k : Nat) (outs : List Bool),
      (extendTrace ω outs k).length = outs.length + k

theorem progDenote_append' (d : Nat) (ω : Nat → Bool) :
    ∀ (p q : PPMProg) (outs : List Bool),
      progDenote d ω outs (p ++ q)
        = progDenote d ω (extendTrace ω outs (PPMProg.cwidth p)) q
            * progDenote d ω outs p

theorem rotOf_mulVec_tensorHigh (n : Nat) (θ : ℝ) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (α β : ℂ) (ψ : Fin (2 ^ n) → ℂ) :
    (rotOf θ (axisMat (n + 1) P)).mulVec (tensorHigh n α β ψ)
      = tensorHigh n α β ((rotOf θ (axisMat n P)).mulVec ψ)

theorem seqDenote_tensorHigh (n : Nat) :
    ∀ (rs : List Rot),
      (∀ r ∈ rs, sortedStrict r.axis = true
        ∧ PauliProduct.width r.axis ≤ n) →
      ∀ (α β : ℂ) (ψ : Fin (2 ^ n) → ℂ),
        (seqDenote (n + 1) rs).mulVec (tensorHigh n α β ψ)
          = tensorHigh n α β ((seqDenote n rs).mulVec ψ)
  | [], _, α, β, ψ =>

noncomputable def ancAmps : List Rot → List ℂ
  | [] => []
  | r :: rs =>
      (match r.angle with
       | RAngle.piQuarter => [ancInAmp r]
       | RAngle.piEighth  => [ancInAmp r]
       | _ => []) ++ ancAmps rs

noncomputable def ancOutAmps (ω : Nat → Bool) : List Rot → Nat → List ℂ
  | [], _ => []
  | r :: rs, c =>
      (match r.angle with
       | RAngle.piQuarter => [ancOutAmp r (ω c) (ω (c + 1))]
       | RAngle.piEighth  => [ancOutAmp r (ω c) (ω (c + 1))]
       | _ => []) ++ ancOutAmps ω rs (c + rotSlots r)

noncomputable def branchScalar (ω : Nat → Bool) : List Rot → Nat → ℂ
  | [], _ => 1
  | r :: rs, c => rotScalar r (ω c) (ω (c + 1)) * branchScalar ω rs (c + rotSlots r)

theorem sortedStrict_append_single :
    ∀ (P : PauliProduct) (a : Nat) (k : PKind),
      sortedStrict P = true → (∀ f ∈ P, f.qubit < a) →
      sortedStrict (P ++ [⟨a, k⟩]) = true
  | [], _, _, _, _ => rfl
  | [f], a, k, _, hq =>

theorem width_append :
    ∀ (P Q : PauliProduct),
      PauliProduct.width (P ++ Q)
        = max (PauliProduct.width P) (PauliProduct.width Q)
  | [], Q => by simp [PauliProduct.width]
  | f :: P, Q =>

theorem qubit_lt_width :
    ∀ (P : PauliProduct), ∀ f ∈ P, f.qubit < PauliProduct.width P
  | f :: P, g, hg =>

theorem lowerRot_low (m c : Nat) (r : Rot)
    (hs : sortedStrict r.axis = true)
    (hw : PauliProduct.width r.axis ≤ m) :
    ∀ st ∈ lowerRot m c r, stmtLow (m + 1) st = true

theorem lowerFlat_denote :
    ∀ (rs : List Rot) (m : Nat) (ψ : Fin (2 ^ m) → ℂ)
      (ω : Nat → Bool) (outs : List Bool),
      (∀ r ∈ rs, sortedStrict r.axis = true) →
      (∀ r ∈ rs, PauliProduct.width r.axis ≤ m) →
      (∀ r ∈ rs, ∀ f ∈ r.axis, f.kind = PKind.z ∨ f.kind = PKind.x) →
      (progDenote (ampsWidth m (ancAmps rs)) ω outs
          (lowerFlat m outs.length rs)).mulVec
        (stateOver (ancAmps rs) (ancAmps rs) m ψ)
      = branchScalar ω rs outs.length
          • stateOver (ancAmps rs) (ancOutAmps ω rs outs.length) m
              ((seqDenote m rs).mulVec ψ)

def LoweredOK (g : FormalRV.Framework.Gate) : Prop

theorem loweredOK_of (g : FormalRV.Framework.Gate)
    (hops : opsOK g = true) : LoweredOK g

theorem cuccaroLowered : LoweredOK (cuccaro_n_bit_adder_full 4 0)

theorem cuccaroAddConstLowered : LoweredOK (cuccaro_addConstGate 3 0 5)

theorem cuccaroSubConstLowered : LoweredOK (cuccaro_subConstGate 3 0 5)

theorem cuccaroCompareLowered :
    LoweredOK (cuccaro_compareConstForwardGate 3 0 5)

theorem cuccaroSubForwardLowered :
    LoweredOK (cuccaro_subConstForwardOnlyGate 3 0 5)

theorem cuccaroSubReverseLowered :
    LoweredOK (cuccaro_subConstReverseOnlyGate 3 0 5)

theorem gidneyLowered : LoweredOK (gidney_adder 2)

theorem gidneyPatchedLowered :
    LoweredOK (gidney_adder_full_faithful_no_measurement_patched 2)

theorem gidneyForwardRevLowered :
    LoweredOK (gidney_adder_forward_faithful_full_reverse_patched 2)

theorem cuccaroModAddLowered :
    LoweredOK (sqir_style_modAddConst_clean_gate 3 5 2)

theorem cuccaroCtrlModAddLowered :
    LoweredOK (sqir_style_controlledModAddConst_gate 3 2 5 2 1 0)

theorem gidneyAddConstLowered : LoweredOK (addConstGate 2 1)

theorem gidneySubConstLowered : LoweredOK (subConstGate 2 1)

theorem gidneyCondAddLowered : LoweredOK (conditionalAddConstGate 2 1 8)

theorem gidneyModAddLowered : LoweredOK (modAddConstGate 2 3 1)

theorem gidneyCtrlModAddLowered :
    LoweredOK (controlledModAddConstGate 2 3 1 9 10)

theorem modMultConstLowered : LoweredOK (modmult_const_gate 2 15 7)

theorem modMultMCPLowered : LoweredOK (modmult_MCP_gate 2 15 7 13)

theorem shorModExpVerifiedLowered :
    LoweredOK (shorModExpVerified 1 15 7 13)

theorem shorModExpLowered : LoweredOK (shorModExp 1 15 7)

theorem unaryLookupLowered :
    LoweredOK (unary_lookup_multi_iteration 2 [([0], [5])])

theorem grayLookupLowered :
    LoweredOK (grayLookupReadAt 2 (fun i => 6 + i) 1 (fun _ => 1))

theorem windowedMulLowered : LoweredOK (windowedMulCircuit 2 4 3 2)

theorem windowedModNMulLowered :
    LoweredOK (windowedModNMulCircuit 2 4 3 7 2)

theorem windowedModNInPlaceLowered :
    LoweredOK (windowedModNMulGate 2 4 7 2 3 5)

theorem grayWindowedMulLowered :
    LoweredOK (grayWindowedMulCircuitOf cuccaroAdder 2 4 3 2)

theorem shor15Lowered (ω : Nat → Bool) (outs : List Bool)
    (ψ : Fin (2 ^ 7) → ℂ) :
    (progDenote
        (ampsWidth 7 (ancAmps
          (qpeRots 3 (gateRots (shorModExpVerified 1 15 7 13))))) ω outs
        (lowerFlat 7 outs.length
          (qpeRots 3 (gateRots (shorModExpVerified 1 15 7 13))))).mulVec
      (stateOver (ancAmps (qpeRots 3 (gateRots (shorModExpVerified 1 15 7 13))))
        (ancAmps (qpeRots 3 (gateRots (shorModExpVerified 1 15 7 13)))) 7 ψ)
    = (branchScalar ω (qpeRots 3 (gateRots (shorModExpVerified 1 15 7 13)))
          outs.length
        * (iqftPhase 2 * gphase (shorModExpVerified 1 15 7 13)

noncomputable def stmtDenote (d : Nat) (outs : List Bool) (outcome : Bool) :
    PPMStmt → Matrix (Fin (2 ^ d)) (Fin (2 ^ d)) ℂ
  | .measure _ P => projHalf (axisMat d P) outcome
  | .measureSel sel _ Pt Pe =>
      projHalf (axisMat d (if xorParity outs sel then Pt else Pe)) outcome
  | .measureSel2 sel1 sel2 _ P00 P01 P10 P11 =>
      projHalf (axisMat d
        (if xorParity outs sel1 then
          (if xorParity outs sel2 then P11 else P10)
         else (if xorParity outs sel2 then P01 else P00))) outcome
  | .frame P => axisMat d P
  | .correct par thn els =>

noncomputable def progDenote (d : Nat) (ω : Nat → Bool) :
    List Bool → PPMProg → Matrix (Fin (2 ^ d)) (Fin (2 ^ d)) ℂ
  | _, [] => 1
  | outs, st :: p =>
      progDenote d ω (outs ++ List.replicate st.binds (ω outs.length)) p
        * stmtDenote d outs (ω outs.length) st

def rotAnc (r : Rot) : Nat

def rotSlots (r : Rot) : Nat

def lowerRot (a c : Nat) (r : Rot) : PPMProg

def lowerFlat (a c : Nat) : List Rot → PPMProg
  | []      => []
  | r :: rs => lowerRot a c r ++ lowerFlat (a + rotAnc r) (c + rotSlots r) rs

def countPi8L (rs : List Rot) : Nat

theorem lowerRot_magicT (a c : Nat) (r : Rot) :
    countMagicT (lowerRot a c r)
      = (if r.angle == RAngle.piEighth then 1 else 0)

theorem lowerFlat_magicT (rs : List Rot) :
    ∀ (a c : Nat), countMagicT (lowerFlat a c rs) = countPi8L rs

theorem lowerRot_cwidth (a c : Nat) (r : Rot) :
    PPMProg.cwidth (lowerRot a c r) = rotSlots r

theorem lowerFlat_cwidth (rs : List Rot) :
    ∀ (a c : Nat),
      PPMProg.cwidth (lowerFlat a c rs) = (rs.map rotSlots).sum

theorem lowerFlat_magicCCZ (rs : List Rot) :
    ∀ (a c : Nat), countMagicCCZ (lowerFlat a c rs) = 0

theorem xorParity_single (outs : List Bool) (c : Nat) :
    xorParity outs [c] = outs.getD c false

theorem xorParity_pair (outs : List Bool) (c c' : Nat) :
    xorParity outs [c, c'] = (outs.getD c false ^^ outs.getD c' false)

theorem getD_append_self (l : List Bool) (x : Bool) :
    (l ++ [x]).getD l.length false = x

theorem getD_append_lt (l l' : List Bool) (i : Nat) (hi : i < l.length) :
    (l ++ l').getD i false = l.getD i false

noncomputable def ancInAmp (r : Rot) : ℂ

noncomputable def ancOutAmp (r : Rot) (o₁ o₂ : Bool) : ℂ

noncomputable def rotScalar (r : Rot) (o₁ o₂ : Bool) : ℂ

theorem lowerRot_denote_free (n : Nat) (r : Rot) (a c : Nat)
    (hanc : rotAnc r = 0)
    (ω : Nat → Bool) (outs : List Bool) (ψ : Fin (2 ^ n) → ℂ) :
    (progDenote n ω outs (lowerRot a c r)).mulVec ψ
      = rotScalar r (ω outs.length) (ω (outs.length + 1))
          • (Rot.denote n r).mulVec ψ

theorem getD_two_snd (outs : List Bool) (x y : Bool) :
    ((outs ++ [x]) ++ [y]).getD (outs.length + 1) false = y

theorem getD_two_fst (outs : List Bool) (x y : Bool) :
    ((outs ++ [x]) ++ [y]).getD outs.length false = x

theorem lowerRot_denote_eighth (n : Nat) (r : Rot)
    (hang : r.angle = RAngle.piEighth)
    (hs : sortedStrict r.axis = true)
    (hw : PauliProduct.width r.axis ≤ n)
    (hk : ∀ f ∈ r.axis, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ω : Nat → Bool) (outs : List Bool) (ψ : Fin (2 ^ n) → ℂ) :
    (progDenote (n + 1) ω outs (lowerRot n outs.length r)).mulVec
        (tensorHigh n 1 (ancInAmp r) ψ)
      = rotScalar r (ω outs.length) (ω (outs.length + 1))
          • tensorHigh n 1 (ancOutAmp r (ω outs.length) (ω (outs.length + 1)))
              ((Rot.denote n r).mulVec ψ)

theorem axisMat_mul_rotOf_quarter (n : Nat) (P : PauliProduct) :
    axisMat n P * rotOf (Real.pi / 4) (axisMat n P)
      = (-Complex.I) • rotOf (-(Real.pi / 4)) (axisMat n P)

theorem lowerRot_denote_quarter (n : Nat) (r : Rot)
    (hang : r.angle = RAngle.piQuarter)
    (hs : sortedStrict r.axis = true)
    (hw : PauliProduct.width r.axis ≤ n)
    (hk : ∀ f ∈ r.axis, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ω : Nat → Bool) (outs : List Bool) (ψ : Fin (2 ^ n) → ℂ) :
    (progDenote (n + 1) ω outs (lowerRot n outs.length r)).mulVec
        (tensorHigh n 1 (ancInAmp r) ψ)
      = rotScalar r (ω outs.length) (ω (outs.length + 1))
          • tensorHigh n 1 (ancOutAmp r (ω outs.length) (ω (outs.length + 1)))
              ((Rot.denote n r).mulVec ψ)

theorem sBlock_branch_00 (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ψ : Fin (2 ^ n) → ℂ) :
    (projHalf (axisMat (n + 1) [(⟨n, .x⟩ : PFactor)]) false).mulVec
      ((projHalf (axisMat (n + 1) (P ++ [⟨n, .z⟩])) false).mulVec
        (tensorHigh n 1 Complex.I ψ))
      = ((2⁻¹ : ℂ) * phaseC (Real.pi / 4))
          • tensorHigh n 1 1 ((rotOf (Real.pi / 4) (axisMat n P)).mulVec ψ)

theorem sBlock_branch_01 (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ψ : Fin (2 ^ n) → ℂ) :
    (projHalf (axisMat (n + 1) [(⟨n, .x⟩ : PFactor)]) true).mulVec
      ((projHalf (axisMat (n + 1) (P ++ [⟨n, .z⟩])) false).mulVec
        (tensorHigh n 1 Complex.I ψ))
      = ((2⁻¹ : ℂ) * phaseC (Real.pi / 4))
          • tensorHigh n 1 (-1)
              ((axisMat n P).mulVec
                ((rotOf (Real.pi / 4) (axisMat n P)).mulVec ψ))

theorem sBlock_branch_10 (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ψ : Fin (2 ^ n) → ℂ) :
    (projHalf (axisMat (n + 1) [(⟨n, .x⟩ : PFactor)]) false).mulVec
      ((projHalf (axisMat (n + 1) (P ++ [⟨n, .z⟩])) true).mulVec
        (tensorHigh n 1 Complex.I ψ))
      = (-(2⁻¹ : ℂ) * phaseC (-(Real.pi / 4)))
          • tensorHigh n 1 1
              ((axisMat n P).mulVec
                ((rotOf (Real.pi / 4) (axisMat n P)).mulVec ψ))

theorem sBlock_branch_11 (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ψ : Fin (2 ^ n) → ℂ) :
    (projHalf (axisMat (n + 1) [(⟨n, .x⟩ : PFactor)]) true).mulVec
      ((projHalf (axisMat (n + 1) (P ++ [⟨n, .z⟩])) true).mulVec
        (tensorHigh n 1 Complex.I ψ))
      = ((2⁻¹ : ℂ) * phaseC (-(Real.pi / 4)))
          • tensorHigh n 1 (-1)
              ((rotOf (Real.pi / 4) (axisMat n P)).mulVec ψ)

noncomputable def projHalf {d : Type*} [Fintype d] [DecidableEq d]
    (M : Matrix d d ℂ) (b : Bool) : Matrix d d ℂ

theorem projHalf_mulVec {d : Type*} [Fintype d] [DecidableEq d]
    (M : Matrix d d ℂ) (b : Bool) (v : d → ℂ) :
    (projHalf M b).mulVec v
      = (2⁻¹ : ℂ) • (v + (if b then (-1 : ℂ) else 1) • M.mulVec v)

theorem tensorHigh_amps_add (n : Nat) (α α' β β' : ℂ) (ψ : Fin (2 ^ n) → ℂ) :
    tensorHigh n (α + α') (β + β') ψ
      = tensorHigh n α β ψ + tensorHigh n α' β' ψ

theorem tensorHigh_amps_smul (n : Nat) (c α β : ℂ) (ψ : Fin (2 ^ n) → ℂ) :
    tensorHigh n (c * α) (c * β) ψ = c • tensorHigh n α β ψ

theorem tBlock_branch_00 (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ψ : Fin (2 ^ n) → ℂ) :
    (projHalf (axisMat (n + 1) [(⟨n, .x⟩ : PFactor)]) false).mulVec
      ((projHalf (axisMat (n + 1) (P ++ [⟨n, .z⟩])) false).mulVec
        (tensorHigh n 1 (phaseC (Real.pi / 4)) ψ))
      = ((2⁻¹ : ℂ) * phaseC (Real.pi / 8))
          • tensorHigh n 1 1 ((rotOf (Real.pi / 8) (axisMat n P)).mulVec ψ)

theorem tBlock_branch_01 (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ψ : Fin (2 ^ n) → ℂ) :
    (projHalf (axisMat (n + 1) [(⟨n, .x⟩ : PFactor)]) true).mulVec
      ((projHalf (axisMat (n + 1) (P ++ [⟨n, .z⟩])) false).mulVec
        (tensorHigh n 1 (phaseC (Real.pi / 4)) ψ))
      = ((2⁻¹ : ℂ) * phaseC (Real.pi / 8))
          • tensorHigh n 1 (-1)
              ((axisMat n P).mulVec
                ((rotOf (Real.pi / 8) (axisMat n P)).mulVec ψ))

theorem tBlock_branch_10 (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ψ : Fin (2 ^ n) → ℂ) :
    (projHalf (axisMat (n + 1) [(⟨n, .y⟩ : PFactor)]) false).mulVec
      ((projHalf (axisMat (n + 1) (P ++ [⟨n, .z⟩])) true).mulVec
        (tensorHigh n 1 (phaseC (Real.pi / 4)) ψ))
      = ((2⁻¹ : ℂ) * phaseC (-(Real.pi / 8)))
          • tensorHigh n 1 Complex.I
              ((rotOf (Real.pi / 8) (axisMat n P)).mulVec ψ)

theorem tBlock_branch_11 (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ψ : Fin (2 ^ n) → ℂ) :
    (projHalf (axisMat (n + 1) [(⟨n, .y⟩ : PFactor)]) true).mulVec
      ((projHalf (axisMat (n + 1) (P ++ [⟨n, .z⟩])) true).mulVec
        (tensorHigh n 1 (phaseC (Real.pi / 4)) ψ))
      = (-(2⁻¹ : ℂ) * phaseC (-(Real.pi / 8)))
          • tensorHigh n 1 (-Complex.I)
              ((axisMat n P).mulVec
                ((rotOf (Real.pi / 8) (axisMat n P)).mulVec ψ))

theorem tBlockNeg_branch_00 (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ψ : Fin (2 ^ n) → ℂ) :
    (projHalf (axisMat (n + 1) [(⟨n, .x⟩ : PFactor)]) false).mulVec
      ((projHalf (axisMat (n + 1) (P ++ [⟨n, .z⟩])) false).mulVec
        (tensorHigh n 1 (phaseC (-(Real.pi / 4))) ψ))
      = ((2⁻¹ : ℂ) * phaseC (-(Real.pi / 8)))
          • tensorHigh n 1 1
              ((rotOf (-(Real.pi / 8)) (axisMat n P)).mulVec ψ)

theorem tBlockNeg_branch_01 (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ψ : Fin (2 ^ n) → ℂ) :
    (projHalf (axisMat (n + 1) [(⟨n, .x⟩ : PFactor)]) true).mulVec
      ((projHalf (axisMat (n + 1) (P ++ [⟨n, .z⟩])) false).mulVec
        (tensorHigh n 1 (phaseC (-(Real.pi / 4))) ψ))
      = ((2⁻¹ : ℂ) * phaseC (-(Real.pi / 8)))
          • tensorHigh n 1 (-1)
              ((axisMat n P).mulVec
                ((rotOf (-(Real.pi / 8)) (axisMat n P)).mulVec ψ))

theorem tBlockNeg_branch_10 (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ψ : Fin (2 ^ n) → ℂ) :
    (projHalf (axisMat (n + 1) [(⟨n, .y⟩ : PFactor)]) false).mulVec
      ((projHalf (axisMat (n + 1) (P ++ [⟨n, .z⟩])) true).mulVec
        (tensorHigh n 1 (phaseC (-(Real.pi / 4))) ψ))
      = (-(2⁻¹ : ℂ) * phaseC (Real.pi / 8))
          • tensorHigh n 1 Complex.I
              ((axisMat n P).mulVec
                ((rotOf (-(Real.pi / 8)) (axisMat n P)).mulVec ψ))

theorem tBlockNeg_branch_11 (n : Nat) (P : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (hk : ∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x)
    (ψ : Fin (2 ^ n) → ℂ) :
    (projHalf (axisMat (n + 1) [(⟨n, .y⟩ : PFactor)]) true).mulVec
      ((projHalf (axisMat (n + 1) (P ++ [⟨n, .z⟩])) true).mulVec
        (tensorHigh n 1 (phaseC (-(Real.pi / 4))) ψ))
      = ((2⁻¹ : ℂ) * phaseC (Real.pi / 8))
          • tensorHigh n 1 (-Complex.I)
              ((rotOf (-(Real.pi / 8)) (axisMat n P)).mulVec ψ)

def lowBits (n : Nat) (m : Fin (2 ^ (n + 1))) : Fin (2 ^ n)

noncomputable def tensorHigh (n : Nat) (α β : ℂ) (ψ : Fin (2 ^ n) → ℂ) :
    Fin (2 ^ (n + 1)) → ℂ

theorem tensorHigh_congr (n : Nat) {α α' β β' : ℂ}
    {ψ ψ' : Fin (2 ^ n) → ℂ} (hα : α = α') (hβ : β = β') (hψ : ψ = ψ') :
    tensorHigh n α β ψ = tensorHigh n α' β' ψ'

theorem tensorHigh_smul (n : Nat) (c α β : ℂ) (ψ : Fin (2 ^ n) → ℂ) :
    tensorHigh n (c * α) (c * β) ψ = c • tensorHigh n α β ψ

theorem lowBits_testBit (n : Nat) (m : Fin (2 ^ (n + 1))) (q : Nat)
    (hq : q < n) :
    ((lowBits n m : Fin (2 ^ n)) : Nat).testBit q = (m : Nat).testBit q

theorem testBit_high_of_lt (n : Nat) (m : Fin (2 ^ (n + 1))) :
    (m : Nat).testBit n = decide ((m : Nat) ≥ 2 ^ n)

theorem joint_index_eq (n : Nat) (m : Fin (2 ^ (n + 1))) :
    (m : Nat) = (if (m : Nat).testBit n then 2 ^ n else 0)
      + ((lowBits n m : Fin (2 ^ n)) : Nat)

theorem zMat_mulVec (n t : Nat) (ht : t < n) (v : Fin (2 ^ n) → ℂ)
    (i : Fin (2 ^ n)) :
    ((axisMat n [(⟨t, .z⟩ : PFactor)]).mulVec v) i
      = (if (i : Nat).testBit t then -1 else 1) * v i

theorem xMat_mulVec (n t : Nat) (ht : t < n) (v : Fin (2 ^ n) → ℂ)
    (i : Fin (2 ^ n)) :
    ((axisMat n [(⟨t, .x⟩ : PFactor)]).mulVec v) i = v (flipT n t ht i)

theorem lowBits_flip (n q : Nat) (hq : q < n) (m : Fin (2 ^ (n + 1))) :
    lowBits n (flipT (n + 1) q (by omega) m)
      = flipT n q hq (lowBits n m)

theorem lowBits_flip_high (n : Nat) (m : Fin (2 ^ (n + 1))) :
    lowBits n (flipT (n + 1) n (by omega) m) = lowBits n m

theorem mulVec_zq_tensorHigh (n q : Nat) (hq : q < n) (α β : ℂ)
    (ψ : Fin (2 ^ n) → ℂ) :
    (axisMat (n + 1) [(⟨q, .z⟩ : PFactor)]).mulVec (tensorHigh n α β ψ)
      = tensorHigh n α β ((axisMat n [(⟨q, .z⟩ : PFactor)]).mulVec ψ)

theorem mulVec_xq_tensorHigh (n q : Nat) (hq : q < n) (α β : ℂ)
    (ψ : Fin (2 ^ n) → ℂ) :
    (axisMat (n + 1) [(⟨q, .x⟩ : PFactor)]).mulVec (tensorHigh n α β ψ)
      = tensorHigh n α β ((axisMat n [(⟨q, .x⟩ : PFactor)]).mulVec ψ)

theorem mulVec_zn_tensorHigh (n : Nat) (α β : ℂ) (ψ : Fin (2 ^ n) → ℂ) :
    (axisMat (n + 1) [(⟨n, .z⟩ : PFactor)]).mulVec (tensorHigh n α β ψ)
      = tensorHigh n α (-β) ψ

theorem mulVec_xn_tensorHigh (n : Nat) (α β : ℂ) (ψ : Fin (2 ^ n) → ℂ) :
    (axisMat (n + 1) [(⟨n, .x⟩ : PFactor)]).mulVec (tensorHigh n α β ψ)
      = tensorHigh n β α ψ

theorem mulVec_axis_tensorHigh (n : Nat) :
    ∀ (P : PauliProduct), sortedStrict P = true →
      PauliProduct.width P ≤ n →
      (∀ f ∈ P, f.kind = PKind.z ∨ f.kind = PKind.x) →
      ∀ (α β : ℂ) (ψ : Fin (2 ^ n) → ℂ),
        (axisMat (n + 1) P).mulVec (tensorHigh n α β ψ)
          = tensorHigh n α β ((axisMat n P).mulVec ψ)
  | [], _, _, _, α, β, ψ =>

theorem applyMat_I (n : Nat) :
    applyMat n FormalRV.Framework.Gate.I = 1

noncomputable def gphase : FormalRV.Framework.Gate → ℂ
  | .I => 1
  | .X _ => -Complex.I
  | .CX _ _ => phaseC (Real.pi / 4)
  | .CCX _ _ _ => -(phaseC (-(Real.pi / 8)))
  | .seq g₁ g₂ => gphase g₁ * gphase g₂

theorem applyNat_realized (n : Nat) :
    ∀ (g : FormalRV.Framework.Gate), width g ≤ n → ∀ (j : Fin (2 ^ n)),
      ∃ k : Fin (2 ^ n), ∀ b : Nat,
        Gate.applyNat g (fun c => (j : Nat).testBit c) b
          = (k : Nat).testBit b

theorem applyMat_seq (n : Nat) (g₁ g₂ : FormalRV.Framework.Gate)
    (hw₁ : width g₁ ≤ n) :
    applyMat n (.seq g₁ g₂) = applyMat n g₂ * applyMat n g₁

theorem gateRots_denote_applyNat (n : Nat) :
    ∀ (g : FormalRV.Framework.Gate), opsOK g = true → width g ≤ n →
      seqDenote n (gateRots g) = gphase g • applyMat n g

theorem gateRotSchedule_applyNat (n : Nat) (g : FormalRV.Framework.Gate)
    (hops : opsOK g = true) (hw : width g ≤ n) :
    RotProg.denote n (gateRotSchedule g) = gphase g • applyMat n g

theorem cuccaroRot_applyNat_4 :
    RotProg.denote (width (cuccaro_n_bit_adder_full 4 0)) (cuccaroRot 4 0)
      = gphase (cuccaro_n_bit_adder_full 4 0)
          • applyMat _ (cuccaro_n_bit_adder_full 4 0)

theorem seqDenote_append (n : Nat) (l₁ l₂ : List Rot) :
    seqDenote n (l₁ ++ l₂) = seqDenote n l₂ * seqDenote n l₁

def flipT (n t : Nat) (ht : t < n) (i : Fin (2 ^ n)) : Fin (2 ^ n)

theorem flipT_flipT (n t : Nat) (ht : t < n) (i : Fin (2 ^ n)) :
    flipT n t ht (flipT n t ht i) = i

theorem xMat_mul_apply (n t : Nat) (ht : t < n)
    (M : Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ) (i j : Fin (2 ^ n)) :
    (axisMat n [(⟨t, .x⟩ : PFactor)] * M) i j = M (flipT n t ht i) j

theorem mul_xMat_apply (n t : Nat) (ht : t < n)
    (M : Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ) (i j : Fin (2 ^ n)) :
    (M * axisMat n [(⟨t, .x⟩ : PFactor)]) i j = M i (flipT n t ht j)

theorem applyMat_CCX (n a b t : Nat) (hat : a ≠ t) (hbt : b ≠ t) (ht : t < n)
    (i j : Fin (2 ^ n)) :
    applyMat n (.CCX a b t) i j
      = if (i : Nat) = (if (j : Nat).testBit a && (j : Nat).testBit b
            then (j : Nat) ^^^ 2 ^ t else (j : Nat))
        then 1 else 0

theorem sort3_bits (f : Nat → Bool) (a b t : Nat) :
    (f (sort3 a b t).1 && f (sort3 a b t).2.1 && f (sort3 a b t).2.2)
      = (f a && f b && f t)

theorem testBit_xor_self_bit (m t : Nat) :
    (m ^^^ 2 ^ t).testBit t = !m.testBit t

theorem had_conj_core (n a b t : Nat) (hat : a ≠ t) (hbt : b ≠ t)
    (ht : t < n) :
    (axisMat n [(⟨t, .z⟩ : PFactor)] + axisMat n [(⟨t, .x⟩ : PFactor)])
        * Matrix.diagonal (fun m : Fin (2 ^ n) =>
            if (m : Nat).testBit a && (m : Nat).testBit b
                && (m : Nat).testBit t then (-1 : ℂ) else 1)
        * (axisMat n [(⟨t, .z⟩ : PFactor)] + axisMat n [(⟨t, .x⟩ : PFactor)])
      = (2 : ℂ) • applyMat n (.CCX a b t)

theorem ccx_rots_applyNat (n a b t : Nat)
    (hab : a ≠ b) (hat : a ≠ t) (hbt : b ≠ t)
    (ha : a < n) (hb : b < n) (ht : t < n) :
    seqDenote n (gateRots (.CCX a b t))
      = (-(phaseC (-(Real.pi / 8)))) • applyMat n (.CCX a b t)

theorem rotOf_diagonal {N : Type*} [Fintype N] [DecidableEq N]
    (θ : ℝ) (d : N → ℂ) :
    rotOf θ (Matrix.diagonal d)
      = Matrix.diagonal (fun i =>
          (Real.cos θ : ℂ) - (Real.sin θ : ℂ) * Complex.I * d i)

theorem axisMat_cons_split (n : Nat) (f : PFactor) (P : PauliProduct)
    (hs : sortedStrict (f :: P) = true) :
    axisMat n (f :: P) = axisMat n [f] * axisMat n P

noncomputable def zsgn (q : Nat) (m : Fin (2 ^ n)) : ℂ

theorem axisMat_zz_diag (n x y : Nat) (hxy : x < y) (hy : y < n) :
    axisMat n [(⟨x, .z⟩ : PFactor), ⟨y, .z⟩]
      = Matrix.diagonal (fun m => zsgn x m * zsgn y m)

theorem axisMat_zzz_diag (n x y z : Nat) (hxy : x < y) (hyz : y < z)
    (hz : z < n) :
    axisMat n [(⟨x, .z⟩ : PFactor), ⟨y, .z⟩, ⟨z, .z⟩]
      = Matrix.diagonal (fun m => zsgn x m * (zsgn y m * zsgn z m))

theorem phase_factor_pos (θ : ℝ) :
    (Real.cos θ : ℂ) - (Real.sin θ : ℂ) * Complex.I * 1 = phaseC (-θ)

theorem phase_factor_neg (θ : ℝ) :
    (Real.cos θ : ℂ) - (Real.sin θ : ℂ) * Complex.I * (-1) = phaseC θ

theorem neg_one_eq_phaseC_pi : (-1 : ℂ) = phaseC Real.pi

noncomputable def cczMat (n x y z : Nat) :
    Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ

theorem ccz_rots_denote (n x y z : Nat) (hxy : x < y) (hyz : y < z)
    (hz : z < n) :
    seqDenote n ((cczGate x y z).flatten)
      = phaseC (-(Real.pi / 8)) • cczMat n x y z

theorem rot_eighth_sq {M : Matrix m m ℂ} (hM : M * M = 1) :
    rotOf (Real.pi / 8) M * rotOf (Real.pi / 8) M = rotOf (Real.pi / 4) M

theorem rot_quarter_sq {M : Matrix m m ℂ} (hM : M * M = 1) :
    rotOf (Real.pi / 4) M * rotOf (Real.pi / 4) M = rotOf (Real.pi / 2) M

theorem rot_half_sq {M : Matrix m m ℂ} (hM : M * M = 1) :
    rotOf (Real.pi / 2) M * rotOf (Real.pi / 2) M = -1

theorem conj_anticomm {M N : Matrix m m ℂ} (hM : M * M = 1)
    (hMN : M * N = -(N * M)) : M * N * M = -N

theorem conj_axis_invol {M N : Matrix m m ℂ} (hM : M * M = 1)
    (hN : N * N = 1) (hMN : M * N = -(N * M)) :
    ((-Complex.I) • (M * N)) * ((-Complex.I) • (M * N)) = 1

theorem rot_quarter_push {M N : Matrix m m ℂ} (hM : M * M = 1)
    (hMN : M * N = -(N * M)) (φ : ℝ) :
    rotOf (Real.pi / 4) M * rotOf φ N
      = rotOf φ ((-Complex.I) • (M * N)) * rotOf (Real.pi / 4) M

theorem rot_braid {M N : Matrix m m ℂ} (hM : M * M = 1)
    (hMN : M * N = -(N * M)) :
    rotOf (Real.pi / 4) M * rotOf (Real.pi / 4) N * rotOf (Real.pi / 4) M
      = (-Complex.I) • ((((Real.sqrt 2 : ℝ) / 2 : ℝ) : ℂ) • (M + N))

theorem pauliZX_anticomm :
    Pauli.toMatrix .Z * Pauli.toMatrix .X
      = -(Pauli.toMatrix .X * Pauli.toMatrix .Z)

theorem hMat_eq_sum :
    hMat = (((Real.sqrt 2 : ℝ) / 2 : ℝ) : ℂ)
      • (Pauli.toMatrix .X + Pauli.toMatrix .Z)

theorem dict_H_from_braid :
    rotOf (Real.pi / 4) (Pauli.toMatrix .Z)
        * rotOf (Real.pi / 4) (Pauli.toMatrix .X)
        * rotOf (Real.pi / 4) (Pauli.toMatrix .Z)
      = (-Complex.I) • hMat

theorem axisMat_anticomm (n : Nat) {P Q : PauliProduct}
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (h : acCount P Q % 2 = 1) :
    axisMat n P * axisMat n Q = -(axisMat n Q * axisMat n P)

theorem acCount_ZX_self (q : Nat) :
    acCount [(⟨q, .z⟩ : PFactor)] [(⟨q, .x⟩ : PFactor)] = 1

theorem hGate_denote (n q : Nat) (hq : q + 1 ≤ n) :
    seqDenote n ((hGate q).flatten)
      = (-Complex.I) • ((((Real.sqrt 2 : ℝ) / 2 : ℝ) : ℂ)
          • (axisMat n [⟨q, .z⟩] + axisMat n [⟨q, .x⟩]))

def mulP (f g : Nat → Pauli) (k : Nat) : Pauli

theorem opsMat_mul_pointwise (n : Nat) (f g : Nat → Pauli)
    (h : ∀ k, f k = .I ∨ g k = .I) :
    opsMat n f * opsMat n g = opsMat n (mulP f g)

theorem kindFn_single (q : Nat) (k : PKind) (i : Nat) :
    kindFn [(⟨q, k⟩ : PFactor)] i
      = if q = i then pkindToBQ k else Pauli.I

theorem kindFn_pair (a b : PFactor) (i : Nat) :
    kindFn [a, b] i
      = if a.qubit = i then pkindToBQ a.kind
        else if b.qubit = i then pkindToBQ b.kind else Pauli.I

theorem pkindToBQ_ne_I (k : PKind) : pkindToBQ k ≠ Pauli.I

theorem axisMat_mk2_split (n c t : Nat) (kc kt : PKind) (hct : c ≠ t) :
    axisMat n (mk2 c kc t kt)
      = axisMat n [⟨c, kc⟩] * axisMat n [⟨t, kt⟩]

theorem commF_singles_disjoint (c t : Nat) (kc kt : PKind) (h : t ≠ c) :
    commF [(⟨c, kc⟩ : PFactor)] [(⟨t, kt⟩ : PFactor)] = true

theorem rot_controlled_pauli {A B : Matrix m m ℂ}
    (hA : A * A = 1) (hB : B * B = 1) (hAB : A * B = B * A) :
    rotOf (-(Real.pi / 4)) B * rotOf (-(Real.pi / 4)) A
        * rotOf (Real.pi / 4) (A * B)
      = phaseC (Real.pi / 4) • ((2 : ℂ)⁻¹ • (1 + A + B - A * B))

theorem cnot_rots_denote (n c t : Nat) (hct : c ≠ t) (hc : c + 1 ≤ n) :
    seqDenote n (gateRots (.CX c t))
      = phaseC (Real.pi / 4) •
          ((2 : ℂ)⁻¹ • (1 + axisMat n [⟨c, .z⟩] + axisMat n [⟨t, .x⟩]
            - axisMat n [⟨c, .z⟩] * axisMat n [⟨t, .x⟩]))

noncomputable def csDagMat (n t : Nat) :
    Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ

theorem csDag_rots_denote (n t : Nat) (ht : t + 1 < n) :
    seqDenote n (csDagRots t) = phaseC (Real.pi / 8) • csDagMat n t

noncomputable def hadSum (n q : Nat) : Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ

noncomputable def hLayerMat (n : Nat) : Nat → Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ
  | 0 => 1
  | k + 1 => hadSum n k * hLayerMat n k

theorem hLayer_denote (n : Nat) :
    ∀ k, k ≤ n →
      seqDenote n (hLayerRots k)
        = ((-Complex.I) * (((Real.sqrt 2 : ℝ) / 2 : ℝ) : ℂ)) ^ k
            • hLayerMat n k

noncomputable def ladderMat (n : Nat) : Nat → Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ
  | 0 => 1
  | t + 1 => ladderMat n t * hadSum n t * csDagMat n t

theorem ladderLow_denote (n : Nat) :
    ∀ t, t < n →
      seqDenote n (aqftLadderLow t)
        = ((-Complex.I) * (((Real.sqrt 2 : ℝ) / 2 : ℝ) : ℂ)
            * phaseC (Real.pi / 8)) ^ t • ladderMat n t

theorem swapRots_denote (n i j : Nat) (hij : i ≠ j) (hi : i < n) (hj : j < n) :
    seqDenote n (swapRots i j)
      = phaseC (Real.pi / 4) ^ 3
          • (applyMat n (.CX i j) * applyMat n (.CX j i)
              * applyMat n (.CX i j))

noncomputable def bitRevMat (n k : Nat) : Nat → Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ
  | 0 => 1
  | i + 1 => (applyMat n (.CX i (k - 1 - i)) * applyMat n (.CX (k - 1 - i) i)
      * applyMat n (.CX i (k - 1 - i))) * bitRevMat n k i

theorem bitRev_denote (n k : Nat) (hk : k ≤ n) :
    seqDenote n (bitRevRots k)
      = (phaseC (Real.pi / 4) ^ 3) ^ (k / 2) • bitRevMat n k (k / 2)

noncomputable def iqftMat (n k : Nat) : Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ

noncomputable def iqftPhase (k : Nat) : ℂ

theorem aqft2_denote (n k : Nat) (hk : k + 1 ≤ n) :
    seqDenote n (aqft2Rots (k + 1)) = iqftPhase k • iqftMat n k

theorem shorQPE_rots_denote (n k : Nat) (oracleG : FormalRV.Framework.Gate)
    (hops : opsOK oracleG = true) (hw : FormalRV.Resource.width oracleG ≤ n)
    (hk : k + 1 ≤ n) :
    seqDenote n (qpeRots (k + 1) (gateRots oracleG))
      = (iqftPhase k * gphase oracleG
            * ((-Complex.I) * (((Real.sqrt 2 : ℝ) / 2 : ℝ) : ℂ)) ^ (k + 1))
          • (iqftMat n k * applyMat n oracleG * hLayerMat n (k + 1))

theorem shorQPE_schedule_denote (n k : Nat) (oracleG : FormalRV.Framework.Gate)
    (hops : opsOK oracleG = true) (hw : FormalRV.Resource.width oracleG ≤ n)
    (hk : k + 1 ≤ n)
    (hb : ∀ r ∈ qpeRots (k + 1) (gateRots oracleG),
        sortedStrict r.axis = true ∧ PauliProduct.width r.axis ≤ n) :
    RotProg.denote n (qpeSchedule (k + 1) (gateRots oracleG))
      = (iqftPhase k * gphase oracleG
            * ((-Complex.I) * (((Real.sqrt 2 : ℝ) / 2 : ℝ) : ℂ)) ^ (k + 1))
          • (iqftMat n k * applyMat n oracleG * hLayerMat n (k + 1))

theorem shor15_schedule_denote :
    RotProg.denote 7 (qpeSchedule 3 (gateRots (shorModExpVerified 1 15 7 13)))
      = (iqftPhase 2 * gphase (shorModExpVerified 1 15 7 13)
            * ((-Complex.I) * (((Real.sqrt 2 : ℝ) / 2 : ℝ) : ℂ)) ^ 3)
          • (iqftMat 7 2 * applyMat 7 (shorModExpVerified 1 15 7 13)
              * hLayerMat 7 3)

noncomputable def phaseC (θ : ℝ) : ℂ

theorem phaseC_eq (θ : ℝ) :
    phaseC θ = (Real.cos θ : ℂ) + (Real.sin θ : ℂ) * Complex.I

theorem phaseC_add (a b : ℝ) : phaseC a * phaseC b = phaseC (a + b)

theorem rotZ_eq_diag (θ : ℝ) :
    rotOf θ (Pauli.toMatrix .Z) = !![phaseC (-θ), 0; 0, phaseC θ]

theorem dict_T :
    rotOf (Real.pi / 8) (Pauli.toMatrix .Z)
      = phaseC (-(Real.pi / 8)) • !![1, 0; 0, phaseC (Real.pi / 4)]

theorem dict_S :
    rotOf (Real.pi / 4) (Pauli.toMatrix .Z)
      = phaseC (-(Real.pi / 4)) • !![1, 0; 0, Complex.I]

noncomputable def hMat : Matrix (Fin 2) (Fin 2) ℂ

theorem dict_H :
    rotOf (Real.pi / 4) (Pauli.toMatrix .Z)
        * rotOf (Real.pi / 4) (Pauli.toMatrix .X)
        * rotOf (Real.pi / 4) (Pauli.toMatrix .Z)
      = (-Complex.I) • hMat

def transversalT4 : RotProg

example : RotProg.wf transversalT4 = true

example : rotDepth transversalT4 = 1

example : countPi8 transversalT4 = 4

example : RotProg.width transversalT4 = 4

def xxzzLayer : RotProg

example : RotProg.wf xxzzLayer = true

example : rotDepth xxzzLayer = 1

def cnotLayer (c t : Nat) : RotProg

example : RotProg.wf (cnotLayer 0 1) = true

example : rotDepth (cnotLayer 0 1) = 1

example : rotDepth (cnotGate 0 1) = 3

def twoCnotLayer : RotProg

example : RotProg.wf twoCnotLayer = true

example : rotDepth twoCnotLayer = 1

example : RotProg.wf (cczLayer 0 1 2) = true

example : rotDepth (cczLayer 0 1 2) = 1

example : countPi8 (cczLayer 0 1 2) = 7

example : RotLayer.wf
    [⟨false, .piEighth, [⟨0, .x⟩]⟩, ⟨false, .piEighth, [⟨0, .z⟩]⟩] = false

example : RotProg.wf
    [[⟨false, .piEighth, [⟨0, .x⟩]⟩], [⟨false, .piEighth, [⟨0, .z⟩]⟩]] = true

def mixedProg : RotProg

example : RotProg.wf mixedProg = true

example : rotDepth mixedProg = 3

example : countPi8 mixedProg = 2

example : countRot mixedProg = 5

def cuccaroRot (bits q_start : Nat) : RotProg

theorem cuccaroRot_countPi8 (bits q_start : Nat) :
    countPi8 (cuccaroRot bits q_start) = 14 * bits

theorem cuccaroRot_denote_4 :
    RotProg.denote (width (cuccaro_n_bit_adder_full 4 0)) (cuccaroRot 4 0)
      = seqDenote _ (gateRots (cuccaro_n_bit_adder_full 4 0))

example : RotProg.wf (cuccaroRot 2 0) = true

example : (gateRots (cuccaro_n_bit_adder_full 2 0)).length = 76

example : rotDepth (cuccaroRot 2 0) = 20

def cuccaroAddConstRot (bits q_start c : Nat) : RotProg

theorem cuccaroAddConstRot_countPi8 (bits q_start c : Nat) :
    countPi8 (cuccaroAddConstRot bits q_start c) = 14 * bits

theorem cuccaroAddConstRot_denote_3 :
    RotProg.denote (width (cuccaro_addConstGate 3 0 5))
        (cuccaroAddConstRot 3 0 5)
      = seqDenote _ (gateRots (cuccaro_addConstGate 3 0 5))

def cuccaroSubConstRot (bits q_start N : Nat) : RotProg

theorem cuccaroSubConstRot_countPi8 (bits q_start N : Nat) :
    countPi8 (cuccaroSubConstRot bits q_start N) = 14 * bits

def cuccaroCompareRot (bits q_start N : Nat) : RotProg

theorem cuccaroCompareRot_countPi8 (bits q_start N : Nat) :
    countPi8 (cuccaroCompareRot bits q_start N) = 7 * bits

def cuccaroSubForwardRot (bits q_start N : Nat) : RotProg

theorem cuccaroSubForwardRot_countPi8 (bits q_start N : Nat) :
    countPi8 (cuccaroSubForwardRot bits q_start N) = 7 * bits

def cuccaroSubReverseRot (bits q_start N : Nat) : RotProg

theorem cuccaroSubReverseRot_countPi8 (bits q_start N : Nat) :
    countPi8 (cuccaroSubReverseRot bits q_start N) = 7 * bits

def gidneyRot (n : Nat) : RotProg

theorem gidneyRot_countPi8 (n : Nat) :
    countPi8 (gidneyRot (n + 2)) = 14 * (n + 2)

theorem gidneyRot_denote_2 :
    RotProg.denote (width (gidney_adder 2)) (gidneyRot 2)
      = seqDenote _ (gateRots (gidney_adder 2))

def gidneyPatchedRot (n : Nat) : RotProg

theorem gidneyPatchedRot_countPi8 (n : Nat) :
    countPi8 (gidneyPatchedRot (n + 2)) = 14 * (n + 2)

theorem gidneyPatchedRot_denote_2 :
    RotProg.denote (width (gidney_adder_full_faithful_no_measurement_patched 2))
        (gidneyPatchedRot 2)
      = seqDenote _ (gateRots (gidney_adder_full_faithful_no_measurement_patched 2))

def gidneyForwardRevRot (n : Nat) : RotProg

theorem gidneyForwardRevRot_countPi8 (n : Nat) :
    countPi8 (gidneyForwardRevRot (n + 2)) = 7 * (n + 2)

def shorModExpVerifiedRot (bits N a ainv : Nat) : RotProg

theorem shorModExpVerifiedRot_countPi8 (bits N a ainv : Nat)
    (hcop : Nat.Coprime a N) (hcopinv : Nat.Coprime ainv N)
    (hpos : 0 < ainv) (hlt : ainv < N) (hodd : Odd N) (h1 : 1 < N) :
    countPi8 (shorModExpVerifiedRot bits N a ainv) = 224 * bits ^ 3

theorem shorModExpVerifiedRot_denote_1 :
    RotProg.denote (width (shorModExpVerified 1 15 7 13))
        (shorModExpVerifiedRot 1 15 7 13)
      = seqDenote _ (gateRots (shorModExpVerified 1 15 7 13))

example : countPi8 (shorModExpVerifiedRot 2 15 7 13) = 1792

def shorModExpRot (bits N a : Nat) : RotProg

theorem shorModExpRot_countPi8 (bits N a : Nat)
    (hcop : Nat.Coprime a N) (hodd : Odd N) (h1 : 1 < N) :
    countPi8 (shorModExpRot bits N a) = 112 * bits ^ 3

def modMultConstRot (bits N a : Nat) : RotProg

theorem modMultConstRot_countPi8 (bits N a : Nat)
    (hcop : Nat.Coprime a N) (hodd : Odd N) (h1 : 1 < N) :
    countPi8 (modMultConstRot bits N a) = 56 * bits ^ 2

theorem modMultConstRot_denote_2_15_7 :
    RotProg.denote (width (modmult_const_gate 2 15 7)) (modMultConstRot 2 15 7)
      = seqDenote _ (gateRots (modmult_const_gate 2 15 7))

def modMultMCPRot (bits N a ainv : Nat) : RotProg

theorem modMultMCPRot_countPi8 (bits N a ainv : Nat)
    (hcop : Nat.Coprime a N) (hcopinv : Nat.Coprime ainv N)
    (hpos : 0 < ainv) (hlt : ainv < N) (hodd : Odd N) (h1 : 1 < N) :
    countPi8 (modMultMCPRot bits N a ainv) = 112 * bits ^ 2

theorem modMultMCPRot_denote_2_15 :
    RotProg.denote (width (modmult_MCP_gate 2 15 7 13)) (modMultMCPRot 2 15 7 13)
      = seqDenote _ (gateRots (modmult_MCP_gate 2 15 7 13))

example : countPi8 (modMultMCPRot 2 15 7 13) = 448

def cuccaroModAddRot (bits N c : Nat) : RotProg

theorem cuccaroModAddRot_countPi8 (bits N c : Nat) :
    countPi8 (cuccaroModAddRot bits N c)
      = if c = 0 then 0 else 56 * bits

theorem cuccaroModAddRot_denote_3 :
    RotProg.denote (width (sqir_style_modAddConst_clean_gate 3 5 2))
        (cuccaroModAddRot 3 5 2)
      = seqDenote _ (gateRots (sqir_style_modAddConst_clean_gate 3 5 2))

def cuccaroCtrlModAddRot (bits q_start N c controlIdx flagPos : Nat) : RotProg

theorem cuccaroCtrlModAddRot_countPi8
    (bits q_start N c controlIdx flagPos : Nat) :
    countPi8 (cuccaroCtrlModAddRot bits q_start N c controlIdx flagPos)
      = if c = 0 then 0 else 56 * bits

def gidneyAddConstRot (bits c : Nat) : RotProg

theorem gidneyAddConstRot_countPi8 (n c : Nat) :
    countPi8 (gidneyAddConstRot (n + 2) c) = 14 * (n + 2)

theorem gidneyAddConstRot_denote_2 :
    RotProg.denote (width (addConstGate 2 1)) (gidneyAddConstRot 2 1)
      = seqDenote _ (gateRots (addConstGate 2 1))

def gidneySubConstRot (bits N : Nat) : RotProg

theorem gidneySubConstRot_countPi8 (n N : Nat) :
    countPi8 (gidneySubConstRot (n + 2) N) = 14 * (n + 2)

def gidneyCondAddRot (bits N flagIdx : Nat) : RotProg

theorem gidneyCondAddRot_countPi8 (n N flagIdx : Nat) :
    countPi8 (gidneyCondAddRot (n + 2) N flagIdx) = 14 * (n + 2)

def gidneyModAddRot (bits N c : Nat) : RotProg

theorem gidneyModAddRot_countPi8 (n N c : Nat) :
    countPi8 (gidneyModAddRot (n + 1) N c) = 70 * (n + 2)

def gidneyCtrlModAddRot (bits N c controlIdx flagIdx : Nat) : RotProg

theorem gidneyCtrlModAddRot_countPi8 (n N c controlIdx flagIdx : Nat) :
    countPi8 (gidneyCtrlModAddRot (n + 1) N c controlIdx flagIdx)
      = 70 * (n + 2) + 14

theorem cuccaroAddConstRot_applyNat :
    RotProg.denote (Resource.width (cuccaro_addConstGate 3 0 5)) (cuccaroAddConstRot 3 0 5)
      = gphase (cuccaro_addConstGate 3 0 5)
          • applyMat _ (cuccaro_addConstGate 3 0 5)

theorem cuccaroSubConstRot_applyNat :
    RotProg.denote (Resource.width (cuccaro_subConstGate 3 0 5)) (cuccaroSubConstRot 3 0 5)
      = gphase (cuccaro_subConstGate 3 0 5)
          • applyMat _ (cuccaro_subConstGate 3 0 5)

theorem cuccaroCompareRot_applyNat :
    RotProg.denote (Resource.width (cuccaro_compareConstForwardGate 3 0 5))
        (cuccaroCompareRot 3 0 5)
      = gphase (cuccaro_compareConstForwardGate 3 0 5)
          • applyMat _ (cuccaro_compareConstForwardGate 3 0 5)

theorem cuccaroSubForwardRot_applyNat :
    RotProg.denote (Resource.width (cuccaro_subConstForwardOnlyGate 3 0 5))
        (cuccaroSubForwardRot 3 0 5)
      = gphase (cuccaro_subConstForwardOnlyGate 3 0 5)
          • applyMat _ (cuccaro_subConstForwardOnlyGate 3 0 5)

theorem cuccaroSubReverseRot_applyNat :
    RotProg.denote (Resource.width (cuccaro_subConstReverseOnlyGate 3 0 5))
        (cuccaroSubReverseRot 3 0 5)
      = gphase (cuccaro_subConstReverseOnlyGate 3 0 5)
          • applyMat _ (cuccaro_subConstReverseOnlyGate 3 0 5)

theorem gidneyRot_applyNat :
    RotProg.denote (Resource.width (gidney_adder 2)) (gidneyRot 2)
      = gphase (gidney_adder 2) • applyMat _ (gidney_adder 2)

theorem gidneyPatchedRot_applyNat :
    RotProg.denote (Resource.width (gidney_adder_full_faithful_no_measurement_patched 2))
        (gidneyPatchedRot 2)
      = gphase (gidney_adder_full_faithful_no_measurement_patched 2)
          • applyMat _ (gidney_adder_full_faithful_no_measurement_patched 2)

theorem gidneyForwardRevRot_applyNat :
    RotProg.denote (Resource.width (gidney_adder_forward_faithful_full_reverse_patched 2))
        (gidneyForwardRevRot 2)
      = gphase (gidney_adder_forward_faithful_full_reverse_patched 2)
          • applyMat _ (gidney_adder_forward_faithful_full_reverse_patched 2)

theorem cuccaroModAddRot_applyNat :
    RotProg.denote (Resource.width (sqir_style_modAddConst_clean_gate 3 5 2))
        (cuccaroModAddRot 3 5 2)
      = gphase (sqir_style_modAddConst_clean_gate 3 5 2)
          • applyMat _ (sqir_style_modAddConst_clean_gate 3 5 2)

theorem cuccaroCtrlModAddRot_applyNat :
    RotProg.denote (Resource.width (sqir_style_controlledModAddConst_gate 3 2 5 2 1 0))
        (cuccaroCtrlModAddRot 3 2 5 2 1 0)
      = gphase (sqir_style_controlledModAddConst_gate 3 2 5 2 1 0)
          • applyMat _ (sqir_style_controlledModAddConst_gate 3 2 5 2 1 0)

theorem gidneyAddConstRot_applyNat :
    RotProg.denote (Resource.width (addConstGate 2 1)) (gidneyAddConstRot 2 1)
      = gphase (addConstGate 2 1) • applyMat _ (addConstGate 2 1)

theorem gidneySubConstRot_applyNat :
    RotProg.denote (Resource.width (subConstGate 2 1)) (gidneySubConstRot 2 1)
      = gphase (subConstGate 2 1) • applyMat _ (subConstGate 2 1)

theorem gidneyCondAddRot_applyNat :
    RotProg.denote (Resource.width (conditionalAddConstGate 2 1 8))
        (gidneyCondAddRot 2 1 8)
      = gphase (conditionalAddConstGate 2 1 8)
          • applyMat _ (conditionalAddConstGate 2 1 8)

theorem gidneyModAddRot_applyNat :
    RotProg.denote (Resource.width (modAddConstGate 2 3 1)) (gidneyModAddRot 2 3 1)
      = gphase (modAddConstGate 2 3 1) • applyMat _ (modAddConstGate 2 3 1)

theorem gidneyCtrlModAddRot_applyNat :
    RotProg.denote (Resource.width (controlledModAddConstGate 2 3 1 9 10))
        (gidneyCtrlModAddRot 2 3 1 9 10)
      = gphase (controlledModAddConstGate 2 3 1 9 10)
          • applyMat _ (controlledModAddConstGate 2 3 1 9 10)

theorem modMultConstRot_applyNat :
    RotProg.denote (Resource.width (modmult_const_gate 2 15 7)) (modMultConstRot 2 15 7)
      = gphase (modmult_const_gate 2 15 7)
          • applyMat _ (modmult_const_gate 2 15 7)

theorem modMultMCPRot_applyNat :
    RotProg.denote (Resource.width (modmult_MCP_gate 2 15 7 13)) (modMultMCPRot 2 15 7 13)
      = gphase (modmult_MCP_gate 2 15 7 13)
          • applyMat _ (modmult_MCP_gate 2 15 7 13)

theorem shorModExpVerifiedRot_applyNat :
    RotProg.denote (Resource.width (shorModExpVerified 1 15 7 13))
        (shorModExpVerifiedRot 1 15 7 13)
      = gphase (shorModExpVerified 1 15 7 13)
          • applyMat _ (shorModExpVerified 1 15 7 13)

theorem shorModExpRot_applyNat :
    RotProg.denote (Resource.width (shorModExp 1 15 7)) (shorModExpRot 1 15 7)
      = gphase (shorModExp 1 15 7) • applyMat _ (shorModExp 1 15 7)

theorem unaryLookupRot_applyNat :
    RotProg.denote (Resource.width (unary_lookup_multi_iteration 2 [([0], [5])]))
        (unaryLookupRot 2 [([0], [5])])
      = gphase (unary_lookup_multi_iteration 2 [([0], [5])])
          • applyMat _ (unary_lookup_multi_iteration 2 [([0], [5])])

theorem grayLookupRot_applyNat :
    RotProg.denote (Resource.width (grayLookupReadAt 2 (fun i => 6 + i) 1 (fun _ => 1)))
        (grayLookupRot 2 (fun i => 6 + i) 1 (fun _ => 1))
      = gphase (grayLookupReadAt 2 (fun i => 6 + i) 1 (fun _ => 1))
          • applyMat _ (grayLookupReadAt 2 (fun i => 6 + i) 1 (fun _ => 1))

theorem windowedMulRot_applyNat :
    RotProg.denote (Resource.width (windowedMulCircuit 2 4 3 2)) (windowedMulRot 2 4 3 2)
      = gphase (windowedMulCircuit 2 4 3 2)
          • applyMat _ (windowedMulCircuit 2 4 3 2)

theorem windowedModNMulRot_applyNat :
    RotProg.denote (Resource.width (windowedModNMulCircuit 2 4 3 7 2))
        (windowedModNMulRot 2 4 3 7 2)
      = gphase (windowedModNMulCircuit 2 4 3 7 2)
          • applyMat _ (windowedModNMulCircuit 2 4 3 7 2)

theorem windowedModNInPlaceRot_applyNat :
    RotProg.denote (Resource.width (windowedModNMulGate 2 4 7 2 3 5))
        (windowedModNInPlaceRot 2 4 7 2 3 5)
      = gphase (windowedModNMulGate 2 4 7 2 3 5)
          • applyMat _ (windowedModNMulGate 2 4 7 2 3 5)

theorem grayWindowedMulRot_applyNat :
    RotProg.denote (Resource.width (grayWindowedMulCircuitOf cuccaroAdder 2 4 3 2))
        (grayWindowedMulRot 2 4 3 2)
      = gphase (grayWindowedMulCircuitOf cuccaroAdder 2 4 3 2)
          • applyMat _ (grayWindowedMulCircuitOf cuccaroAdder 2 4 3 2)

def unaryLookupRot (n_addr : Nat) (iters : List (List Nat × List Nat)) : RotProg

theorem unaryLookupRot_countPi8 (n_addr : Nat)
    (iters : List (List Nat × List Nat)) :
    countPi8 (unaryLookupRot n_addr iters) = 14 * n_addr * iters.length

def grayLookupRot (w : Nat) (pos : Nat → Nat) (W : Nat) (T : Nat → Nat) : RotProg

theorem grayLookupRot_countPi8 (w : Nat) (pos : Nat → Nat) (W : Nat)
    (T : Nat → Nat) :
    countPi8 (grayLookupRot w pos W T) = 14 * (2 ^ w - 1)

def windowedMulRot (w bits a numWin : Nat) : RotProg

theorem windowedMulRot_countPi8 (w bits a numWin : Nat) :
    countPi8 (windowedMulRot w bits a numWin)
      = numWin * (28 * w * 2 ^ w + 14 * bits)

def windowedModNMulRot (w bits a N numWin : Nat) : RotProg

theorem windowedModNMulRot_countPi8 (w bits a N numWin : Nat) :
    countPi8 (windowedModNMulRot w bits a N numWin)
      = numWin * (56 * w * 2 ^ w + 56 * bits)

def windowedModNInPlaceRot (w bits N numWin c cinv : Nat) : RotProg

theorem windowedModNInPlaceRot_countPi8 (w bits N numWin c cinv : Nat) :
    countPi8 (windowedModNInPlaceRot w bits N numWin c cinv)
      = 2 * numWin * (56 * w * 2 ^ w + 56 * bits)

def grayWindowedMulRot (w bits a numWin : Nat) : RotProg

theorem grayWindowedMulRot_countPi8 (w bits a numWin : Nat) :
    countPi8 (grayWindowedMulRot w bits a numWin)
      = numWin * (28 * (2 ^ w - 1) + 14 * bits)

theorem windowedMulRot_denote_2_4_3_2 :
    RotProg.denote (Resource.width (windowedMulCircuit 2 4 3 2))
        (windowedMulRot 2 4 3 2)
      = seqDenote _ (gateRots (windowedMulCircuit 2 4 3 2))

theorem opsMat_one (n : Nat) : opsMat n (fun _ => Pauli.I) = 1

theorem opsMat_succ_apply (n : Nat) (f : Nat → Pauli)
    (i₁ j₁ : Fin (2 ^ n)) (i₂ j₂ : Fin 2) :
    opsMat (n + 1) f (finProdFinEquiv (i₁, i₂)) (finProdFinEquiv (j₁, j₂))
      = opsMat n (fun i => f (i + 1)) i₁ j₁ * (f 0).toMatrix i₂ j₂

theorem val_coe {n : Nat} (x : Fin (2 ^ n * 2)) :
    @Fin.val (2 ^ (n + 1)) x = @Fin.val (2 ^ n * 2) x

theorem pair_val {n : Nat} (i₁ : Fin (2 ^ n)) (i₂ : Fin 2) :
    ((finProdFinEquiv (i₁, i₂) : Fin (2 ^ n * 2)) : Nat)
      = (i₂ : Nat) + 2 * (i₁ : Nat)

theorem pair_testBit_zero {n : Nat} (i₁ : Fin (2 ^ n)) (i₂ : Fin 2) :
    ((finProdFinEquiv (i₁, i₂) : Fin (2 ^ n * 2)) : Nat).testBit 0
      = decide ((i₂ : Nat) = 1)

theorem pair_testBit_succ {n : Nat} (i₁ : Fin (2 ^ n)) (i₂ : Fin 2) (k : Nat) :
    ((finProdFinEquiv (i₁, i₂) : Fin (2 ^ n * 2)) : Nat).testBit (k + 1)
      = (i₁ : Nat).testBit k

theorem xor_one_split (a b : Nat) (hb : b < 2) :
    (b + 2 * a) ^^^ 1 = (1 - b) + 2 * a

theorem xor_pow_succ_split (a b : Nat) (hb : b < 2) (q : Nat) :
    (b + 2 * a) ^^^ 2 ^ (q + 1) = b + 2 * (a ^^^ 2 ^ q)

private theorem opsMat_single_z (n : Nat) :
    ∀ (q : Nat), q < n → ∀ (i j : Fin (2 ^ n)),
      opsMat n (fun k => if q = k then Pauli.Z else Pauli.I) i j
        = if (i : Nat) = (j : Nat)
          then (if (j : Nat).testBit q then -1 else 1) else 0

private theorem opsMat_single_x (n : Nat) :
    ∀ (q : Nat), q < n → ∀ (i j : Fin (2 ^ n)),
      opsMat n (fun k => if q = k then Pauli.X else Pauli.I) i j
        = if (i : Nat) = (j : Nat) ^^^ 2 ^ q then 1 else 0

theorem axisMat_single_z_apply (n q : Nat) (hq : q < n) (i j : Fin (2 ^ n)) :
    axisMat n [(⟨q, .z⟩ : PFactor)] i j
      = if (i : Nat) = (j : Nat)
        then (if (j : Nat).testBit q then -1 else 1) else 0

theorem axisMat_single_x_apply (n q : Nat) (hq : q < n) (i j : Fin (2 ^ n)) :
    axisMat n [(⟨q, .x⟩ : PFactor)] i j
      = if (i : Nat) = (j : Nat) ^^^ 2 ^ q then 1 else 0

noncomputable def applyMat (n : Nat) (g : FormalRV.Framework.Gate) :
    Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ

theorem applyMat_X (n q : Nat) (hq : q < n) (i j : Fin (2 ^ n)) :
    applyMat n (.X q) i j
      = if (i : Nat) = (j : Nat) ^^^ 2 ^ q then 1 else 0

theorem xGate_rots_applyNat (n q : Nat) (hq : q < n) :
    seqDenote n (gateRots (.X q)) = (-Complex.I) • applyMat n (.X q)

theorem axisMat_single_z_diag (n c : Nat) (hc : c < n) :
    axisMat n [(⟨c, .z⟩ : PFactor)]
      = Matrix.diagonal (fun k : Fin (2 ^ n) =>
          if (k : Nat).testBit c then (-1 : ℂ) else 1)

theorem testBit_xor_other {c t : Nat} (hct : c ≠ t) (m : Nat) :
    (m ^^^ 2 ^ t).testBit c = m.testBit c

theorem xor_two_pow_ne (m t : Nat) : m ^^^ 2 ^ t ≠ m

theorem applyMat_CX (n c t : Nat) (hct : c ≠ t) (ht : t < n)
    (i j : Fin (2 ^ n)) :
    applyMat n (.CX c t) i j
      = if (i : Nat) = (if (j : Nat).testBit c
            then (j : Nat) ^^^ 2 ^ t else (j : Nat))
        then 1 else 0

theorem cnot_rots_applyNat (n c t : Nat) (hct : c ≠ t) (hc : c < n)
    (ht : t < n) :
    seqDenote n (gateRots (.CX c t))
      = phaseC (Real.pi / 4) • applyMat n (.CX c t)

private theorem opsMat_single_y (n : Nat) :
    ∀ (q : Nat), q < n → ∀ (i j : Fin (2 ^ n)),
      opsMat n (fun k => if q = k then Pauli.Y else Pauli.I) i j
        = if (i : Nat) = (j : Nat) ^^^ 2 ^ q
          then (if (j : Nat).testBit q then -Complex.I else Complex.I)
          else 0

theorem axisMat_single_y_apply (n q : Nat) (hq : q < n) (i j : Fin (2 ^ n)) :
    axisMat n [(⟨q, .y⟩ : PFactor)] i j
      = if (i : Nat) = (j : Nat) ^^^ 2 ^ q
        then (if (j : Nat).testBit q then -Complex.I else Complex.I)
        else 0

def pauliAC : Pauli → Pauli → Bool
  | .X, .Y => true
  | .Y, .X => true
  | .X, .Z => true
  | .Z, .X => true
  | .Y, .Z => true
  | .Z, .Y => true
  | _,  _  => false

theorem pauli_mul_sign (p q : Pauli) :
    p.toMatrix * q.toMatrix
      = (if pauliAC p q then (-1 : ℂ) else 1) • (q.toMatrix * p.toMatrix)

theorem opsMat_succ (n : Nat) (f : Nat → Pauli) :
    opsMat (n + 1) f
      = Matrix.reindex finProdFinEquiv finProdFinEquiv
          (Matrix.kroneckerMap (· * ·) (opsMat n (fun i => f (i + 1)))
            (f 0).toMatrix)

theorem reindexKron_mul {n : Nat}
    (A B : Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ)
    (a b : Matrix (Fin 2) (Fin 2) ℂ) :
    Matrix.reindex finProdFinEquiv finProdFinEquiv
        (Matrix.kroneckerMap (· * · : ℂ → ℂ → ℂ) A a)
      * Matrix.reindex finProdFinEquiv finProdFinEquiv
          (Matrix.kroneckerMap (· * ·) B b)
      = Matrix.reindex finProdFinEquiv finProdFinEquiv
          (Matrix.kroneckerMap (· * ·) (A * B) (a * b))

private theorem countP_map_succ (p : Nat → Bool) (l : List Nat) :
    (l.map Nat.succ).countP p = l.countP (fun i => p (i + 1))

private theorem countP_range_succ_shift (p : Nat → Bool) (n : Nat) :
    (List.range (n + 1)).countP p
      = (List.range n).countP (fun i => p (i + 1)) + (if p 0 then 1 else 0)

theorem opsMat_mul_sign (n : Nat) (f g : Nat → Pauli) :
    opsMat n f * opsMat n g
      = ((-1 : ℂ) ^ ((List.range n).countP (fun i => pauliAC (f i) (g i)))) •
          (opsMat n g * opsMat n f)

theorem width_le_factor_lt {P : PauliProduct} {n : Nat}
    (h : PauliProduct.width P ≤ n) : ∀ f ∈ P, f.qubit < n

theorem kindFn_cons_self (f : PFactor) (t : PauliProduct) :
    kindFn (f :: t) f.qubit = pkindToBQ f.kind

theorem kindFn_cons_ne (f : PFactor) (t : PauliProduct) (i : Nat)
    (h : f.qubit ≠ i) : kindFn (f :: t) i = kindFn t i

theorem kindFn_eq_I_of_lt_lbound {lo : Nat} {P : PauliProduct}
    (h : lbound lo P = true) {i : Nat} (hi : i < lo) : kindFn P i = .I

theorem pauliAC_kind_lookup (k : PKind) (Q : PauliProduct) (i : Nat) :
    pauliAC (pkindToBQ k) (kindFn Q i) = overlapMismatch Q ⟨i, k⟩

private theorem countP_congr' {p q : Nat → Bool} :
    ∀ {l : List Nat}, (∀ a ∈ l, p a = q a) → l.countP p = l.countP q

private theorem countP_range_split (n a : Nat) (ha : a < n) (p q : Nat → Bool)
    (heq : ∀ j, j ≠ a → q j = p j) (hpa : p a = false) :
    (List.range n).countP q = (List.range n).countP p + (if q a then 1 else 0)

theorem acCount_dense (n : Nat) (P Q : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n) :
    (List.range n).countP (fun i => pauliAC (kindFn P i) (kindFn Q i))
      = acCount P Q

theorem axisMat_comm_of_commF (n : Nat) {P Q : PauliProduct}
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n)
    (h : commF P Q = true) :
    axisMat n P * axisMat n Q = axisMat n Q * axisMat n P

theorem Rot.denote_swap (n : Nat) (r s : Rot)
    (hs : sortedStrict s.axis = true) (hw : PauliProduct.width s.axis ≤ n)
    (h : commF s.axis r.axis = true) :
    Rot.denote n r * Rot.denote n s = Rot.denote n s * Rot.denote n r

example :  -- X₀X₁ and Z₀Z₁ overlap everywhere yet commute — now at the MATRIX level
    axisMat 2 [⟨0, .x⟩, ⟨1, .x⟩] * axisMat 2 [⟨0, .z⟩, ⟨1, .z⟩]
      = axisMat 2 [⟨0, .z⟩, ⟨1, .z⟩] * axisMat 2 [⟨0, .x⟩, ⟨1, .x⟩]

noncomputable def RAngle.val : RAngle → ℝ
  | .pi        => Real.pi
  | .piHalf    => Real.pi / 2
  | .piQuarter => Real.pi / 4
  | .piEighth  => Real.pi / 8

noncomputable def Rot.theta (r : Rot) : ℝ

noncomputable def rotOf (θ : ℝ) (M : Matrix m m ℂ) : Matrix m m ℂ

theorem rotOf_pi_div_two (M : Matrix m m ℂ) :
    rotOf (Real.pi / 2) M = (-Complex.I) • M

theorem rotOf_neg_pi_div_two (M : Matrix m m ℂ) :
    rotOf (-(Real.pi / 2)) M = Complex.I • M

theorem rotOf_mul_same [Fintype m] {M : Matrix m m ℂ} (hM : M * M = 1) (θ φ : ℝ) :
    rotOf θ M * rotOf φ M = rotOf (θ + φ) M

theorem rotOf_cancel [Fintype m] {M : Matrix m m ℂ} (hM : M * M = 1) (θ : ℝ) :
    rotOf θ M * rotOf (-θ) M = 1

theorem rotOf_comm [Fintype m] {M N : Matrix m m ℂ} (h : M * N = N * M) (θ φ : ℝ) :
    rotOf θ M * rotOf φ N = rotOf φ N * rotOf θ M

def pkindToBQ : PKind → Pauli
  | .x => .X
  | .y => .Y
  | .z => .Z

def kindFn (P : PauliProduct) (i : Nat) : Pauli

def toDenseOps (n : Nat) (P : PauliProduct) : PauliString

noncomputable def opsMat : (n : Nat) → (Nat → Pauli) → Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ
  | 0,     _ => 1
  | n + 1, f =>
      Matrix.reindex finProdFinEquiv finProdFinEquiv
        (Matrix.kroneckerMap (· * ·) (opsMat n (fun i => f (i + 1))) (f 0).toMatrix)

noncomputable def axisMat (n : Nat) (P : PauliProduct) :
    Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ

theorem opsMat_mul_self (n : Nat) (f : Nat → Pauli) :
    opsMat n f * opsMat n f = 1

theorem axisMat_mul_self (n : Nat) (P : PauliProduct) :
    axisMat n P * axisMat n P = 1

noncomputable def Rot.denote (n : Nat) (r : Rot) :
    Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ

noncomputable def RotLayer.denote (n : Nat) (L : RotLayer) :
    Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ

noncomputable def RotProg.denote (n : Nat) : RotProg → Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ
  | []     => 1
  | L :: p => RotProg.denote n p * RotLayer.denote n L

theorem RotLayer.denote_cons (n : Nat) (r : Rot) (L : RotLayer) :
    RotLayer.denote n (r :: L) = Rot.denote n r * RotLayer.denote n L

theorem RotProg.denote_append (n : Nat) (p q : RotProg) :
    RotProg.denote n (p ++ q) = RotProg.denote n q * RotProg.denote n p

theorem Rot.denote_mul_same_axis (n : Nat) (r s : Rot) (h : r.axis = s.axis) :
    Rot.denote n r * Rot.denote n s
      = rotOf (r.theta + s.theta) (axisMat n r.axis)

def Rot.inv (r : Rot) : Rot

theorem Rot.inv_theta (r : Rot) : r.inv.theta = -r.theta

theorem Rot.denote_mul_inv (n : Nat) (r : Rot) :
    Rot.denote n r * Rot.denote n r.inv = 1

theorem Rot.denote_pi (n : Nat) (r : Rot) (h : r.angle = .pi) :
    Rot.denote n r = -1

def bqMul : Pauli → Pauli → Pauli
  | .I, q => q
  | p, .I => p
  | .X, .X => .I
  | .Y, .Y => .I
  | .Z, .Z => .I
  | .X, .Y => .Z
  | .Y, .X => .Z
  | .Y, .Z => .X
  | .Z, .Y => .X
  | .Z, .X => .Y
  | .X, .Z => .Y

def bqPhase : Pauli → Pauli → ℕ
  | .X, .Y => 1
  | .Y, .Z => 1
  | .Z, .X => 1
  | .Y, .X => 3
  | .Z, .Y => 3
  | .X, .Z => 3
  | _, _ => 0

theorem pauli_mul_full (p q : Pauli) :
    p.toMatrix * q.toMatrix
      = (Complex.I ^ bqPhase p q) • (bqMul p q).toMatrix

private theorem map_sum_range_succ (h : Nat → ℕ) (n : Nat) :
    ((List.range (n + 1)).map h).sum
      = ((List.range n).map (fun i => h (i + 1))).sum + h 0

theorem opsMat_mul_full (n : Nat) (f g : Nat → Pauli) :
    opsMat n f * opsMat n g
      = (Complex.I ^ (((List.range n).map (fun i => bqPhase (f i) (g i))).sum))
          • opsMat n (fun i => bqMul (f i) (g i))

def phaseAt (Q : PauliProduct) (f : PFactor) : ℕ

def phaseF (P Q : PauliProduct) : ℕ

theorem phaseF_cons (f : PFactor) (P Q : PauliProduct) :
    phaseF (f :: P) Q = phaseAt Q f + phaseF P Q

theorem bqPhase_kind_lookup (k : PKind) (Q : PauliProduct) (i : Nat) :
    bqPhase (pkindToBQ k) (kindFn Q i) = phaseAt Q ⟨i, k⟩

private theorem sum_range_split (n a : Nat) (ha : a < n) (p q : Nat → ℕ)
    (heq : ∀ j, j ≠ a → q j = p j) (hpa : p a = 0) :
    ((List.range n).map q).sum = ((List.range n).map p).sum + q a

theorem phaseF_dense (n : Nat) (P Q : PauliProduct)
    (hs : sortedStrict P = true) (hw : PauliProduct.width P ≤ n) :
    ((List.range n).map (fun i => bqPhase (kindFn P i) (kindFn Q i))).sum
      = phaseF P Q

theorem bqMul_of_mulK_none {a b : PKind} (h : PKind.mulK a b = none) :
    bqMul (pkindToBQ a) (pkindToBQ b) = .I

theorem bqMul_of_mulK_some {a b k : PKind} (h : PKind.mulK a b = some k) :
    bqMul (pkindToBQ a) (pkindToBQ b) = pkindToBQ k

theorem kindFn_eq_I_of_not_lt {P : PauliProduct} {lo i : Nat}
    (hlb : lbound lo P = true) (hi : i < lo) : kindFn P i = .I

theorem kindFn_mulF (P Q : PauliProduct)
    (hsP : sortedStrict P = true) (hsQ : sortedStrict Q = true) (i : Nat) :
    kindFn (mulF P Q) i = bqMul (kindFn P i) (kindFn Q i)

theorem axisMat_mulF (n : Nat) (P Q : PauliProduct)
    (hsP : sortedStrict P = true) (hwP : PauliProduct.width P ≤ n)
    (hsQ : sortedStrict Q = true) :
    axisMat n P * axisMat n Q
      = (Complex.I ^ phaseF P Q) • axisMat n (mulF P Q)

theorem phaseAt_parity (Q : PauliProduct) (f : PFactor) :
    phaseAt Q f % 2 = (if overlapMismatch Q f then 1 else 0)

theorem phaseF_parity (P Q : PauliProduct) :
    phaseF P Q % 2 = acCount P Q % 2

theorem phaseF_even_of_commF {P Q : PauliProduct}
    (h : commF P Q = true) : phaseF P Q % 2 = 0

theorem phaseF_odd_of_not_commF {P Q : PauliProduct}
    (h : commF P Q = false) : phaseF P Q % 2 = 1

theorem I_pow_mod (k : Nat) : Complex.I ^ k = Complex.I ^ (k % 4)

inductive RAngle

def RAngle.eighths : RAngle → Nat
  | .pi => 8 | .piHalf => 4 | .piQuarter => 2 | .piEighth => 1

structure Rot

abbrev RotLayer

abbrev RotProg

def overlapMismatch (Q : PauliProduct) (f : PFactor) : Bool

def acCount (P Q : PauliProduct) : Nat

def commF (P Q : PauliProduct) : Bool

def Rot.wf (r : Rot) : Bool

def layerComm : RotLayer → Bool
  | []     => true
  | r :: t => t.all (fun s => commF r.axis s.axis) && layerComm t

def RotLayer.wf (L : RotLayer) : Bool

def RotProg.wf (p : RotProg) : Bool

def Rot.width (r : Rot) : Nat

def RotLayer.width : RotLayer → Nat
  | []     => 0
  | r :: t => max r.width (RotLayer.width t)

def RotProg.width : RotProg → Nat
  | []     => 0
  | L :: p => max L.width (RotProg.width p)

theorem layerComm_append (L M : RotLayer) :
    layerComm (L ++ M) = true ↔
      (layerComm L = true ∧ layerComm M = true ∧
        ∀ r ∈ L, ∀ s ∈ M, commF r.axis s.axis = true)

theorem RotProg.wf_append (p q : RotProg) :
    RotProg.wf (p ++ q) = (RotProg.wf p && RotProg.wf q)

theorem RotProg.width_append (p q : RotProg) :
    RotProg.width (p ++ q) = max (RotProg.width p) (RotProg.width q)

example : commF [⟨0, .x⟩, ⟨1, .x⟩] [⟨1, .z⟩, ⟨2, .z⟩] = false

example : commF [⟨0, .x⟩, ⟨1, .x⟩] [⟨0, .z⟩, ⟨1, .z⟩] = true

example : commF [⟨0, .x⟩] [⟨5, .z⟩] = true

example : commF [⟨0, .x⟩, ⟨3, .z⟩] [⟨0, .x⟩, ⟨3, .z⟩] = true

example : RotLayer.wf
    [⟨false, .piEighth, [⟨0, .z⟩]⟩, ⟨false, .piEighth, [⟨1, .z⟩]⟩] = true

example : RotLayer.wf
    [⟨false, .piQuarter, [⟨0, .x⟩, ⟨1, .x⟩]⟩,
     ⟨true,  .piQuarter, [⟨0, .z⟩, ⟨1, .z⟩]⟩] = true

example : RotLayer.wf
    [⟨false, .piEighth, [⟨0, .x⟩]⟩, ⟨false, .piEighth, [⟨0, .z⟩]⟩] = false

example : RotProg.width
    [[⟨false, .piEighth, [⟨0, .z⟩, ⟨4, .x⟩]⟩], [⟨true, .pi, [⟨2, .y⟩]⟩]] = 5