F_ofLog
plain-language theorem explainer
F_ofLog converts an arbitrary real function G into one on positive reals by composing with the natural logarithm. Researchers building log-coordinate models of J-cost or constructing counterexamples to d'Alembert's equation cite it to switch between multiplicative and additive variables. The definition is a direct functional composition that inverts the G_F reparametrization from the FunctionalEquation module.
Claim. For any function $G : ℝ → ℝ$, define $F(x) := G(ℝ.log x)$.
background
The Cost module works with J-cost functions obeying the Recognition Composition Law. Its sibling reparametrization, defined in FunctionalEquation, sets $G_F(t) := F(ℝ.exp t)$. F_ofLog supplies the inverse map, allowing direct use of multiplicative arguments $x > 0$. Upstream, the concrete J-cost in log coordinates is given by $G(t) = ℝ.cosh t - 1$ in Gravity.JCostInflaton, which satisfies the even, base-zero, and cosh-sandwich properties later required by LogModel.
proof idea
The declaration is a one-line definition that applies Real.log to the argument before feeding the result to the supplied G.
why it matters
F_ofLog is invoked to define Fquad and its consistency lemmas in Foundation.DAlembert.Counterexamples, and to populate the LogModel class. It supplies the coordinate change needed to test the Recognition Composition Law under the additive combiner Padd, linking directly to the J-uniqueness and eight-tick octave steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.