bhEntropy

formal source

  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 -/
  79
  80/-- The gravitational recognition demand at the horizon.
  81
  82    At the Schwarzschild radius, the dynamical time is T_dyn = 4πM (light-crossing).
  83    Each Planck-mass unit requires one update per T_dyn.
  84    Demand = M / T_dyn = 1/(4π). -/
  85noncomputable def horizonDemand (M : ℝ) : ℝ :=
  86  M / (4 * Real.pi * M)
  87
  88theorem horizonDemand_eq {M : ℝ} (hM : 0 < M) :