theorem proved wrapper

`optimalBufferFraction_lt_half`

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

formal statement (Lean)

  56theorem optimalBufferFraction_lt_half : optimalBufferFraction < 1 / 2 := by

One-line wrapper that applies unfold.

  57  unfold optimalBufferFraction; linarith [phi_lt_onePointSixTwo]
  58

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

cert in IndisputableMonolith.ProjectManagement.CriticalPathFromJCost decl_use

Lean names referenced from this declaration's body.

phi_lt_onePointSixTwo in IndisputableMonolith.Constants decl_use
optimalBufferFraction in IndisputableMonolith.ProjectManagement.CriticalPathFromJCost decl_use