maintenanceBudget_pos

formal source

 103noncomputable def maintenanceBudget (L : ℝ) : ℝ :=
 104  boundaryArea L / (4 * planckArea * k_R)
 105
 106theorem maintenanceBudget_pos {L : ℝ} (hL : 0 < L) : 0 < maintenanceBudget L := by
 107  unfold maintenanceBudget
 108  apply div_pos (boundaryArea_pos hL)
 109  apply mul_pos
 110  apply mul_pos
 111  · linarith [planckArea_pos]
 112  · exact planckArea_pos
 113  · exact k_R_pos
 114
 115/-! ## §4. Maintenance Demand -/
 116
 117/-- The recognition cost of maintaining a boundary of extent L over the
 118    consciousness barrier period.
 119
 120    Uses the canonical J-cost: BoundaryCost = τ · J(L/λ_rec).
 121    In RS-native units with λ_rec = ℓ_P = 1:
 122        demand = 360 · J(L). -/
 123noncomputable def maintenanceDemand (L : ℝ) : ℝ :=
 124  barrierPeriod * Cost.Jcost L
 125
 126/-- Maintenance demand is nonneg for positive extent. -/
 127theorem maintenanceDemand_nonneg {L : ℝ} (hL : 0 < L) :
 128    0 ≤ maintenanceDemand L := by
 129  unfold maintenanceDemand
 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