necessary_is_one
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not extend necessity to non-real numbers.
- Does not characterize necessity for x ≤ 0.
- Does not address vector or multi-dimensional cost functions.
- Does not prove uniqueness of the minimizer without the defect characterization.
formal statement (Lean)
81theorem necessary_is_one (x : ℝ) : RSNecessary x ↔ x = 1 := by
proof body
Term-mode proof.
82 constructor
83 · intro ⟨hpos, hzero⟩; exact (defect_zero_iff_one hpos).mp hzero
84 · intro h; rw [h]; exact ⟨by norm_num, defect_at_one⟩
85
86/-! ## II. Possibility = Positive Ratio -/
87
88/-- **Theorem (Possibility is Positive Ratio)**:
89 Anything with positive ratio is possible in RS.
90 J-cost is finite for all x > 0, so all positive configurations can exist. -/