lightConeCausalityCert
plain-language theorem explainer
lightConeCausalityCert supplies a concrete instance of the LightConeCausalityCert structure by assigning its five_relations field the value of the causalRelation_count theorem. Researchers modeling event separation in RS-derived spacetimes cite this when confirming exactly five canonical causal relations for configDim D = 5. The definition is a direct one-line wrapper that instantiates the structure using the decided cardinality result.
Claim. The light-cone causality certificate is the structure whose sole field satisfies five_relations : |CausalRelation| = 5, instantiated by the theorem that establishes this cardinality.
background
The module derives light-cone causality from Recognition Science by enumerating five canonical relations between events in configuration space of dimension D = 5: timelike separated, spacelike separated, lightlike (null) separated, past light cone boundary, and future light cone boundary. The upstream theorem causalRelation_count proves Fintype.card CausalRelation = 5 by direct decision. The structure LightConeCausalityCert packages this cardinality as its single field, with the module reporting zero axioms and zero sorries.
proof idea
The definition is a one-line wrapper that applies the causalRelation_count theorem to populate the five_relations field of the LightConeCausalityCert structure.
why it matters
This definition completes the certification of light-cone causality in the RS module by supplying an explicit instance of the required structure. It supports verification of causal structure derived from the Recognition Science forcing chain, particularly the emergence of light cones consistent with D = 3 spatial dimensions. No open questions are touched, as the module reports zero sorries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.