energy_creates_processing_gradient
plain-language theorem explainer
Energy distributions with non-zero density gradients induce non-zero gradients in the associated processing field. Physicists modeling weak-field gravity via J-cost in Recognition Science cite this to connect energy concentrations directly to gravitational sourcing. The tactic proof unfolds the linear definition of the processing field, applies the constant-multiple derivative rule, and concludes via the non-zero product lemma.
Claim. Let $ρ : ℝ → ℝ$ be the density function of an energy distribution. For $G_{eff} ≠ 0$ and position $h_0$ where $ρ$ is differentiable with $ρ'(h_0) ≠ 0$, the processing field $Φ(h) = G_{eff} ⋅ ρ(h)$ satisfies $Φ'(h_0) ≠ 0$.
background
EnergyDistribution is a structure carrying a non-negative density function from Position (the reals) to the reals, identified with J-cost density. The definition energy_to_processing_field constructs the processing field by direct scaling: phi(h) := G_eff * density(h). This models the weak-field Newtonian potential in one dimension, where the Poisson relation is axiomatized rather than derived. Position and Energy are reals in RS-native units; the result depends on differentiability from Mathlib and the upstream density structure.
proof idea
The tactic proof begins by simp-unfolding energy_to_processing_field to expose the linear scaling. It then applies the lemma deriv_const_mul to obtain deriv(G_eff * density) = G_eff * deriv(density). A rewrite step reduces the goal to showing the product is non-zero, which follows immediately from mul_ne_zero using the supplied hypotheses hG and h_grad.
why it matters
This theorem supplies the direct link from energy density gradients to non-trivial processing fields inside the EnergyProcessingBridge module. It is invoked by the downstream result energy_distribution_creates_gravity_modifier, which lifts the gradient non-vanishing to an opposing gravitational modification. In the Recognition Science setting it realizes the T⁰⁰ = J-cost density identity that lets energy concentrations source gravity through the processing potential in the weak-field limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.