`harm_linearization_correct`

proved

show as: view math explainer →

module: IndisputableMonolith.Cost.Derivative
domain: Cost
line: 134 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cost.Derivative on GitHub at line 134.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 131/-- **Main Theorem**: The harm linear term is the correct directional derivative.
 132
 133    This justifies using linBondDelta in the harm decomposition. -/
 134theorem harm_linearization_correct (x L : ℝ) (hx : 0 < x) :
 135    -- The linearization linJ captures the first-order behavior of J along exp paths
 136    linJ x L = deriv Jcost x * x * L :=
 137  linJ_eq_derivative_times_x x L hx
 138
 139end Cost
 140end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.