cert_inhabited
plain-language theorem explainer
The declaration establishes existence of a certificate for critical path properties derived from J-cost by direct construction. Project management researchers applying Recognition Science would cite it to confirm a nonempty structure satisfying the buffer inequalities. The proof is a one-line term that supplies the pre-built cert witness to the Nonempty type.
Claim. There exists a structure $C$ such that for all nonzero $d$, the schedule variance cost of $d$ on plan equals zero; for positive actual and planned durations the cost is nonnegative; the optimal buffer fraction is positive; and the optimal buffer fraction is strictly less than $1/2$.
background
The module develops critical path and project buffer from J-cost within Recognition Science. CriticalPathCert is the structure requiring cost on plan to vanish for nonzero durations, cost to remain nonnegative for positive inputs, and the optimal buffer fraction to be positive yet less than one half. This rests on the J-cost function whose fixed point yields the phi-based buffer prediction of approximately 0.118.
proof idea
The proof is a one-line term that directly supplies the cert witness to establish nonemptiness of the CriticalPathCert structure.
why it matters
This theorem closes the existence claim inside the CriticalPathFromJCost module, grounding the J-cost buffer fraction that aligns with Critical Chain Project Management. It supports the Recognition Science prediction of J(phi) approximately 0.118, consistent with the empirical 10-20 percent range cited in the module documentation. The module falsifier remains any large-N study placing the optimal fraction outside (8,20) percent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.