theorem proved term proof

`jcost_deriv_zero_at_one`

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

formal statement (Lean)

  87theorem jcost_deriv_zero_at_one : jcost_deriv 1 = 0 := by

proof body

Term-mode proof.

  88  unfold jcost_deriv; simp
  89
  90/-- **THEOREM IC-005.7**: J'(x) > 0 for x > 1.
  91    The gradient points upward away from the minimum for x > 1. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

ic005_certificate in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use

depends on (4)

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
jcost_deriv in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
gradient in IndisputableMonolith.Relativity.Fields.Scalar decl_use