F_ofLog
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assume G satisfies evenness or non-negativity.
- Does not enforce the Recognition Composition Law on the output.
- Does not incorporate constants such as G, phi, or hbar.
- Does not restrict the domain of G beyond real-to-real maps.
Lean usage
noncomputable def Fquad : ℝ → ℝ := Cost.F_ofLog Gquadformal statement (Lean)
107noncomputable def F_ofLog (G : ℝ → ℝ) : ℝ → ℝ := fun x => G (Real.log x)
proof body
Definition body.
108