CausalRelation
plain-language theorem explainer
The CausalRelation inductive type enumerates five canonical causal relations between events in a five-dimensional configuration space. Physicists formalizing light-cone structure from Recognition Science foundations cite it to ground discrete causality before counting or certifying relations. The definition lists the five constructors and derives decidable equality plus finite cardinality in one step.
Claim. Let $C$ be the set of causal relations between two events in configuration space of dimension 5. Then $C$ consists of timelike separation, spacelike separation, lightlike (null) separation, past light-cone boundary, and future light-cone boundary, equipped with decidable equality and finite type structure.
background
The module derives light-cone causality directly from Recognition Science, where events inhabit a configuration space of dimension 5. Five relations are introduced to exhaust all possible causal connections: timelike, spacelike, lightlike, and the two boundary cases on the light cones. This enumeration supplies the discrete types needed for subsequent cardinality and certification results in the same module.
proof idea
The declaration is an inductive definition that introduces exactly five constructors. It then derives the instances DecidableEq, Repr, BEq, and Fintype automatically to enable equality tests and finite cardinality in downstream statements.
why it matters
This definition supplies the enumeration that feeds the theorem causalRelation_count proving cardinality exactly 5 and the structure LightConeCausalityCert. It anchors the light-cone causality module within the Recognition Science framework, where causal structure emerges from the forcing chain and J-uniqueness. No open questions or scaffolding are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.