RSPossible
plain-language theorem explainer
RSPossible defines a real number x to be possible precisely when x exceeds zero. Modal metaphysicians and Recognition Science researchers cite it to ground possibility in positive ratio with finite J-cost. The declaration is a direct abbreviation of the strict positivity predicate.
Claim. A real number $x$ is possible if and only if $x > 0$.
background
The PH-013 module grounds modal logic in J-cost: necessity holds only for the unique minimizer at $x=1$, actuality coincides with that minimizer, and impossibility follows from non-positive ratio. Possibility is introduced as the complementary predicate covering all positive ratios, which carry finite J-cost by construction. Upstream definitions include RSNecessary as the conjunction of positivity and zero defect, and RSActual as the predicate that coincides with RSNecessary.
proof idea
This is a direct definition that equates RSPossible x with the predicate $0 < x$. No lemmas or tactics are invoked; the abbreviation supplies the base predicate used by all downstream modal statements.
why it matters
The definition supplies the positive-ratio side of the PH-013 modal certificate, which states that possibility equals positive ratio, necessity equals the unique J-minimizer, and actuality equals necessity. It feeds theorems such as ph013_modal_certificate, possibility_is_positive_ratio, and modal_distance_nonneg. The construction aligns with the Recognition Science forcing chain in which J-cost is finite exactly on the positive reals, consistent with the eight-tick octave and the ledger positivity constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.