`ControllerState`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Unification.CriticalRecognitionLoading on GitHub at line 171.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 168/-! ## §4. Controller state and certificate -/
 169
 170/-- Minimal runtime state needed by the governor. -/
 171structure ControllerState where
 172  area : ℝ
 173  demand : ℝ
 174  entropy : ℝ
 175  entropyFloor : ℝ
 176  attention : ℝ
 177  signature : ℝ
 178  signatureMin : ℝ
 179  signatureMax : ℝ
 180  z : ℝ
 181  hArea : 0 < area
 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) :

papers checked against this theorem

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