CovectorField
plain-language theorem explainer
CovectorField abbreviates the (0,1) case of the general tensor type over 4D spacetime. A relativist would cite the abbreviation when introducing covector fields for 1-forms or metric duals. The declaration is a direct one-line abbreviation of the Tensor constructor with no further reduction.
Claim. Let $CovectorField$ denote the type of maps from points in 4-dimensional spacetime to covectors, obtained by specializing the general tensor abbreviation to zero contravariant indices and one covariant index.
background
The Tensor module, marked as a scaffold outside the certificate chain, defines a general (p,q)-tensor as a function from spacetime points (Fin 4 to reals) to multilinear maps with p upper and q lower index slots. CovectorField specializes this to p=0 and q=1. This supplies the basic geometric object for covectors in 4D spacetime. The upstream Tensor definition supplies the functional signature used here.
proof idea
This is a direct abbreviation: CovectorField is defined exactly as Tensor applied to 0 and 1. No lemmas or tactics are applied.
why it matters
The abbreviation supplies the input type for the covariant derivative of covectors in the Connection module. That downstream definition returns the zero field as a placeholder. It prepares geometric infrastructure for the relativity layer but remains outside the certified chain and does not connect to the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.