G_of
plain-language theorem explainer
G_of supplies the log-lift that converts a cost function F on positive reals into an additive function on the reals via direct substitution G(t) = F(e^t). Analysts working on the analytic bridge cite this shift to turn multiplicative consistency into an additive functional equation ready for differentiation and ODE analysis. The definition is a one-line substitution with no additional lemmas.
Claim. For a cost function $F : (0,∞) → ℝ$, the log-lift is the function $G(t) := F(e^t)$ on the reals.
background
This definition sits inside the Analytic Bridge module, whose goal is to prove that structural axioms on F plus an interaction combiner force the d'Alembert equation on the log-lift. The module documentation states that the log-lift H(t) = F(e^t) + 1 satisfies the target functional equation once the combiner is forced into RCL form. Upstream results supply concrete instances of F, including the gap function F(Z) = log(1 + Z/φ) from AnchorPolicy and the generating functional F(z) = log(1 + z/φ) from Pipelines.
proof idea
The definition is a one-line wrapper that substitutes the exponential argument into F. No lemmas or tactics are invoked; the construction directly implements the shifted log-lift described in the module comment.
why it matters
G_of is invoked by analytic_bridge and analytic_bridge_full, which establish that multiplicative consistency plus interaction implies d'Alembert for the log-lift. It also feeds F_forced_to_Jcost, which recovers the J-cost function J(x) = (x + x^{-1})/2 - 1 from the hyperbolic ODE G'' = G + 1. The definition therefore supplies the change of variable that links the Recognition Composition Law to the self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.