modal_distance_nonneg
plain-language theorem explainer
Non-negativity of modal distance holds for every positive real configuration in the Recognition Science modal ontology. Modal metaphysicians and RS framework developers cite the result when verifying that cost measures remain well-behaved on the accessibility relation. The argument is a one-line wrapper that invokes the defect non-negativity lemma once the positivity hypothesis is supplied.
Claim. For every real number $x > 0$, one has $0 ≤ modalDistance(x)$.
background
In the Recognition Science treatment of modal logic (PH-013), possibility is identified with positive ratio: RSPossible x holds precisely when $x > 0$. Modal distance is the cost measure attached to a configuration and is defined in terms of the defect function that quantifies deviation from the J-minimizer at $x = 1$. The module grounds necessity in unique J-minimization, possibility in positive finite J-cost, and impossibility in non-positive ratio or zero defect at $x ≠ 1$ (see MODULE_DOC). Upstream, defect_nonneg states that defect is non-negative for positive arguments, with the explicit identity defect x = ((x-1)^2 / x)/2.
proof idea
The proof is a one-line wrapper that applies the defect_nonneg theorem directly to the hypothesis hx : RSPossible x, which supplies the required positivity condition 0 < x.
why it matters
The result feeds the modal_distance_nonneg lemma in ModalGeometry and thereby supports the accessibility relation used throughout the RS modal framework. It supplies the non-negativity step required by the PH-013 resolution of modal metaphysics, ensuring J-cost measures are ordered for all possible worlds. The theorem connects directly to the J-cost minimization that defines necessity and actuality in the eight-tick octave setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.