timeIndex
plain-language theorem explainer
This definition assigns index 0 as the time coordinate within the four-element spacetime index set. Coordinate-based relativity formalizations cite it to separate the temporal direction from the three spatial ones in manifold charts. The implementation is a direct constant assignment inside the Fin 4 type.
Claim. Let the spacetime indices be the set $I = {0,1,2,3}$. The time coordinate index is defined by $t := 0$.
background
The module supplies placeholder manifold structure for relativity geometry. SpacetimeIndex is the abbreviation Fin 4, serving as the type of coordinate indices for spacetime. The timeIndex definition selects the zeroth element to mark the time direction. These constructions are structural placeholders only and lie outside the verified certificate chain.
proof idea
The definition is a direct constant assignment of 0 inside the SpacetimeIndex type.
why it matters
This definition supplies a minimal label for the time direction in the relativity geometry scaffold. It feeds no downstream theorems and forms no part of the verified RS formalization. The module documentation explicitly marks the entire file as a placeholder that does not constitute rigorous differential geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.