def
definition
IsSubcritical
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Unification.CriticalRecognitionLoading on GitHub at line 72.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
69 loadRatio area demand ≤ rhoMin
70
71/-- Subcritical systems remain below the bandwidth ceiling. -/
72def IsSubcritical (area demand : ℝ) : Prop :=
73 demand < bandwidth area
74
75/-- Overloaded systems hit or exceed the bandwidth ceiling. -/
76def IsOverloaded (area demand : ℝ) : Prop :=
77 bandwidth area ≤ demand
78
79/-- The critical-loading band: close to saturation, but still below it. -/
80def InCriticalBand (rhoMin area demand : ℝ) : Prop :=
81 rhoMin < loadRatio area demand ∧ loadRatio area demand < 1
82
83/-- The forced lower edge of the control band from the phase-transition geometry. -/
84abbrev rhoCriticalMin : ℝ := rhoBandLower
85
86theorem rhoCriticalMin_eq : rhoCriticalMin = phi⁻¹ ^ 2 :=
87 RecognitionBandGeometry.rhoBandLower_eq
88
89/-- The fixed control band used by the runtime. -/
90def InForcedCriticalBand (area demand : ℝ) : Prop :=
91 InCriticalBand rhoCriticalMin area demand
92
93theorem loadRatio_pos {area demand : ℝ} (hArea : 0 < area) (hDemand : 0 < demand) :
94 0 < loadRatio area demand := by
95 unfold loadRatio
96 exact div_pos hDemand (bandwidth_pos hArea)
97
98theorem criticalBand_implies_subcritical
99 {rhoMin area demand : ℝ} (hArea : 0 < area)
100 (h : InCriticalBand rhoMin area demand) :
101 IsSubcritical area demand := by
102 rcases h with ⟨_, hlt⟩