TwoCubeUniversalityCert

formal source

  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
 107  pair_64 : Fintype.card (DFTMode × Q3Vertex) = 64
 108  sixtyfour_identities : 64 = 8 * 8 ∧ 64 = 2^6
 109
 110def twoCubeUniversalityCert : TwoCubeUniversalityCert where
 111  dft_is_2cube := dft_has_2cube
 112  q3_is_2cube := q3_has_2cube
 113  pauli_is_2cube := pauli_has_2cube
 114  tick_is_2cube := tick_has_2cube
 115  all_equicardinal := fun _ _ _ _ => two_cube_equicardinal
 116  pair_64 := dft_q3_product
 117  sixtyfour_identities := sixtyfour_identities
 118
 119end IndisputableMonolith.CrossDomain.TwoCubeUniversality