module module high

`IndisputableMonolith.Modal.ModalGeometry`

ModalGeometry equips possibility space with a metric derived from the J-transition function. Researchers in modal quantum interpretations or configuration-space geometry cite it for distance calculations between states. The module supplies definitions for distance, balls, curvature, and period without embedded proofs.

claimThe modal distance is $d(x,y) = J_{transition}(x,y)/τ_0$, obeying $d(x,x)=0$, symmetry $d(x,y)=d(y,x)$, and the triangle inequality on the space of possibilities.

background

This module imports the foundational notions of possibility and actualization to define a metric geometry on configuration space. The J-transition function measures separation between possibilities, scaled by the base time τ₀. It introduces auxiliary objects such as possibility balls, curvature at the identity, and the modal Nyquist limit, all expressed in the Recognition Science setting of J-cost and self-similar scaling.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the metric primitives required by the parent Modal module. It fills the geometric layer of the modal framework, enabling statements about connectedness, curvature positivity, and period that appear in downstream modal dynamics.

scope and limits

Does not derive the J-transition from the base forcing chain.
Does not prove the triangle inequality.
Does not relate the metric to physical constants such as c or ħ.
Does not address completeness or geodesic completeness of the space.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Modal module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Modal.Actualization module_import
IndisputableMonolith.Modal.Possibility module_import

declarations in this module (28)

def modal_distance L51
lemma modal_distance_nonneg L55
lemma modal_distance_self L63
lemma modal_distance_symm L68
def PossibilityBall L78
lemma identity_in_ball L85
theorem possibility_space_connected L94
def possibility_curvature L114
lemma curvature_at_identity L118
lemma curvature_pos L123
def modal_period L131
def modal_nyquist_limit L139
def modally_equivalent L142
lemma modally_equivalent_refl L146
lemma modally_equivalent_symm L150
theorem modal_nyquist L164
def interference_amplitude L178
def constructive_interference L184
def destructive_interference L190
lemma constructive_at_zero L194
structure ModalManifold L216
def standard_modal_manifold L227
theorem modal_completeness L237
def ImpossibleRegion L249
theorem impossible_infinite_cost L252
def PossibilityBoundary L263
theorem boundary_unreachable L266
def modal_geometry_status L274