demandedRate

formal source

 151
 152    In RS-native units with m_P = 1:
 153        R_demand = M / T_dyn -/
 154noncomputable def demandedRate (mass dynamicalTime : ℝ) : ℝ :=
 155  mass / dynamicalTime
 156
 157theorem demandedRate_pos {M T : ℝ} (hM : 0 < M) (hT : 0 < T) :
 158    0 < demandedRate M T :=
 159  div_pos hM hT
 160
 161/-! ## §6. Saturation Predicate -/
 162
 163/-- A gravitating system is **bandwidth-saturated** when its Newtonian dynamics
 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