criticalRecognitionLoading_certificate

formal source

 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 ∧
 230      s.attention ≤ phi ^ (3 : ℕ) ∧
 231      phi ^ (45 : ℕ) ≤ s.z ∧
 232      pulseTicks ∣ supervisoryTicks ∧
 233      loadPenalty rhoCriticalMin s.area s.demand = 0 := by
 234  exact criticalRecognitionLoading_certificate h
 235
 236end
 237end CriticalRecognitionLoading
 238end Unification
 239end IndisputableMonolith