causalRelation_count
plain-language theorem explainer
The declaration establishes that the type of causal relations between events has exactly five elements under the Recognition Science light-cone construction. Researchers formalizing discrete causality or light-cone structure in physics models would cite this cardinality when certifying completeness of the classification. The proof is a direct computation via the decide tactic on the derived Fintype instance.
Claim. The set of causal relations between two events has cardinality five, consisting of timelike separation, spacelike separation, lightlike separation, past light-cone boundary, and future light-cone boundary.
background
The module derives light-cone causality from Recognition Science and enumerates five canonical relations between events, with configDim D set to 5. The inductive definition lists timelike, spacelike, lightlike, past boundary, and future boundary cases, each equipped with DecidableEq and Fintype instances. This local setting supplies the finite enumeration used for the cardinality claim.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate Fintype.card directly on the inductive type and its five constructors.
why it matters
This supplies the five_relations component of the downstream lightConeCausalityCert definition. It confirms the Recognition Science framework produces precisely five causal relations for the light-cone structure, aligning with the module's claim of configDim D = 5. No open questions or scaffolding are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.