VectorField
plain-language theorem explainer
VectorField aliases the (1,0)-tensor type on 4D spacetime, supplying a standard vector-field carrier for relativity geometry. Discrete Navier-Stokes and covariant-derivative code cite this alias when they need a relativity-compatible vector. The declaration is a direct one-line abbreviation of Tensor 1 0 with no further content.
Claim. A vector field on 4-dimensional spacetime is a map of type $(Fin 4 → ℝ) → (Fin 1 → Fin 4) → (Fin 0 → Fin 4) → ℝ$.
background
The module Relativity.Geometry.Tensor supplies basic tensor scaffolding for 4D spacetime. Its central definition is the abbrev Tensor (p q : ℕ) := (Fin 4 → ℝ) → (Fin p → Fin 4) → (Fin q → Fin 4) → ℝ, which specialises (p,q)-tensors to maps from a point (typed as Fin 4 → ℝ) to selected index tuples. VectorField is the direct special case p=1, q=0. The module header explicitly labels the entire file a scaffold outside the certificate chain. An upstream Navier-Stokes module defines a separate site-indexed VectorField (Fin siteCount → Axis → ℝ), showing the relativity version is meant for geometric rather than lattice use.
proof idea
The declaration is a one-line abbreviation that directly sets VectorField equal to Tensor 1 0, inheriting the tensor type without any additional lemmas or reductions.
why it matters
The alias is referenced by eight downstream declarations, principally advection, divergence, vectorLaplacian and the CoreNSOperator / IncompressibleNSOperator structures inside DiscreteNSOperator, plus covariant_deriv_vector in the Connection module. It therefore supplies the relativity tensor layer that those fluid operators can import when they need a 4D vector type. Because the module is marked scaffold, the declaration sits outside the main Recognition Science certificate chain and carries no direct link to the T0-T8 forcing steps or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.