cert
plain-language theorem explainer
The cert definition assembles a CriticalPathCert record confirming schedule variance cost vanishes on plan and stays nonnegative off plan, with optimal buffer fraction strictly between zero and one half. Project management researchers applying Recognition Science would cite it to connect Goldratt's critical chain buffer to the J-cost minimum at the golden ratio. The construction is a direct record literal that invokes four supporting lemmas on cost properties and buffer bounds.
Claim. Let $C(a,p)$ be the schedule variance cost for actual duration $a$ and planned duration $p$. The certificate asserts $C(d,d)=0$ for all $d≠0$, $C(a,p)≥0$ whenever $a>0$ and $p>0$, and that the optimal buffer fraction $b$ satisfies $0<b<1/2$.
background
In the CriticalPathFromJCost module schedule variance cost is realized as the J-cost of the ratio of actual to planned duration, inheriting nonnegativity from the foundational cost_nonneg theorem. The optimal buffer fraction is identified with J(φ) where φ is the golden-ratio fixed point; its positivity and strict upper bound below one half follow from the known inequalities 1.5<φ<1.62. The module situates the construction inside Critical Chain Project Management, where the RS prediction replaces the classical 50% buffer rule with a J(φ)≈0.118 fraction of critical-path duration.
proof idea
The definition is a one-line record constructor that directly assigns the four fields of CriticalPathCert to the theorems scheduleVarianceCost_on_plan, scheduleVarianceCost_nonneg, optimalBufferFraction_pos, and optimalBufferFraction_lt_half.
why it matters
This definition packages the concrete certificate for the structural theorem on critical path and project buffer. It realizes the RS prediction that the optimal buffer fraction equals J(φ)≈0.118, matching the empirical range 10-20% reported in Leach 2000 and Rand 2000. The module doc states that any large-N controlled study showing optimal buffers consistently outside (8,20)% would falsify the claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.