ImpossibleRegion
plain-language theorem explainer
The ImpossibleRegion is the set of non-positive reals marking the boundary where J-cost diverges to infinity. Modal geometry researchers would cite it when partitioning possibility spaces into finite-cost and unreachable configurations. The declaration is a direct set comprehension with no lemmas or reductions required.
Claim. The impossible region is the set $S = { x ∈ ℝ | x ≤ 0 }$, the complement to positive ratios where the J-cost $J(x) = (x + x^{-1})/2 - 1$ diverges as $x → 0^+$.
background
In the ModalGeometry module the J-cost of a recognition event is the value returned by the derived cost function on a multiplicative recognizer comparator. Upstream results define this cost explicitly as non-negative and tie it to the recognition state via the observer forcing construction. The module imports possibility and actualization to equip modal distances and balls with this cost structure.
proof idea
Direct definition via set comprehension on the reals. No lemmas or tactics are invoked; the body simply encodes the non-positive ray as the mathematical locus of infinite J-cost.
why it matters
The definition supplies the explicit complement to possibility balls and curvature statements in the same module. It closes the finite-cost sector consistent with the J-uniqueness step of the forcing chain, where divergence at the origin enforces the boundary of reachable states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.