no_hair_field_decay

formal source

  74    1. Conserved charges (M,Q,J) are protected by Noether currents.
  75    2. All other field modes have positive J-cost.
  76    3. J-cost minimization forces all non-conserved modes to zero. -/
  77theorem no_hair_field_decay
  78    (hair_amplitude : ℝ)
  79    (h_nonzero : hair_amplitude ≠ 0)
  80    (hpos : 0 < 1 + hair_amplitude) :
  81    0 < hair_cost hair_amplitude := by
  82  have h_nonneg : 0 ≤ hair_cost hair_amplitude := by
  83    unfold hair_cost; exact Jcost_nonneg hpos
  84  have h_ne : hair_cost hair_amplitude ≠ 0 := by
  85    intro h_eq; exact h_nonzero ((hair_cost_zero_iff hair_amplitude hpos).mp h_eq)
  86  exact lt_of_le_of_ne h_nonneg (Ne.symm h_ne)
  87
  88/-- **KEY UNIQUENESS THEOREM**:
  89    Two black hole states with the same (M, Q, J) have the same J-cost,
  90    and thus the same physical state (by J-cost uniqueness). -/
  91theorem bh_state_determined_by_charges (s₁ s₂ : BHState) :
  92    s₁.mass = s₂.mass →
  93    s₁.charge = s₂.charge →
  94    s₁.angular_momentum = s₂.angular_momentum →
  95    s₁ = s₂ := by
  96  intro hM hQ hJ
  97  cases s₁; cases s₂
  98  simp_all
  99
 100/-- **THREE CHARGES ONLY**:
 101    The RS framework has exactly three independent asymptotic symmetries
 102    for an asymptotically flat spacetime in D=3+1 dimensions:
 103    - Time translation → energy/mass M
 104    - U(1) gauge → charge Q
 105    - SO(3) rotation → angular momentum J
 106
 107    All other would-be symmetries are either broken or non-compact. -/