SpacetimeIndex
SpacetimeIndex is the finite type of coordinate labels on four-dimensional spacetime, ranging over {0,1,2,3}. It is referenced in the relativity geometry scaffold to distinguish the time component from the three spatial ones. The declaration is a direct abbreviation to Fin 4 with no further reduction steps.
claimLet $I := Fin 4 = {0,1,2,3}$ be the set of coordinate indices on four-dimensional spacetime, with 0 reserved for the time coordinate.
background
This abbrev sits inside the scaffold module Relativity.Geometry.Manifold, which supplies minimal typed structures for manifold operations but is explicitly excluded from the verified certificate chain. The module documentation states that these definitions are structural placeholders only and should not be cited as proven mathematics. It depends on the upstream abbrev Time := ℝ from RSNativeUnits, which supplies the real line for coordinate values.
proof idea
One-line abbreviation that directly equates SpacetimeIndex to the standard finite type Fin 4.
why it matters in Recognition Science
The definition supplies the index type used by the sibling declarations timeIndex, spatialIndices and isSpatial inside the same scaffold file. It therefore enables the basic index predicates required by the relativity geometry infrastructure, while the module doc warns that the entire file lies outside the T0-T8 forcing chain and the verified RS certificate.
scope and limits
- Does not supply a rigorous differential geometry formalization.
- Does not participate in the verified certificate chain.
- Does not define any manifold charts, tangent spaces or metric tensors.
formal statement (Lean)
50abbrev SpacetimeIndex := Fin 4
proof body
Definition body.
51
52/-- Time coordinate (index 0). -/