Flog_nonneg_of_derivation
plain-language theorem explainer
The lemma shows that Flog remains nonnegative whenever F obeys the averaging derivation rule. Cost-function analysts in the Recognition Science program cite it to complete the minimum property in the log domain. Its proof is a direct reduction to the nonnegativity of the underlying Jlog via the equality lemma that equates the two at each point.
Claim. If $F : {R} {to} {R}$ satisfies the averaging derivation condition, then $0 {leq} F(e^{t})$ for every real $t$.
background
The module treats log-domain costs obtained by composing Jcost with the exponential map. AveragingDerivation is the typeclass asserting that F(exp t) coincides with Jcost(exp t) for all t, thereby identifying Flog with Jlog. The upstream lemma Jlog_nonneg asserts 0 {leq} Jlog t, justified by the AM-GM inequality on exp t and its reciprocal, as noted in its doc-comment that J(x) > 0 for x {neq} 1 and x > 0.
proof idea
This is a one-line wrapper. It pulls the nonnegativity statement for Jlog t from the lemma Jlog_nonneg and rewrites the target using the equality Flog F t = Jlog t supplied by the companion lemma Flog_eq_Jlog_pt.
why it matters
It supplies the nonnegativity clause required by the general T5 equivalence theorem T5_EL_equiv_general in the same module. That theorem assembles derivative zero, nonnegativity, and zero-equivalence into the full T5 statement for the EL cost. In the broader framework this confirms the J-uniqueness property (T5) in the logarithmic representation, supporting the self-similar fixed point and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.