`tick_has_2cube`

proved

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.TwoCubeUniversality
domain: CrossDomain
line: 54 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.TwoCubeUniversality on GitHub at line 54.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  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

papers checked against this theorem

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