necessity_is_unique_minimizer
plain-language theorem explainer
Necessity in Recognition Science is the unique real with zero defect under the J-cost function. The theorem shows exactly one such number exists, namely x=1. It is cited in the PH-013 modal certificate and the actuality uniqueness result. The proof exhibits the witness 1 and invokes the defect-zero characterization lemma for uniqueness.
Claim. There exists a unique real number $x$ such that $x>0$ and the defect of $x$ is zero, where defect measures deviation from unity via the J-cost function.
background
The ModalOntologyStructure module grounds modal notions in the J-cost function imported from LawOfExistence. RSNecessary x is defined as the conjunction of positivity and zero defect. Upstream results establish the concrete facts: defect_at_one proves defect 1 equals zero, while defect_zero_iff_one states that for any positive real the defect vanishes if and only if the argument equals one.
proof idea
The term-mode proof applies the use tactic to exhibit 1 as witness. It then constructs the existence half by pairing a norm_num positivity proof with defect_at_one, and the uniqueness half by introducing an arbitrary y satisfying the RSNecessary conditions and discharging via the forward direction of defect_zero_iff_one.
why it matters
This theorem supplies the first clause of the PH-013 modal certificate, identifying necessity with the unique J-minimizer. It is invoked directly by actuality_is_unique to equate actuality with the same minimizer and by the full ph013_modal_certificate that resolves modal metaphysics. Within the Recognition framework it instantiates the J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.