Pith. sign in
lemma

Jcost_pos_of_ne_one

proved
show as:
module
IndisputableMonolith.Cost
domain
Cost
line
238 · github
papers citing
45 papers (below)

plain-language theorem explainer

The lemma proves that the J-cost function is strictly positive for every positive real not equal to one. Researchers modeling speech intelligibility, chemical thresholds, and climate predictability cite it to guarantee positive penalties away from the symmetric scale. The proof rewrites the cost via its squared algebraic form and applies standard positivity of squares and positive denominators.

Claim. For every real number $x > 0$ with $x ≠ 1$, the J-cost satisfies $J(x) > 0$, where $J(x) = (x + x^{-1})/2 - 1$.

background

The J-cost is defined by Jcost(x) := (x + x^{-1})/2 - 1. This is the unique function satisfying the Recognition Composition Law that vanishes at the fixed point x = 1. An equivalent form J(x) = (x-1)^2/(2x) for x ≠ 0 is obtained by field simplification and ring algebra, as recorded in the sibling lemma Jcost_eq_sq.

proof idea

The proof first obtains x ≠ 0 from the positivity hypothesis. It rewrites via the upstream lemma Jcost_eq_sq, then applies div_pos. The numerator is positive by sub_ne_zero followed by sq_pos_of_ne_zero; the denominator is positive by mul_pos of 2 and x.

why it matters

This lemma is invoked in more than forty downstream results, including srCost_pos_off_threshold for speech, aestheticCost_pos_off_optimum for cultural aesthetics, and oxidative_stress for reactive oxygen species. It supplies the strict positivity half of J-uniqueness (T5) and thereby supports the forcing chain from the Recognition Composition Law through the eight-tick octave to D = 3. It closes the zero-at-unity property required by the phi-ladder mass formula.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 30 of 45)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.