ModalManifold
plain-language theorem explainer
ModalManifold defines the geometric arena for possibility spaces as the set of configurations equipped with modal distance as metric and possibility curvature as curvature, defaulting to dimension 2. Modal theorists and Recognition Science modelers cite it when constructing actualization maps or possibility balls. The declaration is a direct structure definition that assembles its four fields from sibling functions in the same module.
Claim. A modal manifold consists of a subset of points $P$ from the configuration space, a dimension $d := 2$, a metric function given by the modal distance, and a curvature function given by the possibility curvature.
background
Config is the configuration type imported from the ILG gravity model. The module ModalGeometry sits atop Possibility and Actualization, where modal_distance and possibility_curvature are defined as sibling functions. Dimension is the natural-number field defaulting to 2, matching the doc-comment description of one value coordinate plus one time coordinate. Upstream structures such as Dimension from Constants.Dimensions and the of-structure from PhiForcingDerived supply the J-cost and dimensional signatures used to calibrate the metric and curvature.
proof idea
Direct structure definition. The four fields are assigned explicitly: points as Set Config, dimension as the literal 2, metric as the modal_distance function, and curvature as the possibility_curvature function.
why it matters
standard_modal_manifold instantiates this structure to supply the concrete object used in all downstream modal geometry lemmas. The definition realizes the geometric layer of Recognition Science in which points represent possible configurations and curvature encodes possibility density, consistent with the eight-tick octave and the boundary condition J → ∞. It closes the interface between the modal layer and the phi-ladder structures imported from SpectralEmergence and DimensionForcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.