BilinearForm
plain-language theorem explainer
BilinearForm aliases the (0,2)-tensor type over four-dimensional spacetime. Relativity geometry and Hamiltonian modules cite it when constructing the metric, Ricci tensor, Einstein tensor, and stress-energy tensor from the recognition field. The declaration is a direct type abbreviation with no further computation.
Claim. A bilinear form on spacetime is the type of rank-(0,2) tensors, i.e., maps from a point in $R^4$ to a function selecting two covariant indices in Fin 4 and returning a real value.
background
Tensor specializes (p,q)-tensors to 4D spacetime as maps from a point in R^4 to selections of p contravariant and q covariant indices. The module is explicitly marked a scaffold outside the certificate chain. The upstream Hamiltonian bilinear form supplies a related placeholder interface taking a point, another point, and a two-index map.
proof idea
The declaration is a one-line abbreviation that instantiates Tensor with p=0 and q=2.
why it matters
The type is referenced by eta, ricci_tensor, einstein_tensor, covariant_deriv_bilinear, and StressEnergyTensor. It supplies the common interface for bilinear objects in the relativity geometry layer, which sits above the recognition forcing chain and feeds curvature definitions. Scaffold status leaves open full integration with the main certificate chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.