bandwidth_monotone

formal source

  98  bandwidth_pos hA
  99
 100/-- Bandwidth is monotone in area: larger boundary → more throughput. -/
 101theorem bandwidth_monotone {A₁ A₂ : ℝ} (_h₁ : 0 < A₁) (h : A₁ ≤ A₂) :
 102    bandwidth A₁ ≤ bandwidth A₂ := by
 103  unfold bandwidth
 104  exact div_le_div_of_nonneg_right h (le_of_lt bandwidth_denom_pos)
 105
 106/-- Bandwidth scales linearly with area. -/
 107theorem bandwidth_linear (A c : ℝ) (_hc : 0 < c) :
 108    bandwidth (c * A) = c * bandwidth A := by
 109  unfold bandwidth
 110  ring
 111
 112/-! ## §3. Holographic Capacity Recovery -/
 113
 114/-- The total holographic capacity (bits) of area A. -/
 115noncomputable def holographicBits (area : ℝ) : ℝ :=
 116  area / (4 * planckArea)
 117
 118/-- Bandwidth equals holographic bits divided by (k_R · 8τ₀). -/
 119theorem bandwidth_eq_bits_over_cost {A : ℝ} (_hA : 0 < A) :
 120    bandwidth A = holographicBits A / (k_R * eightTickCadence) := by
 121  unfold bandwidth holographicBits
 122  ring
 123
 124/-- Each recognition event within the bandwidth budget consumes k_R bits
 125    of holographic capacity per 8-tick cycle. -/
 126theorem bandwidth_times_cost_eq_rate {A : ℝ} (hA : 0 < A) :
 127    bandwidth A * (k_R * eightTickCadence) = holographicBits A := by
 128  rw [bandwidth_eq_bits_over_cost hA]
 129  have h : 0 < k_R * eightTickCadence := mul_pos k_R_pos eightTickCadence_pos
 130  exact div_mul_cancel₀ (holographicBits A) (ne_of_gt h)
 131