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

energy_creates_processing_gradient

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)

  93theorem energy_creates_processing_gradient
  94    (energy : EnergyDistribution) (G_eff : ℝ) (hG : G_eff ≠ 0)
  95    (h0 : Position)
  96    (h_diff : DifferentiableAt ℝ energy.density h0)
  97    (h_grad : deriv energy.density h0 ≠ 0) :
  98    deriv (energy_to_processing_field energy G_eff).phi h0 ≠ 0 := by

proof body

Tactic-mode proof.

  99  simp only [energy_to_processing_field]
 100  have : deriv (fun h => G_eff * energy.density h) h0 = G_eff * deriv energy.density h0 := by
 101    exact deriv_const_mul G_eff h_diff
 102  rw [this]
 103  exact mul_ne_zero hG h_grad
 104
 105/-! ## 3. The Bridge: Any Energy Source Gravitates -/
 106
 107/-- Structure packaging the energy-processing equivalence. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.