ContravariantBilinear
plain-language theorem explainer
ContravariantBilinear supplies the type of (2,0)-tensors on 4D spacetime by direct abbreviation over the general Tensor constructor. Researchers constructing inverse metrics or 1PN expansions cite it when they need a contravariant bilinear object. The definition is a one-line abbreviation that fixes two contravariant indices and zero covariant indices.
Claim. A contravariant bilinear tensor on 4-dimensional spacetime is the map type given by a point in coordinates together with two contravariant index slots: $T : (Fin 4 → ℝ) → ((Fin 2 → Fin 4) → (Fin 0 → Fin 4) → ℝ)$.
background
The module Relativity.Geometry.Tensor defines basic tensor infrastructure for 4D spacetime. Its central sibling definition states that Tensor (p q : ℕ) is the function type (Fin 4 → ℝ) → (Fin p → Fin 4) → (Fin q → Fin 4) → ℝ, representing a (p,q)-tensor with the first argument a spacetime point and the remaining arguments selecting the index slots.
proof idea
One-line abbreviation that instantiates Tensor with p=2 and q=0.
why it matters
The abbreviation supplies the target type for inverse_metric, which returns a ContravariantBilinear from a MetricTensor, and for inverse_metric_1PN, which builds the 1PN inverse metric components. It therefore supports the geometric layer required for relativistic calculations inside the Recognition Science scaffolding, even though the module itself lies outside the main forcing-chain certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.