module module high

`IndisputableMonolith.Modal.ModalGeometry`

ModalGeometry defines the modal distance metric on possibility space as d(x,y) = J_transition(x,y)/τ₀. Researchers in modal aspects of Recognition Science cite it to quantify configuration separation. The module supplies the core definition plus supporting properties such as non-negativity, symmetry, and the triangle inequality.

claim$d(x,y) = J_{transition}(x,y)/τ_0$ is the modal distance between configurations, obeying $d(x,x)=0$, $d(x,y)=d(y,x)$, and the triangle inequality.

background

The module imports Possibility and Actualization to introduce metric structure on modal space. The central object is the possibility metric d(x,y) = J_transition(x,y)/τ₀ measuring separation via normalized transition cost. Sibling declarations establish PossibilityBall, curvature_at_identity, and modal_period derived from this distance.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the metric geometry required by the parent IndisputableMonolith.Modal module. It enables distance-based modal arguments inside the Recognition framework and feeds downstream modal theorems.

scope and limits

Does not define the explicit functional form of J_transition.
Does not prove metric completeness or geodesic existence.
Does not link the distance to the phi-ladder or T5-T8 forcing steps.
Does not address embeddings into higher-dimensional modal spaces.

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