LogModel
plain-language theorem explainer
LogModel axiomatizes functions G:ℝ→ℝ that are even, vanish at zero, and equal cosh(t)−1 identically via matching upper and lower bounds. Researchers reparametrizing the J-cost to logarithmic coordinates cite this when moving from the multiplicative functional equation to additive form in t. The declaration is a direct class definition whose two cosh inequalities collapse to equality with no lemmas or tactics applied.
Claim. A function $G:ℝ→ℝ$ is a log model when it satisfies $G(-t)=G(t)$ for all $t$, $G(0)=0$, and $G(t)=((e^t+e^{-t})/2-1)$ for all $t$.
background
In Recognition Science the J-cost is the function J(x)=(x+x^{-1})/2−1. The change of variable t=log x converts it to G(t)=J(e^t), which equals cosh(t)−1 exactly. The LogModel class records the four properties any such G must obey: evenness under t↦−t, vanishing at the origin, and the two-sided bound by the hyperbolic-cosine expression. This supplies the concrete interface used by the main LogModel declaration in the Cost module. Upstream results include the RS-native gravitational constant G=λ_rec²c³/(πℏ) from Constants, the reparametrization G_F(t)=F(exp t) from FunctionalEquation, and the explicit inflaton form G(t)=cosh(t)−1 from Gravity.JCostInflaton.
proof idea
The declaration is a direct class definition with an empty body. The four fields even_log, base0, upper_cosh and lower_cosh are stated verbatim; the pair of cosh inequalities forces G(t)=cosh(t)−1 pointwise. No lemmas are applied and no tactics are used.
why it matters
This supplies the precise log-coordinate interface required by the parent LogModel class in the Cost module. It realizes the T5 J-uniqueness step of the forcing chain by exhibiting the explicit solution G(t)=cosh(t)−1 that satisfies the Recognition Composition Law after the exponential reparametrization. The definition closes the passage from the multiplicative J-cost to the additive form used in subsequent derivations of the phi-ladder and mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.