def
definition
SemanticCondensationGate
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 146.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
143 linarith
144
145/-- Query-level semantic admissibility region. -/
146def SemanticCondensationGate
147 (entropy entropyFloor attention signature signatureMin signatureMax z : ℝ) : Prop :=
148 entropyFloor < entropy ∧
149 signatureMin ≤ signature ∧
150 signature ≤ signatureMax ∧
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 : ℝ