barrierPeriod_pos

formal source

  69/-- The barrier period in RS time units (τ₀ = 1). -/
  70noncomputable def barrierPeriod : ℝ := (barrierTicks : ℝ) * τ₀
  71
  72theorem barrierPeriod_pos : 0 < barrierPeriod := by
  73  unfold barrierPeriod τ₀ tick barrierTicks
  74  norm_num
  75
  76theorem barrierPeriod_eq : barrierPeriod = 360 := by
  77  unfold barrierPeriod τ₀ tick barrierTicks
  78  norm_num
  79
  80/-! ## §2. Boundary Area Model -/
  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) -/