RSNecessary
plain-language theorem explainer
The definition states that a real number x counts as necessary exactly when it is positive and achieves zero defect under the J-functional. Modal logicians working inside Recognition Science cite this predicate to ground necessity in unique cost minimization. It is introduced as a direct abbreviation that pairs the positivity condition with the zero-defect clause supplied by the Law of Existence.
Claim. A real number $x$ is necessary if and only if $x > 0$ and its defect vanishes, i.e., $J(x) = 0$.
background
Defect is defined in LawOfExistence as defect(x) := J(x) for positive x, where J is the recognition cost J(x) = (x + x^{-1})/2 - 1. The ModalOntologyStructure module grounds modal notions in this cost: necessity requires the configuration to reach the absolute minimum cost of zero, while possibility requires only positive ratio and actuality is identified with the necessary case.
proof idea
This is a definition that directly encodes the condition as the conjunction of positivity and zero defect. No lemmas or tactics are invoked; the predicate is supplied ready for use in downstream results such as necessity_is_unique_minimizer.
why it matters
The definition supplies the base predicate for the entire RS modal system. It is invoked by necessity_is_unique_minimizer to prove that exactly one necessary configuration exists, by necessary_is_one to identify it with x = 1, and by ph013_modal_certificate to resolve the nature of possibility and necessity. It realizes the J-uniqueness step of the forcing chain by tying necessity to the unique zero of the defect functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.