energy_distribution_creates_gravity_modifier
plain-language theorem explainer
An energy distribution whose density has nonzero derivative at h0 induces a processing field with nonzero gradient at the same point. Researchers deriving weak-field gravity from J-cost densities would cite this as the explicit energy-to-processing link. The proof is a term-mode wrapper that applies the gradient-creation lemma to the explicit definition of the processing field.
Claim. Let $E$ be an energy distribution with nonnegative density function $rho: Position to real numbers$, where $Position = real$. Suppose $rho$ is differentiable at $h_0$ with $rho'(h_0) neq 0$ and $G_eff > 0$. Then the processing field defined by $Phi(h) = G_eff cdot rho(h)$ satisfies $Phi'(h_0) neq 0$.
background
Position is the real line. EnergyDistribution is the structure carrying a nonnegative density function from Position to reals; its doc-comment states that energy is J-cost and J-cost is the processing potential sourcing gravity, realizing the identity T00 equals J-cost density. ProcessingField is the structure whose phi component is the potential function. The map energy_to_processing_field sets phi(h) explicitly to G_eff times density(h). The upstream theorem energy_creates_processing_gradient states that any energy concentration with nonzero density gradient at a point produces a nonzero processing gradient there.
proof idea
The proof is a term-mode application of energy_creates_processing_gradient to the supplied energy distribution, G_eff, position, differentiability hypothesis, and nonzero gradient hypothesis, followed by reflexivity to equate the processing field with the image under energy_to_processing_field.
why it matters
This theorem supplies the direct bridge from energy distributions to processing fields inside the Gravity.EnergyProcessingBridge module. It realizes the doc-comment claim that energy creates a processing field whose gradient can oppose gravity, supporting the emergence of Newtonian gravity from Recognition Science J-cost axioms. The result sits immediately downstream of energy_to_processing_field and energy_creates_processing_gradient; no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.