energy_creates_processing_gradient
plain-language theorem explainer
Energy distributions whose density has a non-zero gradient at a point induce a non-zero gradient in the processing field obtained by scaling that density by a nonzero effective constant. Researchers modeling the emergence of weak-field gravity from J-cost in Recognition Science cite the result to connect energy concentrations directly to nontrivial processing potentials. The proof reduces the claim to the product rule for derivatives followed by the algebraic fact that a nonzero scalar times a nonzero number is nonzero.
Claim. Let $ρ : ℝ → ℝ$ be nonnegative. For $G_ eff ≠ 0$ and $h_0 ∈ ℝ$ such that $ρ$ is differentiable at $h_0$ with $ρ'(h_0) ≠ 0$, the function $ϕ(h) := G_ eff ⋅ ρ(h)$ satisfies $ϕ'(h_0) ≠ 0$.
background
EnergyDistribution packages a density function from Position (≡ ℝ) to nonnegative reals; the accompanying doc-comment identifies this density with J-cost density, which sources gravity via the identity T⁰⁰ = J-cost density from EFE emergence. The sibling definition energy_to_processing_field constructs a ProcessingField whose potential is exactly the scaled density: ϕ(h) := G_eff ⋅ energy.density(h). The module EnergyProcessingBridge situates these objects inside the Recognition Science treatment of energy-to-gravity links in the weak-field regime.
proof idea
The tactic proof first simplifies the definition of energy_to_processing_field. It then applies the lemma deriv_const_mul to obtain deriv(G_eff ⋅ density) = G_eff ⋅ deriv(density) at h0, rewrites the goal, and finishes with mul_ne_zero using the two nonzero hypotheses.
why it matters
The theorem is invoked by the downstream result energy_distribution_creates_gravity_modifier, whose doc-comment describes it as the key bridge: energy → processing → gravitational modification. It thereby supplies the local analytic step required to show that nonzero energy gradients produce processing gradients capable of opposing gravity, consistent with the framework identification of energy density as the source term in the Newtonian potential.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.