actuality_is_unique
plain-language theorem explainer
The theorem establishes that exactly one real number satisfies the RSActual predicate in the Recognition Science modal framework. Modal metaphysicians and physicists grounding possibility in J-cost minimization would cite this to fix the actual world as unique. The proof is a direct term application of the necessity_is_unique_minimizer lemma.
Claim. There exists a unique real number $x$ such that $x$ is actual, where actuality holds precisely when $x$ is necessary (i.e., the unique J-cost minimizer at $x=1$).
background
The module resolves modal metaphysics via J-cost: necessity means unique J-minimizer (only $x=1$ achieves defect zero), possibility means positive ratio with finite J-cost, and impossibility means non-positive ratio or defect zero at $x≠1$. Actuality is defined as RSNecessary, which the referenced sibling equates to the identity configuration $x=1$. The local setting is PH-013, which lists this uniqueness as one of six key theorems completing the RS modal certificate alongside necessity_is_unique_minimizer and rs_modal_resolution.
proof idea
The proof is a one-line term wrapper that applies necessity_is_unique_minimizer directly to discharge the unique-existence goal for RSActual.
why it matters
This declaration closes the modal chain by confirming the actual world is the unique J-minimizer, feeding the downstream rs_modal_resolution and s5_actuality_implies_possibility results listed in the module. It instantiates the Recognition Science resolution that actualization selects the identity configuration, consistent with T5 J-uniqueness and the forcing chain's self-similar fixed point at phi. No open scaffolding remains here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.