hair_cost

formal source

  38
  39/-- A "hair" field mode at radius r carries positive J-cost.
  40    This is the RS mechanism for hair decay. -/
  41noncomputable def hair_cost (field_amplitude : ℝ) : ℝ :=
  42  Jcost (1 + field_amplitude)
  43
  44/-- Hair cost is non-negative. -/
  45theorem hair_cost_nonneg (amplitude : ℝ) (h : |amplitude| ≤ 1/2) :
  46    0 ≤ hair_cost amplitude := by
  47  unfold hair_cost
  48  apply Jcost_nonneg
  49  have := (abs_le.mp h).1
  50  linarith
  51
  52/-- Hair cost vanishes only when amplitude = 0 (no hair). -/
  53theorem hair_cost_zero_iff (amplitude : ℝ) (hpos : 0 < 1 + amplitude) :
  54    hair_cost amplitude = 0 ↔ amplitude = 0 := by
  55  unfold hair_cost
  56  constructor
  57  · intro h
  58    have hne : (1 + amplitude) ≠ 0 := ne_of_gt hpos
  59    rw [Jcost_eq_sq hne] at h
  60    have hnum : (1 + amplitude - 1)^2 = 0 := by
  61      have hden : (0 : ℝ) < 2 * (1 + amplitude) := by linarith
  62      exact (div_eq_zero_iff.mp h).resolve_right (ne_of_gt hden)
  63    have : amplitude ^ 2 = 0 := by linarith [hnum]
  64    exact pow_eq_zero_iff (n := 2) (by norm_num) |>.mp this
  65  · intro h; simp [h, Jcost_unit0]
  66
  67/-! ## No-Hair Theorem -/
  68
  69/-- **NO-HAIR THEOREM** (structural version):
  70    Any field perturbation δs that encodes classical information
  71    beyond (M, Q, J) has positive J-cost at the horizon and must decay.