IndisputableMonolith.Relativity.Geometry.Manifold
The Manifold module defines a smooth manifold equipped with dimension and a coordinate system. It is imported by the Geometry aggregator for use in relativity constructions within Recognition Science. This is a definition module with no proofs.
claimA smooth manifold $M$ of dimension $n$ equipped with a coordinate system.
background
The module introduces the core objects for differential geometry in the relativity section. It defines Manifold as a smooth manifold with dimension and coordinate system, together with Point, TangentVector, Covector, Spacetime, SpacetimeIndex, and related index and Kronecker structures. The setting is the geometry layer of spacetime models, imported solely from Mathlib.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module is re-exported by the Geometry Module Aggregator, which collects all geometry components for convenient importing. It supplies the manifold foundation required by downstream relativity geometry in the Recognition Science framework.
scope and limits
- Does not contain any theorem proofs or sorry placeholders.
- Does not import Recognition Science modules beyond Mathlib.
- Does not define metric tensors or curvature operators.
- Does not address forcing chain steps or phi-ladder mass formulas.