bandwidth_linear

formal source

 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
 132/-! ## §4. Connection to ILG Parameters -/
 133
 134/-- ILG coherence energy C_lag = φ⁻⁵ equals the coherence exponent E_coh.
 135    This is the energy quantum per recognition event in RS-native units. -/
 136theorem Clag_eq_phi_neg5 : Clag = 1 / phi ^ (5 : ℕ) := by
 137  unfold Clag