bhEntropy_pos

formal source

  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) :
  89    horizonDemand M = 1 / (4 * Real.pi) := by
  90  unfold horizonDemand
  91  have hM0 : M ≠ 0 := ne_of_gt hM
  92  field_simp
  93
  94/-- Horizon demand is mass-independent (universal). -/