Jlog_eq_cosh_sub_one
plain-language theorem explainer
Equivalence between the logarithm-domain cost function and cosh(t) minus one holds for every real number t. Researchers deriving convexity bounds or the J-uniqueness result T5 cite this identity repeatedly. The argument reduces to a direct call on the algebraic unfolding lemma that precedes it.
Claim. For every real number $t$, $J(t) = e^{t} + e^{-t}$ over 2 minus 1 equals cosh(t) minus 1, where $J(x)$ denotes the cost function $(x + x^{-1})/2 - 1$.
background
The Cost.Convexity module proves that the logarithm-domain cost equals cosh(t) minus one and is strictly convex on the reals, while the original cost is strictly convex on the positive reals. These facts support the uniqueness theorem T5 in the forcing chain. The logarithm-domain version arises by composing the cost with the exponential map, so the standard hyperbolic identity transfers directly to the cost function.
proof idea
This is a one-line wrapper that invokes the algebraic identity lemma Jlog_as_cosh from the Cost module.
why it matters
The identity feeds the strict convexity theorem in the same module, which rewrites the logarithm-domain cost as cosh minus one and applies the known strict convexity of cosh. It also supports non-negativity and positivity lemmas in the Jlog submodule. In the Recognition Science framework this realizes the alternative expression for J given in T5, linking the algebraic form to the hyperbolic representation required for the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.