J_log_eq_J_exp
plain-language theorem explainer
The equality equates the logarithmic cost J_log(t) to the defect of e^t, bridging multiplicative and additive representations of the J-cost. Researchers analyzing the cost bowl for discreteness forcing cite it to justify coordinate changes in stability arguments. The proof is a direct term simplification that invokes the definitions of J_log and defect together with the hyperbolic cosine identity and an exponential negation rewrite.
Claim. For every real number $t$, $J(t) = D(e^{t})$, where $J(t) := J(e^{t})$ is defined by $J(t) = J(e^{t}) = J(e^{t})$ with $J(x) = (x + x^{-1})/2 - 1$ and $D(x) := J(x)$ is the defect functional.
background
The DiscretenessForcing module shows that continuous configuration spaces admit no isolated J-minima because infinitesimal perturbations incur vanishing cost, while discrete spaces permit stable minima at finite step cost. J_log is the sibling definition J_log(t) := cosh(t) - 1, the image of the original J under the substitution x = e^t. Defect is the upstream definition defect(x) := J(x) for positive x, taken from LawOfExistence.
proof idea
The proof is a one-line term wrapper. It applies simp only on the definitions J_log, defect, J and the lemma Real.cosh_eq, then rewrites with Real.exp_neg to match the two exponential terms inside the hyperbolic cosine.
why it matters
It supplies the coordinate bridge required by the downstream theorem zeroDefect_eq_J_log in NumberTheory.ZeroLocationCost, which rewrites the zero-location defect exactly as J_log of the deviation. The result fills the explicit connection step stated in the module doc-comment, enabling the main theorems continuous_no_stable_minima and rs_exists_requires_discrete that derive discreteness from the J-cost landscape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.