Jlog_as_exp
plain-language theorem explainer
Equivalence of the logarithmic cost function to its exponential representation holds for every real argument. Analysts working with cost functions in the Recognition Science framework cite this identity when reducing expressions to hyperbolic form ahead of the J-uniqueness step. The proof is immediate reflexivity matching the module definition.
Claim. $J(t) = (e^t + e^{-t})/2 - 1$ for all real $t$, where $J$ denotes the log-domain cost.
background
The Cost.Jlog module defines the log-domain cost as the composition of Jcost with the exponential map. An upstream sibling supplies the direct exponential expression, while another upstream result records the composition form. The local setting is the cost domain of Recognition Science, where this function supports the J-uniqueness property in the forcing chain.
proof idea
One-line wrapper that applies reflexivity to the definition of the log-domain cost.
why it matters
The lemma supplies the explicit exponential form required for the J-uniqueness landmark (T5) in UnifiedForcingChain, where J(x) equals cosh(log x) minus one. It underpins later reductions that feed the Recognition Composition Law and the phi-ladder mass formulas, even though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.