class definition def or abbrev

`UnitCurvature`

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

Last generation error: xAI API error (429): The model is currently at capacity due to high demand. Please try again in a few minutes. For guaranteed processing and availability, please request Provisioned Throughput: https://docs.x.ai/developers/advanced-api-usage/provisioned-throughput

generate prose now

formal statement (Lean)

  61class UnitCurvature (F : ℝ → ℝ) : Prop where
  62  second_deriv_at_identity : deriv (deriv (F ∘ exp)) 0 = 1
  63
  64instance : UnitCurvature Jcost where
  65  second_deriv_at_identity := Jcost_comp_exp_second_deriv_at_zero

proof body

Definition body.

  66
  67end Cost
  68end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.

Jcost_comp_exp_second_deriv_at_zero in IndisputableMonolith.Cost.Calibration decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use