necessary_is_one
plain-language theorem explainer
The theorem identifies the unique necessary configuration in Recognition Science as the real number 1. Modal logicians and philosophers of physics working in the RS framework cite it when grounding necessity in J-cost minimization. The proof splits the biconditional by applying the defect-zero characterization to the forward direction and substituting the identity into the defect-at-unity fact for the reverse.
Claim. For a real number $x$, $x$ is necessary if and only if $x=1$, where necessary means $x>0$ and the defect of $x$ vanishes.
background
In the Recognition Science framework, modal notions rest on the J-cost function. RSNecessary x holds precisely when $x>0$ and defect(x)=0, which encodes that x achieves the unique minimum of the cost. The module PH-013 resolves modal metaphysics by defining necessity as the unique J-minimizer, possibility as positive ratio, and actuality as the cost minimum at unity. Upstream results supply the supporting facts: defect vanishes at 1, and for positive arguments defect(x)=0 holds exactly when x=1. These lemmas derive from the explicit form of defect induced by the multiplicative recognizer.
proof idea
The proof splits the biconditional via constructor. The forward direction feeds the positivity and zero-defect hypotheses into the defect-zero characterization lemma. The reverse direction rewrites the assumption x=1, then invokes numerical normalization for positivity together with the dedicated lemma that defect equals zero at unity.
why it matters
This theorem supplies the concrete identification required by the PH-013 modal certificate, which asserts that necessity coincides with the unique J-minimizer at x=1, actuality equals necessity, and possibility covers all positive reals. It closes the first clause of the certificate and aligns with the J-uniqueness step in the forcing chain. The result is invoked directly in the downstream certificate theorem that completes the RS resolution of modal logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.