theorem
proved
semanticGate_implies_attention_cap
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 154.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
151 attention ≤ phi ^ (3 : ℕ) ∧
152 phi ^ (45 : ℕ) ≤ z
153
154theorem semanticGate_implies_attention_cap
155 {entropy entropyFloor attention signature signatureMin signatureMax z : ℝ}
156 (h : SemanticCondensationGate entropy entropyFloor attention
157 signature signatureMin signatureMax z) :
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. -/