s5_possible_accessible_to_necessary
plain-language theorem explainer
Any positive real x admits a J-cost decreasing path to the unique necessary configuration y=1. Modal metaphysicians working in Recognition Science cite this as the accessibility direction of the S5 axiom B analog. The proof is a direct term construction that exhibits the witness 1 and invokes the zero-defect fact at unity.
Claim. For every real number $x > 0$, there exists a real number $y$ such that $y$ is necessary (i.e., $y > 0$ and defect$(y) = 0$) and $(y = 1$ implies defect$(y) = 0)$.
background
Modal ontology in Recognition Science grounds necessity as the unique J-minimizer, which occurs only at $x=1$ where defect vanishes. Possibility is identified with positive ratio ($x>0$), which guarantees finite J-cost. The accessibility relation holds precisely when a J-cost decreasing path exists; the module shows the minimum at unity is reachable from any positive starting point. Upstream, defect is the J functional on positive reals, and defect_at_one states defect(1)=0 by direct simplification.
proof idea
The proof is a one-line term-mode construction. It supplies the witness y=1, verifies necessity via norm_num for positivity together with the defect_at_one lemma for zero defect, and confirms the implication by the same zero-defect fact.
why it matters
This theorem supplies the accessibility half of the S5 modal axioms in the Recognition Science framework. It feeds the complete modal resolution rs_modal_resolution listed in the module. The result shows that J-cost minimization renders the necessary configuration accessible from every possible state, grounding the ontology in the forcing chain where the unique minimizer at unity is reached via cost reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.