SpacetimeIndex
plain-language theorem explainer
SpacetimeIndex abbreviates the finite set with four elements to label coordinate directions on a spacetime manifold. Sibling definitions in the same module rely on it to separate the time slot from the three spatial slots. The abbreviation is a direct type alias with no computation or lemmas.
Claim. The spacetime coordinate indices are the elements of the finite set $Fin 4 = {0,1,2,3}$.
background
The declaration lives inside a scaffold module whose module documentation states it supplies only a minimal typed manifold structure and is not part of the verified certificate chain. The module imports Mathlib and depends on the upstream abbreviation Time := ℝ from RSNativeUnits. Coordinate indices label the directions in which tangent vectors and covectors are expressed.
proof idea
Direct abbreviation to Fin 4.
why it matters
It supplies the index type consumed by the sibling definitions timeIndex, spatialIndices and isSpatial. These definitions in turn support the placeholder manifold infrastructure for the relativity layer. The module documentation explicitly warns that such definitions are structural placeholders and should not be cited as proven mathematics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.