No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
43theorem scheduleVarianceCost_nonneg (a p : ℝ) (ha : 0 < a) (hp : 0 < p) :
44 0 ≤ scheduleVarianceCost a p := by
proof body
Term-mode proof.
45 unfold scheduleVarianceCost; exact Jcost_nonneg (div_pos ha hp)
46
47/-- Optimal project buffer: J(φ) fraction of critical path. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
cert
in IndisputableMonolith.ProjectManagement.CriticalPathFromJCost
decl_use
depends on (12)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
Jcost_nonneg
in IndisputableMonolith.Cost
decl_use
-
Jcost_nonneg
in IndisputableMonolith.Cost.JcostCore
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
project
in IndisputableMonolith.Foundation.Determinism
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
Jcost_nonneg
in IndisputableMonolith.Gravity.CoherenceCollapse
decl_use
-
Jcost_nonneg
in IndisputableMonolith.Gravity.EnergyProcessingBridge
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
Jcost_nonneg
in IndisputableMonolith.NavierStokes.PhiLadderCutoff
decl_use
-
scheduleVarianceCost
in IndisputableMonolith.ProjectManagement.CriticalPathFromJCost
decl_use