IndisputableMonolith.Cost.FlogEL
Module FlogEL supplies log-domain cost functions obtained by composing the base Jcost with the exponential map. Researchers analyzing costs in logarithmic coordinates within Recognition Science reference these constructions for equivalence and derivative results. The module is built from a sequence of definitions for Jlog and Flog plus lemmas that establish nonnegativity, zero conditions, and derivative preservation.
claimDefines $Jlog(x) := J(e^x)$ and $Flog$ as the log-domain cost with $Flog(x) = Jlog(x)$ at evaluation points, together with derivative and nonnegativity statements lifted from the base Jcost.
background
The parent Cost module introduces the J-cost function that encodes the Recognition Composition Law. This submodule works in the log domain by composing J with exp, yielding Jlog and the auxiliary Flog. These objects preserve key algebraic features such as nonnegativity while enabling pointwise and derivative comparisons.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module equips the Cost domain with log-domain variants that support later equivalence and derivative lemmas inside the same file. It aligns with the J-uniqueness step (T5) by preserving the functional equation under the exponential change of variable.
depends on (1)
declarations in this module (13)
-
def
Jlog -
lemma
Jlog_eq_zero_iff -
lemma
Jlog_nonneg -
lemma
hasDerivAt_Jlog -
class
AveragingDerivation -
def
Flog -
lemma
Flog_eq_Jlog_pt -
lemma
Flog_eq_Jlog -
lemma
hasDerivAt_Flog_of_derivation -
lemma
deriv_Flog_zero_of_derivation -
lemma
Flog_nonneg_of_derivation -
lemma
Flog_eq_zero_iff_of_derivation -
theorem
T5_EL_equiv_general