optimalBufferFraction_eq_Jph
plain-language theorem explainer
The declaration equates the optimal project buffer fraction to the J-cost of the golden ratio. Operations researchers and critical chain practitioners would cite it to justify setting the buffer at J(φ) ≈ 0.118 of critical path length. The proof is a one-line wrapper applying symmetry of the lemma that fixes Jcost phi as phi minus 3/2.
Claim. The optimal project buffer fraction equals the J-cost of the golden ratio: optimalBufferFraction = J(φ), where J(φ) = φ - 3/2.
background
The module treats Critical Chain Project Management, where the project buffer is a fraction of the critical path sum of task durations. Recognition Science predicts this fraction equals J(φ), the minimum nonzero recognition cost at the golden ratio. The upstream lemma Jcost_phi_val states Jcost phi = phi - 3/2 exactly, using φ² = φ + 1 and algebraic simplification. The sibling definition optimalBufferFraction sets the same value directly as phi - 3/2.
proof idea
One-line wrapper that applies Jcost_phi_val.symm to equate the definition to the lemma value.
why it matters
The result confirms the project buffer definition matches the J-cost from the forcing chain at T5. It closes the structural theorem for the module, aligning the RS prediction J(φ) ≈ 0.118 with empirical buffers of 10-20 percent. The module doc cites Leach and Rand studies as consistency checks and lists the falsifier as any large-N study placing the optimum outside (8,20) percent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.