Covector
plain-language theorem explainer
Covector equips a manifold M with the type of coordinate covectors as maps from Fin M.dim to the reals. It would be referenced in coordinate-based relativity geometry setups inside the Recognition Science scaffold. The declaration is a direct type abbreviation with no computational content or proof obligations.
Claim. For a manifold $M$ of dimension $n$, a covector is a map from the finite set of $n$ indices to the reals.
background
The module supplies placeholder manifold structures for relativity geometry in the Recognition framework and is explicitly labeled a scaffold outside the verified certificate chain. The sibling Manifold structure consists only of a dimension field of type ℕ. Upstream, dim is supplied as D from TauStepDerivation, where D is the spatial dimension forced by the T8 step; Recognition.M and Cycle3.M supply the underlying recognition algebra that the manifold is intended to interface with.
proof idea
The declaration is a direct one-line abbreviation that identifies Covector M with the function type Fin M.dim → ℝ, providing a coordinate representation of covectors with no further lemmas or reductions.
why it matters
This definition populates the manifold scaffolding in Relativity.Geometry.Manifold, which the module documentation states lies outside the verified certificate chain and has no downstream uses. It prepares typed infrastructure for potential extensions to tangent and cotangent bundles while remaining unverified. The setup touches the open question of embedding full differential geometry into the Recognition Science forcing chain (T0-T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.