alpha_locked_in_unit

formal source

 138  ring
 139
 140/-- The ILG modification parameter α = (1−1/φ)/2 is between 0 and 1. -/
 141theorem alpha_locked_in_unit : 0 < alpha_locked ∧ alpha_locked < 1 :=
 142  ⟨alpha_locked_pos, alpha_locked_lt_one⟩
 143
 144/-! ## §5. Demanded Recognition Rate -/
 145
 146/-- The recognition event rate demanded by Newtonian gravitational dynamics
 147    of mass M at dynamical time T_dyn.
 148
 149    Each Planck-mass element requires one ledger update per dynamical time:
 150        R_demand = M / (m_P · T_dyn)
 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 :=