zero_tensor
plain-language theorem explainer
zero_tensor supplies the additive identity for (p,q)-tensors over 4D spacetime. It would be referenced in any construction that initializes tensor fields or proves linearity and homogeneity properties. The definition is realized by a direct functional assignment that returns the scalar zero for every combination of spacetime point and index selectors.
Claim. The zero tensor of valence $(p,q)$ is the map $T: (x : (Fin 4 → ℝ)) → (α : Fin p → Fin 4) → (β : Fin q → Fin 4) → ℝ$ such that $T(x, α, β) = 0$ for all inputs.
background
The module Relativity.Geometry.Tensor is explicitly marked as a scaffold and lies outside the Recognition Science certificate chain. It introduces basic tensor types specialized to four-dimensional spacetime without participating in the main forcing chain or phi-ladder constructions.
proof idea
The definition is a direct one-line functional assignment. It constructs the tensor by returning the constant value 0 irrespective of the spacetime point or index arguments, without calling any lemmas.
why it matters
This definition supplies the zero element needed for the vector-space structure on tensors in the relativity geometry scaffold. The module carries no recorded downstream uses and does not connect to the core Recognition Science results such as the J-uniqueness theorem or the eight-tick octave. It remains available for any future tensor-based extensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.