  29
  30/-! ## Canonical 2³ domains. -/
  31
  32inductive DFTMode where
  33  | m0 | m1 | m2 | m3 | m4 | m5 | m6 | m7
  34  deriving DecidableEq, Repr, BEq, Fintype
  35
  36inductive Q3Vertex where
  37  | v000 | v001 | v010 | v011 | v100 | v101 | v110 | v111
  38  deriving DecidableEq, Repr, BEq, Fintype
  39
  40inductive PauliElement where
  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) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.