pith. sign in
module module high

IndisputableMonolith.Modal.ModalGeometry

show as:
view Lean formalization →

The ModalGeometry module defines the modal distance on possibility configurations as d(x,y) = J_transition(x,y)/τ₀. Modal researchers cite it when equipping possibility space with a metric for transition costs. The module assembles this definition plus its immediate metric axioms from the imported Possibility and Actualization modules.

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

background

This module belongs to the Modal domain and imports Possibility together with Actualization. It introduces the possibility metric that quantifies separation between configurations via the normalized J-transition cost. The DOC_COMMENT states the explicit formula and lists the three metric axioms that follow from the upstream modules.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the metric geometry required by the parent IndisputableMonolith.Modal module. It thereby enables the sibling declarations for balls, curvature, and modal period that appear in the same file.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (28)