loadPenalty_zero_of_critical

formal source

 196def loadPenalty (rhoMin area demand : ℝ) : ℝ :=
 197  max 0 (rhoMin - loadRatio area demand) + max 0 (loadRatio area demand - 1)
 198
 199theorem loadPenalty_zero_of_critical
 200    {rhoMin area demand : ℝ}
 201    (h : InCriticalBand rhoMin area demand) :
 202    loadPenalty rhoMin area demand = 0 := by
 203  unfold loadPenalty
 204  have hLeft : rhoMin - loadRatio area demand ≤ 0 := by
 205    linarith [h.1]
 206  have hRight : loadRatio area demand - 1 ≤ 0 := by
 207    linarith [h.2]
 208  rw [max_eq_left hLeft, max_eq_left hRight]
 209  ring
 210
 211theorem criticalRecognitionLoading_certificate
 212    {rhoMin : ℝ} {s : ControllerState}
 213    (h : IsCriticalRecognitionLoading rhoMin s) :
 214    IsSubcritical s.area s.demand ∧
 215      s.attention ≤ phi ^ (3 : ℕ) ∧
 216      phi ^ (45 : ℕ) ≤ s.z ∧
 217      pulseTicks ∣ supervisoryTicks ∧
 218      loadPenalty rhoMin s.area s.demand = 0 := by
 219  refine ⟨?_, ?_, ?_, ?_, ?_⟩
 220  · exact criticalBand_implies_subcritical s.hArea h.1
 221  · exact semanticGate_implies_attention_cap h.2
 222  · exact semanticGate_implies_gap_ready h.2
 223  · exact pulse_divides_supervisory
 224  · exact loadPenalty_zero_of_critical h.1
 225
 226theorem forcedCriticalRecognitionLoading_certificate
 227    {s : ControllerState}
 228    (h : IsForcedCriticalRecognitionLoading s) :
 229    IsSubcritical s.area s.demand ∧