RSActual
plain-language theorem explainer
RSActual equates actuality with necessity in Recognition Science, so that only the unique zero-defect configuration counts as actual. Modal metaphysicians and foundations-of-physics researchers cite it when reducing modal categories to J-cost minimization. The declaration is a direct one-line alias to the RSNecessary predicate.
Claim. A real number $x$ is actual if and only if $0 < x$ and the defect of $x$ is zero.
background
The module PH-013 grounds modal logic in the J-cost function on the real line. Necessity is defined as the conjunction of positive ratio and zero defect; impossibility is defined as non-positive ratio. Actuality is introduced by direct identification with the necessity predicate, making the actual world coincide with the unique J-minimizer at unity.
proof idea
This is a one-line definition that aliases RSActual directly to RSNecessary.
why it matters
RSActual supplies the predicate used in the PH-013 modal certificate and in theorems such as actuality_is_j_minimum and actuality_is_unique. It identifies the actual world with the necessary configuration x=1, consistent with T5 J-uniqueness and the reduction of modal notions to cost minimization. Downstream results derive S5-style implications from this identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.