G_of_F
plain-language theorem explainer
This definition supplies the log-coordinate representation G(t) = F(exp(t)) of an arbitrary cost function F, enabling curvature analysis in the d'Alembert form of the Recognition metric. Workers on the geometric classification of cost functions cite it to separate the flat counterexample from the hyperbolic case required by the Recognition Composition Law. The implementation is a direct functional composition with the exponential map.
Claim. For a cost function $F : ℝ → ℝ$, the log-lifted representation is defined by $G(t) := F(e^t)$.
background
The Curvature Gate module requires that the cost metric has constant nonzero curvature. The log-coordinate representation G(t) = F(e^t) defines a 1D metric via ds² = G''(t) dt². This distinguishes flat (κ = 0): G(t) = t²/2, hyperbolic (κ = -1): G(t) = cosh(t) - 1 (the RCL), and spherical (κ = +1): G(t) = 1 - cos(t) (ruled out by F ≥ 0). Upstream results supply concrete F instances, including the gap function F(Z) = log(1 + Z/φ)/log(φ) from AnchorPolicy and the generating functional F(z) = log(1 + z/φ) from Pipelines.
proof idea
This is a direct definition implementing the log-lift via substitution of the exponential argument. No lemmas are applied; it is the primitive operation that shifts the cost function into logarithmic coordinates for subsequent curvature checks.
why it matters
This definition is used by H_of_F to produce the shifted version G + 1. It fills the role in the Curvature Gate of providing the coordinate change needed to analyze the metric curvature, which must be hyperbolic to satisfy the Recognition Composition Law and the J-uniqueness from the forcing chain (T5). It supports the requirement that recognition geometry is non-trivially curved, ruling out flat space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.