def
definition
scheduleVarianceCost
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.ProjectManagement.CriticalPathFromJCost on GitHub at line 36.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
33noncomputable section
34
35/-- J-cost on the actual-to-plan duration ratio. -/
36def scheduleVarianceCost (actual_duration planned_duration : ℝ) : ℝ :=
37 Jcost (actual_duration / planned_duration)
38
39theorem scheduleVarianceCost_on_plan (d : ℝ) (h : d ≠ 0) :
40 scheduleVarianceCost d d = 0 := by
41 unfold scheduleVarianceCost; rw [div_self h]; exact Jcost_unit0
42
43theorem scheduleVarianceCost_nonneg (a p : ℝ) (ha : 0 < a) (hp : 0 < p) :
44 0 ≤ scheduleVarianceCost a p := by
45 unfold scheduleVarianceCost; exact Jcost_nonneg (div_pos ha hp)
46
47/-- Optimal project buffer: J(φ) fraction of critical path. -/
48def optimalBufferFraction : ℝ := phi - 3 / 2
49
50theorem optimalBufferFraction_eq_Jph : optimalBufferFraction = Jcost phi :=
51 Jcost_phi_val.symm
52
53theorem optimalBufferFraction_pos : 0 < optimalBufferFraction := by
54 unfold optimalBufferFraction; linarith [phi_gt_onePointFive]
55
56theorem optimalBufferFraction_lt_half : optimalBufferFraction < 1 / 2 := by
57 unfold optimalBufferFraction; linarith [phi_lt_onePointSixTwo]
58
59structure CriticalPathCert where
60 cost_on_plan : ∀ d : ℝ, d ≠ 0 → scheduleVarianceCost d d = 0
61 cost_nonneg : ∀ a p : ℝ, 0 < a → 0 < p → 0 ≤ scheduleVarianceCost a p
62 buffer_pos : 0 < optimalBufferFraction
63 buffer_lt_half : optimalBufferFraction < 1 / 2
64
65noncomputable def cert : CriticalPathCert where
66 cost_on_plan := scheduleVarianceCost_on_plan