ModalManifold
ModalManifold equips the set of configurations with a two-dimensional geometric structure whose metric is the modal distance and whose curvature is the possibility curvature. Researchers modeling possibility spaces or modal interpretations in quantum foundations would cite this structure when tracking directions of possible change on the phi-ladder. The definition is a direct field assembly that pulls the metric and curvature functions from sibling declarations without additional lemmas.
claimA modal manifold consists of a set of points drawn from the space of configurations, a dimension fixed at 2, a metric function given by the modal distance, and a curvature function given by the possibility curvature.
background
The ModalGeometry module imports Possibility and Actualization to supply the underlying Config type and the modal_distance and possibility_curvature functions. Upstream, the Dimension structure records length, time, and mass exponents while the of structure from NucleosynthesisTiers places physical quantities on discrete phi-tiers; the of structure from PhiForcingDerived supplies the J-cost whose uniqueness is stated in T5. The local setting treats the manifold as the space of all possibilities whose tangent space at each point encodes directions of possible change, with boundary condition J to infinity as the configuration value approaches zero from above.
proof idea
The declaration is a pure structure definition that directly assigns the points field to a Set of Config, defaults the dimension field to 2, and binds the metric field to modal_distance and the curvature field to possibility_curvature. No tactics or upstream lemmas are invoked; the construction is a one-line field assembly.
why it matters in Recognition Science
ModalManifold supplies the geometric carrier for the modal layer and is instantiated by the downstream standard_modal_manifold definition. It realizes the T5 J-uniqueness and T7 eight-tick octave by embedding the phi-ladder into a two-dimensional space whose curvature is possibility_curvature, thereby closing the link from possibility to actualization and spectral emergence. The structure therefore occupies the position between the forcing chain (T0-T8) and concrete modal constructions.
scope and limits
- Does not compute explicit numerical values or closed forms for modal_distance or possibility_curvature.
- Does not establish metric axioms such as non-negativity or the triangle inequality.
- Does not extend the manifold to higher dimensions or incorporate explicit time evolution.
- Does not address boundary behavior beyond the stated J to infinity condition.
Lean usage
def standard : ModalManifold := standard_modal_manifoldformal statement (Lean)
216structure ModalManifold where
217 /-- Points of the manifold -/
218 points : Set Config
219 /-- Dimension (value + time) -/
220 dimension : ℕ := 2
proof body
Definition body.
221 /-- The metric structure -/
222 metric : Config → Config → ℝ := modal_distance
223 /-- The curvature function -/
224 curvature : Config → ℝ := possibility_curvature
225
226/-- The standard modal manifold. -/