`HasTwoCubeCount`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.TwoCubeUniversality
domain: CrossDomain
line: 28 · 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 28.

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

  25namespace IndisputableMonolith.CrossDomain.TwoCubeUniversality
  26
  27/-- A type has 2³-structure iff |T| = 2^3 = 8. -/
  28def HasTwoCubeCount (T : Type) [Fintype T] : Prop := Fintype.card T = 2 ^ 3
  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

papers checked against this theorem

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