optimalBufferFraction_pos
plain-language theorem explainer
The declaration proves that the optimal project buffer fraction, given by the golden ratio minus 1.5, is strictly positive. Critical chain project managers using the Recognition Science J-cost model would cite this to support buffer sizes near 11.8 percent of the critical path. The proof is a one-line wrapper that unfolds the definition and applies linear arithmetic to the phi lower bound lemma.
Claim. $0 < phi - 3/2$, where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
In the CriticalPathFromJCost module the framework models project buffers via the J-cost at the golden ratio. The definition sets optimalBufferFraction to phi minus three halves, which equals J(phi) by the recognition composition law. This depends on the upstream lemma phi_gt_onePointFive establishing phi > 1.5 from the quadratic minimal polynomial of phi.
proof idea
The proof is a one-line wrapper. It unfolds optimalBufferFraction to phi - 3/2 and invokes linarith using the fact phi > 1.5.
why it matters
This supplies the buffer_pos field in the CriticalPathCert structure, which certifies the full J-cost schedule model. It implements the RS claim that the optimal buffer fraction is J(phi), the minimal nonzero recognition cost, linking to the phi fixed point in the forcing chain. The module falsifier states that controlled studies showing optimal buffers outside (8,20) percent would refute the prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.