module module

`IndisputableMonolith.Modal.ModalGeometry`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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