def
definition
InCriticalBand
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 80.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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⟩
103 unfold IsSubcritical
104 unfold loadRatio at hlt
105 have hB : 0 < bandwidth area := bandwidth_pos hArea
106 rw [div_lt_one hB] at hlt
107 simpa using hlt
108
109theorem criticalBand_not_overloaded
110 {rhoMin area demand : ℝ} (hArea : 0 < area)