isSpatial
plain-language theorem explainer
This definition returns true for any spacetime index that is not the time coordinate. It would be referenced in typed calculations that separate temporal and spatial components within the manifold scaffold. The implementation is a direct Boolean negation of equality to zero on the four-element index set.
Claim. Let $I$ be the set of spacetime indices, identified with the finite set $I = {0,1,2,3}$ where index 0 denotes the time coordinate. For any $I$-valued index $μ$, the predicate isSpatial$(μ)$ holds precisely when $μ ≠ 0$.
background
The module supplies a minimal typed manifold structure for relativity geometry in the ILG setting. SpacetimeIndex is defined as the abbreviation Fin 4, with the explicit convention that index 0 is the time coordinate. The upstream delta definition supplies the Kronecker delta on Fin n, while the 'for' structure from UniversalForcingSelfReference records structural properties required for meta-realization. The module documentation states that these are structural placeholders only and are not part of the verified certificate chain.
proof idea
The declaration is a direct one-line definition that evaluates the Boolean expression $μ ≠ 0$ on the input index. No lemmas or tactics are invoked; the body is simply the negation of equality to the zero element of Fin 4.
why it matters
The predicate supports downstream manifold operations that must distinguish the time direction from the three spatial directions. It sits inside the scaffold module whose documentation explicitly warns against citing its contents as proven mathematics. No downstream theorems depend on it, consistent with the module's role as a non-certificate placeholder rather than a step in the T0-T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.