theorem proved term proof

`harm_linearization_correct`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 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 :=

proof body

Term-mode proof.

 137  linJ_eq_derivative_times_x x L hx
 138
 139end Cost
 140end IndisputableMonolith

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
linJ in IndisputableMonolith.Cost.Derivative decl_use
linJ_eq_derivative_times_x in IndisputableMonolith.Cost.Derivative decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use