CriticalPathCert
plain-language theorem explainer
CriticalPathCert packages four properties asserting that schedule variance cost vanishes on the plan, remains nonnegative for positive durations, and that the optimal buffer fraction is positive yet strictly below one half. Project management researchers applying Recognition Science would cite it to encode the predicted buffer size of J(φ) ≈ 0.118. The declaration is a direct record bundling lemmas already established in sibling definitions.
Claim. A certificate consists of four properties: for every nonzero real duration $d$, the schedule variance cost $J(d/d)$ equals zero; for all positive actual duration $a$ and planned duration $p$, the schedule variance cost $J(a/p)$ is nonnegative; the optimal buffer fraction $J(φ)$ is positive; and $J(φ) < 1/2$.
background
The module formalizes Critical Chain Project Management by replacing the classical 50% buffer rule with a Recognition Science prediction. Schedule variance cost is defined as the J-cost of the ratio of actual to planned duration, where J-cost is the nonnegative recognition cost of any event. Optimal buffer fraction is defined as $φ - 3/2$, which evaluates to the minimum nonzero J-cost value $J(φ) ≈ 0.118$ of the critical path length. The upstream theorem cost_nonneg states that the cost of any recognition event is nonnegative, supplying the nonnegativity field directly.
proof idea
This is a structure definition that assembles four fields. The first field is supplied by the lemma scheduleVarianceCost_on_plan, the second by scheduleVarianceCost_nonneg, the third by optimalBufferFraction_pos, and the fourth by optimalBufferFraction_lt_half. No additional tactics or reductions are performed inside the declaration itself.
why it matters
The structure supplies the certificate type instantiated by the definition cert, which is then shown to be inhabited by the theorem cert_inhabited. It encodes the Recognition Science claim that the optimal project buffer lies in (0, 1/2), matching the J-cost minimum at the identity event and the empirical range 10-20% reported in Leach 2000 and Rand 2000. The declaration closes the structural theorem for the project-management application of the J-cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.