optimalBufferFraction
plain-language theorem explainer
The definition sets the optimal project buffer fraction to phi minus 3/2. Recognition Science applications to Critical Chain Project Management cite it as the predicted buffer size of J(phi) approximately 0.118 of critical path duration. It is introduced by direct assignment that matches the closed form of the J-cost evaluated at the golden ratio.
Claim. The optimal project buffer fraction is the real number $b = phi - 3/2$, equivalently $b = J(phi)$ where $J(x) = (x + x^{-1})/2 - 1$.
background
The module treats Critical Chain Project Management as a setting where the J-cost function supplies the minimum nonzero recognition cost. The golden ratio phi is the self-similar fixed point forced by the upstream chain. This definition supplies the explicit real value used to state buffer positivity and the strict upper bound below one half in the CriticalPathCert structure.
proof idea
One-line definition that directly assigns the constant phi - 3/2 to optimalBufferFraction.
why it matters
It supplies the concrete buffer fraction that populates the CriticalPathCert structure, which records cost_on_plan, cost_nonneg, buffer_pos and buffer_lt_half. The module documentation presents it as the RS-native replacement for Goldratt's 50 percent rule, matching the empirical 10-20 percent range reported in Leach and Rand studies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.