`harm_linearization_correct`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cost.Derivative on GitHub at line 134.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.