tensor_product
plain-language theorem explainer
Tensor product is defined to return the zero tensor for any pair of (p,q)-tensors in four-dimensional spacetime. This definition appears in the scaffold module for tensor operations and serves as a temporary placeholder. The implementation directly maps all inputs to the zero function without computation.
Claim. The tensor product of a $(p_1,q_1)$-tensor $T_1$ and a $(p_2,q_2)$-tensor $T_2$ is the zero tensor of type $(p_1+p_2, q_1+q_2)$.
background
A Tensor of type (p, q) is an abbrev for maps from spacetime points (Fin 4 → ℝ) to multilinear forms on p contravariant indices and q covariant indices, each ranging over Fin 4. This module is explicitly marked as a scaffold, not part of the certificate chain. The only upstream reference is the Tensor type itself, which supplies the domain and codomain for the operation.
proof idea
The definition is a direct one-line assignment that ignores both input tensors and returns the constant zero function of the appropriate type.
why it matters
This definition supplies a placeholder tensor product within the relativity geometry scaffold. It connects to no downstream results. As part of the non-certificate module, it marks an area where full tensor algebra remains undeveloped in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.