`energy_distribution_creates_gravity_modifier`

proved

show as: view math explainer →

module: IndisputableMonolith.Gravity.EnergyProcessingBridge
domain: Gravity
line: 137 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gravity.EnergyProcessingBridge on GitHub at line 137.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 134/-- An energy distribution with non-zero gradient at position h₀ creates a
 135    non-trivial processing field whose gradient can oppose gravity.
 136    This is the key bridge: energy → processing → gravitational modification. -/
 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
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.