def
definition
horizonBandwidth
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Unification.BlackHoleBandwidth on GitHub at line 71.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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). -/
95theorem horizonDemand_universal {M₁ M₂ : ℝ} (h₁ : 0 < M₁) (h₂ : 0 < M₂) :
96 horizonDemand M₁ = horizonDemand M₂ := by
97 rw [horizonDemand_eq h₁, horizonDemand_eq h₂]
98
99/-! ## §4. Maximal Saturation -/
100
101/-- **THEOREM**: A black hole is maximally bandwidth-saturated.