`IsCriticalRecognitionLoading`

definition

show as: view math explainer →

module: IndisputableMonolith.Unification.CriticalRecognitionLoading
domain: Unification
line: 185 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Unification.CriticalRecognitionLoading on GitHub at line 185.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 182  hDemand : 0 < demand
 183
 184/-- The full critical-loading condition. -/
 185def IsCriticalRecognitionLoading (rhoMin : ℝ) (s : ControllerState) : Prop :=
 186  InCriticalBand rhoMin s.area s.demand ∧
 187    SemanticCondensationGate
 188      s.entropy s.entropyFloor s.attention
 189      s.signature s.signatureMin s.signatureMax s.z
 190
 191/-- The non-parameterized critical-loading condition. -/
 192def IsForcedCriticalRecognitionLoading (s : ControllerState) : Prop :=
 193  IsCriticalRecognitionLoading rhoCriticalMin s
 194
 195/-- Penalty for leaving the critical-loading band. -/
 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 : ℕ) ∧

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.