schwarzschildRadius

formal source

  45/-! ## §1. Black Hole Parameters (RS-native: G=1, ℓ_P=1, c=1) -/
  46
  47/-- Schwarzschild radius in RS-native units: r_s = 2M. -/
  48noncomputable def schwarzschildRadius (M : ℝ) : ℝ := 2 * M
  49
  50/-- Horizon area: A = 4π r_s² = 16πM². -/
  51noncomputable def horizonArea (M : ℝ) : ℝ := 16 * Real.pi * M ^ 2
  52
  53theorem horizonArea_pos {M : ℝ} (hM : 0 < M) : 0 < horizonArea M := by
  54  unfold horizonArea
  55  exact mul_pos (mul_pos (by linarith) Real.pi_pos) (sq_pos_of_pos hM)
  56
  57/-- Bekenstein-Hawking entropy: S_BH = A/(4ℓ_P²) = 4πM² (with ℓ_P = 1). -/
  58noncomputable def bhEntropy (M : ℝ) : ℝ := horizonArea M / 4
  59
  60theorem bhEntropy_eq (M : ℝ) : bhEntropy M = 4 * Real.pi * M ^ 2 := by
  61  unfold bhEntropy horizonArea
  62  ring
  63
  64theorem bhEntropy_pos {M : ℝ} (hM : 0 < M) : 0 < bhEntropy M := by
  65  rw [bhEntropy_eq]
  66  exact mul_pos (mul_pos (by linarith) Real.pi_pos) (sq_pos_of_pos hM)
  67
  68/-! ## §2. Horizon Bandwidth -/
  69
  70/-- Recognition bandwidth at the horizon: total holographic bits / (k_R · 8τ₀). -/
  71noncomputable def horizonBandwidth (M : ℝ) : ℝ :=
  72  bhEntropy M / (k_R * eightTickCadence)
  73
  74theorem horizonBandwidth_pos {M : ℝ} (hM : 0 < M) : 0 < horizonBandwidth M := by
  75  unfold horizonBandwidth
  76  exact div_pos (bhEntropy_pos hM) (mul_pos k_R_pos eightTickCadence_pos)
  77
  78/-! ## §3. Gravitational Demand at Horizon -/