module module high

`IndisputableMonolith.Modal.ModalGeometry`

The ModalGeometry module defines a metric on possibility configurations via the J-transition cost scaled by a base time. Researchers in modal quantum foundations or possibility-space geometry would cite it when measuring distances between states. The module supplies the core distance definition together with its listed algebraic properties.

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

background

The module sits inside the Modal domain and imports the foundational notions of possibility configurations and actualization from its two sibling modules. Its central object is the possibility metric, expressed directly as the J-transition cost normalized by the reference time τ₀. The supplied documentation states the three metric axioms that follow from this definition.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the metric structure required by the parent IndisputableMonolith.Modal module. It thereby supplies the geometric layer that later modal constructions (distance, balls, curvature) rest upon.

scope and limits

Does not derive or axiomatize the J_transition function itself.
Does not prove the triangle inequality or other metric axioms.
Does not relate the metric to the phi-ladder or Recognition Science constants.
Does not address physical interpretation or measurement of τ₀.

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