pith. sign in
lemma

Jcost_reciprocal

proved
show as:
module
IndisputableMonolith.Cost
domain
Cost
line
645 · github
papers citing
1 paper (below)

plain-language theorem explainer

Jcost is symmetric under inversion for positive arguments: the cost of ratio x equals the cost of its reciprocal. Researchers deriving small-strain bounds or modeling reciprocal costs in recidivism calculations cite the symmetry to interchange ratio arguments. The proof is a one-line wrapper that applies the core Jcost_symm lemma directly to the positivity hypothesis.

Claim. Let $J(y) := (y + y^{-1})/2 - 1$. Then for every real $x > 0$, $J(x) = J(x^{-1})$.

background

In the Cost module Jcost is defined by the expression $(x + x^{-1})/2 - 1$, matching the J-uniqueness function from the T5 step of the forcing chain. The module builds on Mathlib and treats costs as quantities via the Cost abbrev imported from RSNative.Core. Related sibling results include Jcost_nonneg (via AM-GM) and Jcost_eq_sq (used in algebraic rewrites).

proof idea

The proof is a term-mode one-line wrapper. It applies the upstream lemma Jcost_symm to the hypothesis hx : 0 < x.

why it matters

This alias supplies a shorthand for J-cost reciprocity that feeds the small-strain bound lemma and the recidivismCost_reciprocal theorem. The latter invokes it to equate recidivismCost reoffense baseline with its argument-swapped version. In the Recognition framework the symmetry supports ratio calculations on the phi-ladder and satisfies a parallel-work compatibility requirement noted in the module.

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

papers checked against this theorem (showing 1 of 1)