zero_tensor
The zero_tensor definition supplies the additive identity for (p,q)-tensors on four-dimensional spacetime. Any tensor-algebra construction needing a neutral element under addition would reference this object. It is realized directly as the constant function that returns zero for every point and every index tuple.
claimThe zero tensor of valence (p,q) is the map sending every x in R^4, every p-tuple of indices, and every q-tuple of indices to the real number 0.
background
Tensor is the abbreviation for a (p,q)-tensor field on R^4, given explicitly as the function type (Fin 4 → R) → (Fin p → Fin 4) → (Fin q → Fin 4) → R. The present module is labeled a scaffold and is excluded from the Recognition Science certificate chain.
proof idea
One-line definition that applies the constant-zero function to all three arguments.
why it matters in Recognition Science
As a scaffold definition outside the certificate chain, zero_tensor supplies a basic neutral element for tensor operations but feeds no downstream theorems and does not touch the forcing chain, RCL, or phi-ladder constructions.
scope and limits
- Does not equip the tensor with any metric or connection.
- Does not impose symmetry, antisymmetry, or contraction rules.
- Does not reference J-cost, defectDist, or the phi-ladder.
formal statement (Lean)
40def zero_tensor {p q : ℕ} : Tensor p q := fun _ _ _ => 0
proof body
Definition body.
41
42end Geometry
43end Relativity
44end IndisputableMonolith