Point
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.