J_log
plain-language theorem explainer
J_log(ε) evaluates the J-cost at exp(ε), which equals cosh(ε) minus one. Researchers deriving the continuum limit from the simplicial ledger cite this to shift from multiplicative to additive coordinates for Laplacian identification. The definition is a direct composition of the exponential with the base J-cost functional.
Claim. $J_ {log}(ε) := J(e^ε)$ where $J(x) = (x + x^{-1})/2 - 1$, equivalently $J(e^ε) = cosh(ε) - 1$.
background
The ContinuumBridge module establishes that J-cost stationarity on the simplicial ledger yields the Regge action and converges to the Einstein field equations. In log coordinates ε = ln ψ the coupling term J(ψ1/ψ2) expands quadratically as (ε1 - ε2)^2/2 + O((ε1 - ε2)^4), matching the structure of a discrete Laplacian and the Regge action Σ δ_h A_h.
proof idea
One-line definition that composes Jcost with Real.exp. It draws on the upstream J_log from DiscretenessForcing, which states J in log coordinates: J(e^t) = cosh(t) - 1, a convex bowl centered at t = 0.
why it matters
This definition supplies the log-coordinate form required for the module's derivation chain from SimplicialLedger.J_global through discrete Laplacian identification to Regge action and EFE convergence. It is invoked by downstream results in DiscretenessForcing including discreteness_forcing_principle (which uses the curvature J''(1) = 1) and cosh_quadratic_bound. It directly supports the quadratic structure of J-cost that forces D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.