PossibilityBall
plain-language theorem explainer
PossibilityBall defines the closed ball of radius r around configuration c under modal distance. Modal geometry work in Recognition Science cites it to describe reachable sets in possibility space. The definition is a direct set comprehension from the modal distance predicate on Config.
Claim. The possibility ball of radius $r$ centered at configuration $c$ is the set $B_r(c) := { y ∈ Config | d_modal(c,y) ≤ r }$, where $d_modal$ is the modal distance function.
background
The ModalGeometry module constructs geometric objects on the space of configurations, importing from Possibility and Actualization. Config denotes the type of modal configurations. modal distance is the distance function on this space, drawing on the zero-cost identity event (ObserverForcing.identity) and the Identity property that comparison cost of x with itself is zero (LogicAsFunctionalEquation.Identity).
proof idea
One-line definition that constructs the set of configurations y satisfying modal distance c y ≤ r via set comprehension. No lemmas or tactics are invoked.
why it matters
This definition is the direct parent of the lemma identity_in_ball, which places the identity configuration inside sufficiently large balls. It supplies the basic geometric primitive for the modal domain, connecting to the zero-cost identity in the forcing chain and the possibility space structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.