identity_viable

formal source

 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
 164        demand(L, Z) = barrierPeriod · J(L) · (1 + |Z| · k_R)
 165
 166    Higher Z requires more recognition events per barrier cycle. -/
 167noncomputable def complexDemand (L : ℝ) (Z : ℤ) : ℝ :=
 168  maintenanceDemand L * (1 + |Z| * k_R)
 169
 170/-- Complex demand ≥ simple demand for any Z. -/
 171theorem complexDemand_ge {L : ℝ} (hL : 0 < L) (Z : ℤ) :
 172    maintenanceDemand L ≤ complexDemand L Z := by
 173  unfold complexDemand
 174  have hd := maintenanceDemand_nonneg hL
 175  have hfac : 1 ≤ 1 + ↑|Z| * k_R := by
 176    have : 0 ≤ ↑|Z| * k_R := mul_nonneg (by exact_mod_cast abs_nonneg Z) (le_of_lt k_R_pos)
 177    linarith
 178  calc maintenanceDemand L
 179      = maintenanceDemand L * 1 := (mul_one _).symm
 180    _ ≤ maintenanceDemand L * (1 + ↑|Z| * k_R) := by
 181        apply mul_le_mul_of_nonneg_left hfac hd
 182
 183/-- Higher Z-complexity strictly increases demand (when J > 0). -/
 184theorem higher_Z_more_demand {L : ℝ} (hL : 0 < L) (hL1 : L ≠ 1)