Point
A point on manifold M of dimension d is a coordinate map from the finite index set of size d into the reals. Relativity and inevitability modules cite this type to label coordinate tuples in downstream geometry and choke-point arguments. The declaration is a direct one-line abbreviation of the standard coordinate representation.
claimFor a manifold $M$ with dimension $d$, a point on $M$ is a function from the finite set of $d$ indices to the reals.
background
Manifold is the structure carrying a single natural-number dimension field; the module supplies only this minimal typed placeholder for relativity geometry. The local setting is an explicit scaffold whose purpose is to let downstream code type-check without a full differential-geometry development. Upstream dimension values arrive from the spatial-dimension derivation (D) and active-edge count (A) in the integration-gap and lepton-generation modules.
proof idea
One-line definition that sets Point(M) equal to the function type Fin M.dim → ℝ.
why it matters in Recognition Science
The definition supplies the coordinate type used by consistency_defines_composition and the choke-point axioms in the inevitability structure. It occupies the placeholder slot for points inside the relativity geometry scaffold. The module lies outside the verified certificate chain and is not part of the T0–T8 forcing sequence.
scope and limits
- Does not supply a full atlas or transition maps.
- Does not prove smoothness or differentiability of coordinate functions.
- Does not link points to J-cost or the recognition composition law.
- Does not define tangent or cotangent spaces beyond the sibling declarations.
formal statement (Lean)
38def Point (M : Manifold) := Fin M.dim → ℝ
proof body
Definition body.
39
40/-- A vector at a point (tangent space). -/