phiRung

formal source

 214/-- Every positive mass has a unique decomposition on the φ-ladder:
 215    M = M₀ · φ^r for some reference mass M₀ and rung r ∈ ℝ.
 216    The rung is r = log_φ(M/M₀) = ln(M/M₀) / ln(φ). -/
 217noncomputable def phiRung (M M₀ : ℝ) : ℝ :=
 218  Real.log (M / M₀) / Real.log phi
 219
 220/-- The φ-rung recovers the mass: M₀ · φ^(phiRung M M₀) = M. -/
 221theorem phi_ladder_recovery (M M₀ : ℝ) (hM : 0 < M) (hM₀ : 0 < M₀) :
 222    M₀ * phi ^ (phiRung M M₀) = M := by
 223  unfold phiRung
 224  have hlog_phi : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
 225  rw [Real.rpow_def_of_pos phi_pos]
 226  rw [show Real.log phi * (Real.log (M / M₀) / Real.log phi) =
 227      Real.log (M / M₀) from by field_simp]
 228  rw [Real.exp_log (div_pos hM hM₀)]
 229  field_simp
 230
 231/-! ## Theorem 6: Cosmic Censorship Is Automatic -/
 232
 233/-- In RS, there are no singularities to censor. The Weak Cosmic Censorship
 234    Conjecture is trivially satisfied because J(x) is finite for all x > 0,
 235    and x = 0 is excluded by the derived Meta-Principle (J(0⁺) → ∞). -/
 236theorem cosmic_censorship_automatic (x : ℝ) (hx : 0 < x) :
 237    0 ≤ Jcost x ∧ Jcost x = (x - 1) ^ 2 / (2 * x) := by
 238  exact ⟨Jcost_nonneg hx, Jcost_eq_sq (ne_of_gt hx)⟩
 239
 240/-- For any x ∈ [a, B] with a > 0, J-cost is bounded above.
 241    The BH interior at any finite region has finite recognition cost. -/
 242theorem bh_interior_finite_cost (x a B : ℝ) (ha : 0 < a) (hax : a ≤ x)
 243    (hxB : x ≤ B) :
 244    Jcost x ≤ (B + a⁻¹) / 2 := by
 245  unfold Jcost
 246  have hx_pos : 0 < x := lt_of_lt_of_le ha hax
 247  have hxinv_le : x⁻¹ ≤ a⁻¹ := by