pith. machine review for the scientific record. sign in
def

SemanticCondensationGate

definition
show as:
view math explainer →
module
IndisputableMonolith.Unification.CriticalRecognitionLoading
domain
Unification
line
146 · 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 146.

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

 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 : ℝ