LogModel
plain-language theorem explainer
LogModel encodes the interface for a function G on reals that is even, vanishes at zero, and equals cosh(t) minus one via matching upper and lower bounds. Cost-function derivations in Recognition Science cite this when reparametrizing multiplicative costs through logarithms to reach the J-cost. The declaration supplies the class axioms plus two instances that transfer evenness and base-zero directly to F_ofLog G and invoke JensenSketch.of_log_bounds to obtain the axis bounds.
Claim. A function $G : ℝ → ℝ$ is a LogModel when it satisfies $G(-t) = G(t)$ for all real $t$, $G(0) = 0$, and $((e^t + e^{-t})/2 - 1) ≤ G(t) ≤ ((e^t + e^{-t})/2 - 1)$ for all $t$, forcing equality with cosh$(t) - 1$.
background
In the Cost module, LogModel supplies the axioms needed to treat a log-reparametrized cost. The sibling def F_ofLog composes G with Real.log to produce the multiplicative cost function. SymmUnit requires symmetry under inversion for positive arguments together with vanishing at the unit. JensenSketch extends SymmUnit by adding axis_upper and axis_lower bounds relative to Jcost on the exponential axis.
proof idea
The class is defined by the four listed properties. An instance of SymmUnit for F_ofLog G is built by substituting log x into even_log to obtain symmetry and using base0 at log 1 = 0. A second instance of JensenSketch is obtained by applying JensenSketch.of_log_bounds, passing the upper_cosh and lower_cosh fields after dsimp on F_ofLog.
why it matters
This interface feeds the LogModel declaration inside JcostCore and thereby connects the additive log description to the core cost axioms. It realizes the T5 J-uniqueness step by pinning the log model to cosh(t) - 1, which is the expression appearing in the Recognition Composition Law and the self-similar fixed point that generates the phi ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.