pith. machine review for the scientific record. sign in
theorem proved tactic proof

no_hair_field_decay

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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

proof body

Tactic-mode proof.

  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). -/

depends on (13)

Lean names referenced from this declaration's body.