`HasCubeFaceCount`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.CubeFaceUniversality
domain: CrossDomain
line: 29 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.CubeFaceUniversality on GitHub at line 29.

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

  26namespace IndisputableMonolith.CrossDomain.CubeFaceUniversality
  27
  28/-- A type has cube-face count iff |T| = 6. -/
  29def HasCubeFaceCount (T : Type) [Fintype T] : Prop := Fintype.card T = 6
  30
  31inductive Quark where
  32  | up | down | strange | charm | bottom | top
  33  deriving DecidableEq, Repr, BEq, Fintype
  34
  35inductive Lepton where
  36  | electron | muon | tau | nuE | nuMu | nuTau
  37  deriving DecidableEq, Repr, BEq, Fintype
  38
  39inductive CorticalLayer where
  40  | l1 | l2 | l3 | l4 | l5 | l6
  41  deriving DecidableEq, Repr, BEq, Fintype
  42
  43inductive BraakStage where
  44  | b1 | b2 | b3 | b4 | b5 | b6
  45  deriving DecidableEq, Repr, BEq, Fintype
  46
  47inductive RoboticDOF where
  48  | x | y | z | rollAxis | pitchAxis | yawAxis
  49  deriving DecidableEq, Repr, BEq, Fintype
  50
  51theorem quark_has_6 : HasCubeFaceCount Quark := by
  52  unfold HasCubeFaceCount; decide
  53theorem lepton_has_6 : HasCubeFaceCount Lepton := by
  54  unfold HasCubeFaceCount; decide
  55theorem cortical_has_6 : HasCubeFaceCount CorticalLayer := by
  56  unfold HasCubeFaceCount; decide
  57theorem braak_has_6 : HasCubeFaceCount BraakStage := by
  58  unfold HasCubeFaceCount; decide
  59theorem robotic_has_6 : HasCubeFaceCount RoboticDOF := by

papers checked against this theorem

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