two_cube_powerset_256

formal source

  73  simp [Fintype.card_prod, hA, hB]
  74
  75/-- Power set of a 2³-cube has size 2^8 = 256. -/
  76theorem two_cube_powerset_256
  77    {A : Type} [Fintype A] [DecidableEq A] (hA : HasTwoCubeCount A) :
  78    Fintype.card (Finset A) = 256 := by
  79  rw [Fintype.card_finset, hA]; decide
  80
  81/-- DFT modes and Q₃ vertices are equinumerous. -/
  82theorem dft_q3_equicardinal :
  83    Fintype.card DFTMode = Fintype.card Q3Vertex :=
  84  two_cube_equicardinal dft_has_2cube q3_has_2cube
  85
  86/-- Pauli group and tick phases are equinumerous (both 8 = 2³). -/
  87theorem pauli_tick_equicardinal :
  88    Fintype.card PauliElement = Fintype.card TickPhase :=
  89  two_cube_equicardinal pauli_has_2cube tick_has_2cube
  90
  91/-- DFT-8 × Q₃ = 64 (product of two 2³-cubes). -/
  92theorem dft_q3_product :
  93    Fintype.card (DFTMode × Q3Vertex) = 64 :=
  94  two_cube_pair_64 dft_has_2cube q3_has_2cube
  95
  96/-- 64 = 8² and 64 = 2^6. Both identities. -/
  97theorem sixtyfour_identities : 64 = 8 * 8 ∧ 64 = 2^6 := by decide
  98
  99structure TwoCubeUniversalityCert where
 100  dft_is_2cube : HasTwoCubeCount DFTMode
 101  q3_is_2cube : HasTwoCubeCount Q3Vertex
 102  pauli_is_2cube : HasTwoCubeCount PauliElement
 103  tick_is_2cube : HasTwoCubeCount TickPhase
 104  all_equicardinal : ∀ (A B : Type) [Fintype A] [Fintype B],
 105    HasTwoCubeCount A → HasTwoCubeCount B →
 106    Fintype.card A = Fintype.card B