recognition / Physics / Physics.LightConeCausalityFromRS / causalRelation_count

theorem

`causalRelation_count`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.LightConeCausalityFromRS
domain: Physics
line: 24 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.LightConeCausalityFromRS on GitHub at line 24.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

Derivations using this theorem

Five Canonical Causal Relations · foundational / THEOREM
Two events relate in exactly five ways; the cone structure is finite

depends on

CausalRelation IndisputableMonolith.Physics.LightConeCausalityFromRS

used by

lightConeCausalityCert IndisputableMonolith.Physics.LightConeCausalityFromRS

formal source

  21  | futureBoundary
  22  deriving DecidableEq, Repr, BEq, Fintype
  23
  24theorem causalRelation_count : Fintype.card CausalRelation = 5 := by decide
  25
  26structure LightConeCausalityCert where
  27  five_relations : Fintype.card CausalRelation = 5
  28
  29def lightConeCausalityCert : LightConeCausalityCert where
  30  five_relations := causalRelation_count
  31
  32end IndisputableMonolith.Physics.LightConeCausalityFromRS

papers checked against this theorem

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