boundaryArea

formal source

  81
  82/-- Boundary area as a function of extent (spherical boundary).
  83    A(L) = 4πL². -/
  84noncomputable def boundaryArea (L : ℝ) : ℝ := 4 * Real.pi * L ^ 2
  85
  86theorem boundaryArea_pos {L : ℝ} (hL : 0 < L) : 0 < boundaryArea L := by
  87  unfold boundaryArea
  88  exact mul_pos (mul_pos (by linarith) Real.pi_pos) (sq_pos_of_pos hL)
  89
  90theorem boundaryArea_monotone {L₁ L₂ : ℝ} (h₁ : 0 < L₁) (h : L₁ ≤ L₂) :
  91    boundaryArea L₁ ≤ boundaryArea L₂ := by
  92  unfold boundaryArea
  93  apply mul_le_mul_of_nonneg_left
  94  · exact sq_le_sq' (by linarith) h
  95  · exact mul_nonneg (by linarith) (le_of_lt Real.pi_pos)
  96
  97/-! ## §3. Holographic Maintenance Budget -/
  98
  99/-- Maximum recognition events available over the barrier period
 100    for a boundary of extent L:
 101
 102        N_budget(L) = boundaryArea(L) / (4ℓ_P² · k_R) -/
 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