maintenanceDemand_zero_iff

formal source

 130  exact mul_nonneg (le_of_lt barrierPeriod_pos) (Cost.Jcost_nonneg hL)
 131
 132/-- Maintenance demand is zero only when L = 1 (identity scale). -/
 133theorem maintenanceDemand_zero_iff {L : ℝ} (hL : 0 < L) :
 134    maintenanceDemand L = 0 ↔ L = 1 := by
 135  unfold maintenanceDemand
 136  constructor
 137  · intro h
 138    have hb := barrierPeriod_pos
 139    have := (mul_eq_zero.mp h).resolve_left (ne_of_gt hb)
 140    exact (Cost.Jcost_eq_zero_iff L hL).mp this
 141  · intro h
 142    rw [h, Cost.Jcost_unit0, mul_zero]
 143
 144/-! ## §5. Critical Extent -/
 145
 146/-- A boundary is **holographically viable** if its maintenance demand
 147    does not exceed its holographic budget.
 148
 149    This is the bandwidth constraint on consciousness. -/
 150def IsViable (L : ℝ) : Prop :=
 151  maintenanceDemand L ≤ maintenanceBudget L
 152
 153/-- The identity scale L = 1 is always viable (zero demand). -/
 154theorem identity_viable : IsViable 1 := by
 155  unfold IsViable maintenanceDemand maintenanceBudget
 156  rw [Cost.Jcost_unit0, mul_zero]
 157  exact le_of_lt (maintenanceBudget_pos (by norm_num : (0:ℝ) < 1))
 158
 159/-! ## §6. Z-Complexity Increases Demand -/
 160
 161/-- For a system with Z-complexity (conserved information integer),
 162    the maintenance demand scales with complexity:
 163