TangentVector
plain-language theorem explainer
TangentVector defines the tangent space on a manifold M as the set of real-valued maps indexed by the finite set of its dimension. This placeholder supports coordinate-based typing in the relativity geometry scaffold. The definition proceeds by direct abbreviation equating the type to coordinate vectors in R to the power of dim M.
Claim. Let $M$ be a manifold of dimension $n$. The tangent space is the vector space of maps $Fin(n) → ℝ$.
background
The module supplies a minimal typed manifold structure for differential geometry in the relativity infrastructure. Manifold is a structure with a single field dim of type ℕ. The local setting is explicitly a scaffold providing placeholders to enable downstream modules to type-check, rather than a rigorous formalization of smooth manifolds with charts.
proof idea
The definition is a direct abbreviation that sets TangentVector M to the type Fin M.dim → ℝ, representing coordinate vectors in the dimension of the manifold.
why it matters
This placeholder definition supports the relativity geometry infrastructure by providing a basic type for tangent vectors. It feeds no downstream theorems. As a scaffold, it does not participate in the verified certificate chain or the core Recognition Science results such as the forcing chain T0 to T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.