Jlog_eq_cosh_sub_one
plain-language theorem explainer
The lemma equates the Jlog cost function, defined via exponentials, to cosh(t) minus one for real t. Physicists deriving convexity and positivity properties in Recognition Science cost models cite it to simplify subsequent arguments. The proof is a direct term-mode reduction that unfolds the definition and substitutes the standard cosh identity.
Claim. For every real number $t$, $Jlog(t) = cosh(t) - 1$, where $Jlog(t) := ((exp(t) + exp(-t))/2) - 1$.
background
In the Cost.Jlog module, Jlog is defined directly as ((Real.exp t + Real.exp (-t))/2) - 1. This expression arises as the log-domain form of the J-cost, satisfying the Recognition Composition Law J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y). Upstream structures from LedgerFactorization calibrate J on the positive reals, while NucleosynthesisTiers place physical densities on discrete phi-tiers that rely on such cost identities.
proof idea
The term proof unfolds the definition of Jlog and rewrites the right-hand side via Real.cosh_eq, which states cosh t = (exp t + exp (-t))/2, then closes by reflexivity.
why it matters
This identity feeds Jlog_nonneg, Jlog_pos_iff, and Jlog_strictMonoOn_Ici0 in the same module, plus the strict-convexity theorem in Convexity. It realizes the T5 J-uniqueness landmark where J(x) = cosh(log x) - 1, supplying the tractable expression needed for order facts in cost-to-atomicity bridges and the eight-tick octave analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.