scheduleVarianceCost_on_plan
plain-language theorem explainer
When actual and planned durations are equal and nonzero, the J-cost of their ratio vanishes. Critical-chain project schedulers cite the result to confirm zero baseline cost under the Recognition Science model. The proof is a one-line wrapper that unfolds the variance definition, reduces the ratio to unity, and invokes the unit lemma for J-cost.
Claim. For any nonzero real number $d$, the J-cost of the actual-to-planned duration ratio is zero when the durations coincide: $J(d/d)=0$, where $J(x)=(x-1)^2/(2x)$.
background
The module adapts Critical Chain Project Management to Recognition Science by defining schedule variance cost as the J-cost applied to the ratio of actual task duration to planned duration. The J-cost function is given by the squared-ratio expression and satisfies $J(1)=0$ by direct simplification, as recorded in the Cost module. Local context replaces the conventional 50% project buffer with the RS prediction that the optimal buffer fraction is $J(φ)≈0.118$ of critical-path length, the minimum nonzero recognition cost.
proof idea
One-line wrapper: unfold the definition of schedule variance cost to obtain J-cost of the duration ratio, rewrite the ratio to 1 using the nonzero hypothesis, then apply the lemma that J-cost at argument 1 equals zero.
why it matters
The theorem supplies the cost-on-plan field inside the CriticalPathCert record. It thereby certifies that execution exactly on plan incurs zero recognition cost, consistent with the framework minimum at unity ratio. The module as a whole contrasts CCPM buffer sizing with the RS value $J(φ)$ and lists empirical studies (Leach 2000; Rand 2000) as supporting evidence within the (8,20)% band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.