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

energy_distribution_creates_gravity_modifier

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)

 137theorem energy_distribution_creates_gravity_modifier
 138    (energy : EnergyDistribution) (G_eff : ℝ) (hG : 0 < G_eff)
 139    (h0 : Position)
 140    (h_diff : DifferentiableAt ℝ energy.density h0)
 141    (h_grad : deriv energy.density h0 ≠ 0) :
 142    ∃ pf : ProcessingField,
 143      pf = energy_to_processing_field energy G_eff ∧
 144      deriv pf.phi h0 ≠ 0 := by

proof body

Term-mode proof.

 145  exact ⟨energy_to_processing_field energy G_eff, rfl,
 146    energy_creates_processing_gradient energy G_eff (ne_of_gt hG) h0 h_diff h_grad⟩
 147
 148end IndisputableMonolith.Gravity.EnergyProcessingBridge

depends on (6)

Lean names referenced from this declaration's body.