def
definition
IsSaturated
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Unification.RecognitionBandwidth on GitHub at line 167.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
164 demand more recognition events per unit time than the holographic bound permits.
165
166 This is the regime where ILG must activate. -/
167def IsSaturated (area mass dynamicalTime : ℝ) : Prop :=
168 demandedRate mass dynamicalTime ≥ bandwidth area
169
170/-- A system is **sub-saturated** (Newtonian regime) when demand < bandwidth. -/
171def IsSubSaturated (area mass dynamicalTime : ℝ) : Prop :=
172 demandedRate mass dynamicalTime < bandwidth area
173
174/-- Every system is either saturated or sub-saturated (excluded middle). -/
175theorem saturated_or_sub (area mass dynamicalTime : ℝ) :
176 IsSaturated area mass dynamicalTime ∨ IsSubSaturated area mass dynamicalTime := by
177 unfold IsSaturated IsSubSaturated
178 rcases le_or_lt (bandwidth area) (demandedRate mass dynamicalTime) with h | h
179 · left; exact h
180 · right; exact h
181
182end RecognitionBandwidth
183end Unification
184end IndisputableMonolith