possible_has_finite_cost
plain-language theorem explainer
Every real x greater than zero has bounded defect under the J-functional. Researchers working on modal interpretations in Recognition Science cite this to confirm that positive-ratio configurations carry finite existence cost. The proof is a direct term that witnesses the bound by defect x itself, using non-negativity of defect together with order reflexivity.
Claim. If $x > 0$, then there exists $B$ such that $0 ≤ J(x)$ and $J(x) ≤ B$, where $J$ is the defect functional.
background
The module grounds modal logic in J-cost: necessity holds only at the unique minimizer x=1, possibility requires positive ratio together with finite J-cost, and impossibility follows from non-positive ratio or deviation from the minimum. RSPossible is defined as the predicate 0 < x. The defect functional equals J on positive arguments, and upstream defect_nonneg states that defect is non-negative for every positive argument.
proof idea
The proof is a one-line term construction. It supplies defect x as the witness B, applies defect_nonneg to the hypothesis 0 < x to obtain the lower bound, and invokes le_refl to obtain the upper bound defect x ≤ defect x.
why it matters
The result verifies the finite-cost clause in the definition of possibility, supporting the RS modal resolution that lists necessity_is_unique_minimizer, possibility_is_positive_ratio, and the complete rs_modal_resolution certificate. It aligns with the J-cost accessibility relation and the eight-tick octave structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.