G
plain-language theorem explainer
The definition reparametrizes an arbitrary real function F into logarithmic coordinates by setting G(t) to F of e to the t. Researchers establishing uniqueness of the J-cost functional at forcing-chain step T5 cite this reparametrization when converting between multiplicative and additive forms of the composition law. It is realized as a direct one-line mapping with no auxiliary conditions.
Claim. For any function $F : ℝ → ℝ$, define the reparametrized map $G_F(t) := F(e^t)$.
background
The module supplies helper material for the T5 uniqueness argument in the forcing chain. The log reparametrization converts the multiplicative variable x of the cost functional into an additive coordinate t = log x, which simplifies application of differential operators and d'Alembert-type equations. The J-cost is defined by $J(x) = ½(x + x^{-1}) - 1$, equivalently cosh(log x) - 1, and obeys the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. Upstream results supply the concrete realization G(t) = cosh(t) - 1 for the inflaton potential and the gap function F(Z) = log(1 + Z/φ)/log(φ).
proof idea
The declaration is a one-line definition that composes the input function F with the real exponential map. No lemmas or tactics are applied; the construction is purely notational to support later derivative and regularity arguments in log space.
why it matters
This reparametrization supports the parent result that any cost algebra satisfying the axioms plus calibration of the second derivative at zero must coincide with J. It occupies a supporting position in forcing-chain step T5 and enables downstream derivations of mass formulas on the phi-ladder together with zero-parameter certificates for astrophysical observables. It indirectly connects to the eight-tick octave and the derivation of D = 3 while leaving open the full unification of all constants under the Meta-Principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.