pith. machine review for the scientific record. sign in
def definition def or abbrev

standard_modal_manifold

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

formal statement (Lean)

 227def standard_modal_manifold : ModalManifold where
 228  points := {c : Config | 0 < c.value}

proof body

Definition body.

 229  dimension := 2
 230  metric := modal_distance
 231  curvature := possibility_curvature
 232
 233/-- **MODAL COMPLETENESS**: Every point can reach identity.
 234
 235    The modal manifold is "geodesically complete" in the sense that
 236    every configuration has a finite-cost path to the attractor. -/

depends on (18)

Lean names referenced from this declaration's body.