def
definition
optimalBufferFraction
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 48.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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
67 cost_nonneg := scheduleVarianceCost_nonneg
68 buffer_pos := optimalBufferFraction_pos
69 buffer_lt_half := optimalBufferFraction_lt_half
70
71theorem cert_inhabited : Nonempty CriticalPathCert := ⟨cert⟩
72
73end
74end CriticalPathFromJCost
75end ProjectManagement
76end IndisputableMonolith