LightConeCausalityCert
plain-language theorem explainer
The LightConeCausalityCert structure records that exactly five causal relations exist between events when configDim equals five. Physicists deriving light-cone structure from Recognition Science would cite it to fix the enumeration of timelike, spacelike, lightlike, and boundary separations. It is realized as a bare structure definition whose single field states the Fintype cardinality of the CausalRelation inductive type.
Claim. Let $C$ be the set of causal relations between two events. The structure LightConeCausalityCert asserts that $|C|=5$, where the five elements are timelike separation, spacelike separation, lightlike separation, past light-cone boundary, and future light-cone boundary.
background
The module establishes light-cone causality directly from Recognition Science by enumerating five canonical relations between events when the configuration dimension is five. CausalRelation is the inductive type whose constructors are precisely timelike, spacelike, lightlike, pastBoundary, and futureBoundary, each carrying DecidableEq, Repr, BEq, and Fintype instances. This enumeration supplies the concrete content for the light-cone construction in the Recognition framework.
proof idea
The declaration is a structure definition containing one field. The field five_relations is typed as the equality Fintype.card CausalRelation = 5. No lemmas or tactics are invoked; the definition simply packages the cardinality statement supplied by the inductive type.
why it matters
This structure supplies the certificate instantiated by the downstream lightConeCausalityCert definition. It anchors the five-relation count that the module uses to derive light-cone causality from the Recognition Science forcing chain, matching the configDim D=5 stated in the module documentation. The result therefore closes the enumeration step before any further causal analysis proceeds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.