TickPhase

formal source

  41  | plusI | minusI | plusX | minusX | plusY | minusY | plusZ | minusZ
  42  deriving DecidableEq, Repr, BEq, Fintype
  43
  44inductive TickPhase where
  45  | t0 | t1 | t2 | t3 | t4 | t5 | t6 | t7
  46  deriving DecidableEq, Repr, BEq, Fintype
  47
  48theorem dft_has_2cube : HasTwoCubeCount DFTMode := by
  49  unfold HasTwoCubeCount; decide
  50theorem q3_has_2cube : HasTwoCubeCount Q3Vertex := by
  51  unfold HasTwoCubeCount; decide
  52theorem pauli_has_2cube : HasTwoCubeCount PauliElement := by
  53  unfold HasTwoCubeCount; decide
  54theorem tick_has_2cube : HasTwoCubeCount TickPhase := by
  55  unfold HasTwoCubeCount; decide
  56
  57/-! ## Cross-domain theorems. -/
  58
  59/-- Any two 2³-cube domains have the same cardinality. -/
  60theorem two_cube_equicardinal
  61    {A B : Type} [Fintype A] [Fintype B]
  62    (hA : HasTwoCubeCount A) (hB : HasTwoCubeCount B) :
  63    Fintype.card A = Fintype.card B := by
  64  rw [hA, hB]
  65
  66/-- A 2³ cube squared: 64 = 2^6 (the six faces squared? No, 2^(2·3) — the
  67    product of two cube-8 structures). -/
  68theorem two_cube_pair_64
  69    {A B : Type} [Fintype A] [Fintype B]
  70    (hA : HasTwoCubeCount A) (hB : HasTwoCubeCount B) :
  71    Fintype.card (A × B) = 64 := by
  72  unfold HasTwoCubeCount at hA hB
  73  simp [Fintype.card_prod, hA, hB]
  74