s5_necessity_implies_actuality
plain-language theorem explainer
Necessity in Recognition Science means being the unique J-minimizer with defect zero at x=1, which by definition coincides with actuality. Modal logicians embedding S5 axioms into physical ontologies would cite this as the direct resolution of axiom T. The proof is a one-line term wrapper that applies the definitional identity between the two predicates.
Claim. For all real numbers $x$, if $x$ is necessary (i.e., $x>0$ and defect$(x)=0$), then $x$ is actual (i.e., it satisfies the same condition).
background
The module PH-013 grounds modal logic in J-cost minimization. Necessity is defined as the unique configuration achieving defect zero, which occurs only at the identity point x=1. Actuality is introduced by the same predicate, making the two notions identical by construction. The upstream Possibility definition supplies the positive-ratio condition that distinguishes possible from impossible states, while the J-minimizer uniqueness lemma supplies the defect-zero anchor.
proof idea
The proof is a one-line term wrapper that applies the definition of RSActual as identical to RSNecessary, discarding the antecedent variable.
why it matters
This declaration supplies the S5 axiom T (necessity implies actuality) inside the Recognition Science modal ontology. It feeds directly into the ph013_modal_certificate theorem that assembles the complete resolution of possibility, necessity, and actuality. The result closes the definitional loop from unique J-minimizer to the actual world within the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.