F_ofLog
plain-language theorem explainer
The log reparametrization operator converts any real-valued function G into a new function on the multiplicative domain by composing with the natural logarithm. Model builders working on J-cost symmetries or DAlembert counterexamples cite it to move between additive log coordinates and the original scale. The construction is a direct functional definition with no lemmas or reductions required.
Claim. For any function $G : ℝ → ℝ$, define the reparametrized map by $F(G)(x) := G(ℝ.log x)$.
background
The Cost module studies cost functions that obey the Recognition Composition Law and related symmetries. Upstream, the FunctionalEquation module introduces the forward reparametrization $G_F(t) := F(ℝ.exp t)$ to shift multiplicative arguments into additive log space. The JCostInflaton module supplies the concrete example $G(t) = ℝ.cosh t - 1$, which equals the J-cost evaluated at $e^t$ and satisfies evenness together with the cosh bounds. F_ofLog supplies the inverse map that recovers the original multiplicative variable.
proof idea
One-line definition that composes the input function G with the natural logarithm on the positive reals.
why it matters
The operator is required by the LogModel class to state even_log, base0, and the cosh sandwich inequalities in additive coordinates. It is instantiated to build the quadratic counterexample Fquad and its consistency lemmas in the DAlembert foundations, allowing direct verification of the Recognition Composition Law on log-scale functions. This step supports the J-uniqueness and self-similar fixed-point results in the T5-T6 forcing chain by keeping coordinate changes explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.