spatialIndices
plain-language theorem explainer
Spatial indices are defined as the constant list [1, 2, 3] over the four coordinate labels of a spacetime manifold. Researchers building typed geometry layers in the Recognition Science relativity scaffolding would reference this list to separate spatial directions from the time coordinate. The definition is introduced by direct assignment with no lemmas or computation.
Claim. Let $I := Fin 4$ be the set of spacetime coordinate indices. The spatial indices are the list $[1, 2, 3]$.
background
The module supplies a minimal typed manifold structure as an explicit scaffold, not part of the verified certificate chain; downstream modules may use it for type-checking but the definitions carry no rigorous differential geometry content. SpacetimeIndex is the abbreviation Fin 4 serving as coordinate indices for spacetime, with the time coordinate singled out as index 0 in the sibling declaration. This local setting follows the module's stated purpose of providing placeholder manifold infrastructure while deferring verified RS formalization to the Verification and URCGenerators directories.
proof idea
The definition is introduced by direct assignment of the list containing the integers 1, 2, and 3.
why it matters
This definition supplies the spatial coordinate labels within the placeholder manifold structure for the relativity geometry infrastructure. It aligns with the framework landmark of D = 3 spatial dimensions but remains outside the verified certificate chain and has no downstream dependents in the current graph. The module documentation explicitly warns against citing these definitions as proven mathematics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.