Flog
plain-language theorem explainer
Flog defines the composition of an arbitrary real function F with the exponential, producing a cost evaluated at the log-domain variable t. Workers on log-domain cost functions and averaging derivations in Recognition Science cite it to shift between linear and exponential scales. The declaration is a direct one-line definition with no lemmas or tactics.
Claim. For a function $F : ℝ → ℝ$, the log-domain cost is given by $Flog(F, t) := F(e^t)$.
background
The Cost.FlogEL module develops log-domain versions of cost functions by composing the generating functional with the exponential map. The local setting is the composition of Jcost with exp to obtain a function of the additive variable t, enabling direct comparison with Jlog. Upstream, F denotes the generating functional $F(z) := log(1 + z/φ)$ (Pipelines) or the equivalent gap function $F(Z) = log(1 + Z/φ)/log(φ)$ (AnchorPolicy), both of which serve as the master gap generator at z = 1.
proof idea
This is a direct definition: Flog F t is set equal to F (exp t). No lemmas are invoked inside the definition itself; downstream results such as Flog_eq_Jlog_pt and Flog_eq_Jlog apply the AveragingDerivation.agrees hypothesis to identify the result with Jlog.
why it matters
Flog supplies the log-domain bridge that lets AveragingDerivation equate the composed function to Jlog, after which non-negativity, zero-equivalence, and derivative lemmas follow by transport from the corresponding Jlog facts. It supports the shift to logarithmic variables required for analyzing costs on the phi-ladder and near the T5 J-uniqueness fixed point. The definition is invoked by eight downstream declarations inside the same module, including the equivalence Flog_eq_Jlog and the derivative result hasDerivAt_Flog_of_derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.