modal_distance_nonneg
plain-language theorem explainer
The lemma establishes non-negativity of the modal distance between any pair of configurations. Researchers formalizing modal geometry or ontology structures cite it to confirm the distance behaves as a non-negative quantity. The proof is a direct term-mode reduction that unfolds the distance definition involving the J-transition cost and chains standard non-negativity lemmas for multiplication, division, absolute value, and the J function.
Claim. For any configurations $c_1$ and $c_2$, the modal distance $d(c_1,c_2)$ satisfies $0leq d(c_1,c_2)$, where $d$ is built from the J-cost evaluated at transition states scaled by sums of J-values at the configuration positions.
background
Configurations are structures carrying parameters such as upsilon-star and the four epsilon terms drawn from the ILG gravity model. The J-cost at a transition state is the value of the J function at the starred point, serving as a dimensionless activation energy. Modal distance is assembled from these J values, typically via an absolute difference multiplied by a sum of J-terms at the two positions and divided by a positive constant.
proof idea
The term proof unfolds the modal distance definition together with the J-transition expression. It then applies mul_nonneg to an absolute-value non-negativity instance, followed by div_nonneg whose numerator is the sum of two J_nonneg applications at the configuration positions and whose denominator is a manifestly positive numeral.
why it matters
The result supplies the non-negativity property required by the modal distance nonnegativity theorem in the modal ontology structure module. It forms a basic building block for treating modal distance as a precursor to a metric within the possibility-actualization framework, consistent with the non-negative character of J-costs throughout the recognition science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.