theorem
proved
semanticGate_implies_gap_ready
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 161.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
158 attention ≤ phi ^ (3 : ℕ) :=
159 h.2.2.2.1
160
161theorem semanticGate_implies_gap_ready
162 {entropy entropyFloor attention signature signatureMin signatureMax z : ℝ}
163 (h : SemanticCondensationGate entropy entropyFloor attention
164 signature signatureMin signatureMax z) :
165 phi ^ (45 : ℕ) ≤ z :=
166 h.2.2.2.2
167
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. -/