jcost_measurable
plain-language theorem explainer
J-cost satisfies non-negativity for every positive real. Researchers building measure spaces from Recognition Science foundations cite this to confirm the cost function integrates against the five canonical measures. The proof splits on whether the argument equals one, reducing directly to the zero value or to the strict positivity lemma.
Claim. For every real number $r > 0$, the J-cost function satisfies $J(r) = (r-1)^2/(2r) $ and therefore $J(r) 0$.
background
The J-cost function is expressed as the squared ratio $J(r) = (r-1)^2/(2r)$ for $r > 0$, obtained from the Recognition Composition Law and the uniqueness property of the J-function. The module MeasureTheoryFromRS embeds this cost into measure theory by constructing five canonical measures (Lebesgue, counting, Dirac, Hausdorff, Borel) whose number equals the configuration dimension, with non-negativity of J-cost required for compatibility with integration and probability.
proof idea
The tactic proof opens with by_cases on equality to 1. When equality holds it rewrites with the Jcost_unit0 lemma to obtain zero. When inequality holds it applies the Jcost_pos_of_ne_one lemma to obtain a strict lower bound and finishes with le_of_lt.
why it matters
The theorem supplies the jcost_nonneg field inside the measureTheoryCert definition that certifies the full measure-theoretic structure derived from RS. It directly supports the module claim that J-cost is a measure-compatible object among the five canonical measures. Within the framework this non-negativity is a prerequisite for using J-cost in integration, consistent with the J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.