optimalBufferFraction_lt_half
plain-language theorem explainer
The theorem establishes that the optimal project buffer fraction J(φ) is strictly less than one half. Critical chain project managers would cite this to justify buffers below 50% of critical path length. The proof is a one-line wrapper that unfolds the definition and applies linear arithmetic with the bound φ < 1.62.
Claim. $J(φ) < 1/2$, where $J(x) = (x + x^{-1})/2 - 1$ and $φ = (1 + √5)/2$ is the golden ratio.
background
The CriticalPathFromJCost module defines the optimal project buffer fraction as J(φ) = φ - 3/2, the minimum nonzero recognition cost in the Recognition Science framework. This contrasts with the traditional 50% buffer in Critical Chain Project Management (Goldratt 1997) and predicts J(φ) ≈ 0.118, consistent with empirical 10-20% buffers from Leach 2000 and Rand 2000. The upstream lemma phi_lt_onePointSixTwo states φ < 1.62, obtained by bounding √5 < 2.24.
proof idea
The proof is a one-line wrapper. It unfolds optimalBufferFraction to φ - 3/2, then invokes linarith supplying the fact φ < 1.62 to obtain the strict inequality.
why it matters
This populates the buffer_lt_half field inside the CriticalPathCert structure. It supports the Recognition Science prediction that the optimal buffer is J(φ) rather than 50%, tying into T5 (J-uniqueness) and T6 (φ as self-similar fixed point) of the unified forcing chain. The module falsifier is any large-N study showing optimal buffers consistently outside (8, 20)%.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.