PossibilityBall
plain-language theorem explainer
The possibility ball definition supplies the closed ball of radius r around a configuration c measured by modal distance. Modal geometry researchers cite this when analyzing reachable configurations in possibility space. The definition is realized as a direct set comprehension over the modal distance predicate.
Claim. Let $B_r(c)$ denote the possibility ball of radius $r$ centered at configuration $c$. Then $B_r(c) = { y : Config | d_{modal}(c, y) ≤ r }$, where $d_{modal}$ is the modal distance function.
background
The ModalGeometry module operates in the modal domain, importing from Possibility and Actualization to equip the space of configurations with geometric structure. Modal distance serves as the metric on this space, with nonnegativity, self-distance zero, and symmetry established in sibling declarations. Upstream, the Identity definition from LogicAsFunctionalEquation encodes that comparing a state to itself costs zero, while the identity event from ObserverForcing sits at the J-cost minimum with state equal to 1.
proof idea
This is a definition by direct set comprehension: the set of all y in Config such that modal_distance c y ≤ r. No lemmas are applied.
why it matters
The possibility ball definition underpins the identity_in_ball lemma, which shows that the identity configuration belongs to any ball whose radius exceeds the modal distance to identity. It supplies the basic reachability object in modal geometry, supporting analysis of possibility spaces that connect to the forcing chain steps T5 through T8 and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.