def definition def or abbrev

`cert`

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

formal statement (Lean)

  65noncomputable def cert : CriticalPathCert where
  66  cost_on_plan := scheduleVarianceCost_on_plan

proof body

Definition body.

  67  cost_nonneg := scheduleVarianceCost_nonneg
  68  buffer_pos := optimalBufferFraction_pos
  69  buffer_lt_half := optimalBufferFraction_lt_half
  70

depends on (6)

Lean names referenced from this declaration's body.

cost_nonneg in IndisputableMonolith.Foundation.ObserverForcing decl_use
CriticalPathCert in IndisputableMonolith.ProjectManagement.CriticalPathFromJCost decl_use
optimalBufferFraction_lt_half in IndisputableMonolith.ProjectManagement.CriticalPathFromJCost decl_use
optimalBufferFraction_pos in IndisputableMonolith.ProjectManagement.CriticalPathFromJCost decl_use
scheduleVarianceCost_nonneg in IndisputableMonolith.ProjectManagement.CriticalPathFromJCost decl_use
scheduleVarianceCost_on_plan in IndisputableMonolith.ProjectManagement.CriticalPathFromJCost decl_use