scheduleVarianceCost_nonneg
plain-language theorem explainer
The theorem shows that schedule variance cost is nonnegative whenever activity duration a and critical path length p are positive reals. Critical-chain project managers would cite it when bounding deterministic buffer sizes from J-cost. The proof is a one-line wrapper that unfolds the definition and invokes the general Jcost_nonneg lemma on the positive ratio a/p.
Claim. For all real numbers $a>0$ and $p>0$, the schedule variance cost satisfies $0≤J(a/p)$, where $J(x)=(x+1/x)/2-1$ is the recognition cost function.
background
The J-cost function $J(x)$ for $x>0$ is defined by $J(x)=(x+x^{-1})/2-1$, equivalently $cosh(log x)-1$, and is nonnegative by the AM-GM inequality. The module applies this to Critical Chain Project Management: a denotes a task duration on the critical path and p the total critical path length, so that schedule variance cost is the J-cost of their ratio. Upstream lemmas include Jcost_nonneg from the Cost module, which states $J(x)≥0$ for $x>0$, together with positivity preservation under division.
proof idea
The proof is a one-line wrapper. It unfolds scheduleVarianceCost to expose Jcost of the ratio a/p, then applies the lemma Jcost_nonneg to the fact that a/p>0, which follows immediately from div_pos ha hp.
why it matters
The result supplies the cost_nonneg field of the CriticalPathCert structure defined later in the same module. That certificate encodes the RS prediction that the optimal project buffer is the J(φ) fraction of the critical path, with J(φ)≈0.118. The module documentation notes consistency with empirical buffer studies in the 10-20% range. It closes a basic nonnegativity step in the project-management application of the forcing chain and Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.