theorem proved term proof

`hair_cost_nonneg`

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

formal statement (Lean)

  45theorem hair_cost_nonneg (amplitude : ℝ) (h : |amplitude| ≤ 1/2) :
  46    0 ≤ hair_cost amplitude := by

proof body

Term-mode proof.

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

depends on (10)

Lean names referenced from this declaration's body.

Jcost_nonneg in IndisputableMonolith.Cost decl_use
Jcost_nonneg in IndisputableMonolith.Cost.JcostCore decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
Jcost_nonneg in IndisputableMonolith.Gravity.CoherenceCollapse decl_use
Jcost_nonneg in IndisputableMonolith.Gravity.EnergyProcessingBridge decl_use
Jcost_nonneg in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
hair_cost in IndisputableMonolith.Physics.NoHairTheorem decl_use
amplitude in IndisputableMonolith.QFT.SMatrixUnitarity decl_use
amplitude in IndisputableMonolith.Quantum.DoubleSlit decl_use