energy_creates_processing_gradient
plain-language theorem explainer
Any energy distribution whose density function has a non-zero derivative at a point induces a non-zero derivative in the associated processing field whenever the effective gravitational constant is non-zero. Workers modeling weak-field gravity as sourced by J-cost densities would cite this when connecting energy concentrations to processing gradients. The proof is a short tactic sequence that reduces the claim to the constant-multiple derivative rule followed by the algebraic fact that a non-zero scalar times a non-zero value is non-zero.
Claim. Let $ρ : ℝ → ℝ$ be the density of an energy distribution (non-negative by definition). For $G_{eff} ≠ 0$ and point $h_0$ at which $ρ$ is differentiable with $ρ'(h_0) ≠ 0$, the processing field defined by $ϕ(h) := G_{eff} ⋅ ρ(h)$ satisfies $ϕ'(h_0) ≠ 0$.
background
EnergyDistribution is the structure whose density field maps Position (≡ ℝ) to ℝ and is required to be non-negative; the doc-comment states that in RS this density is J-cost and equals the T⁰⁰ source of gravity. The sibling definition energy_to_processing_field constructs the ProcessingField whose phi component is exactly the scaled density $G_{eff} ⋅$ density(h). The module EnergyProcessingBridge sits between CoherenceFall (which supplies Position) and downstream gravity-modifier theorems; it imports RSNativeUnits.Energy (≡ ℝ) and CrystalStructure.Structure only for module context.
proof idea
The tactic proof begins with simp only [energy_to_processing_field] to unfold the definition of phi. It then applies the lemma deriv_const_mul to obtain deriv (G_eff ⋅ density) = G_eff ⋅ deriv density, rewrites the goal, and finishes with mul_ne_zero on the two non-zero hypotheses.
why it matters
The theorem is used directly by the sibling energy_distribution_creates_gravity_modifier, which lifts the non-zero gradient into an existential statement about a processing field that can oppose gravity. It supplies the elementary link in the energy-to-processing-to-gravity chain inside the Recognition framework, where energy is identified with J-cost density and the weak-field Poisson relation is axiomatized; the result therefore supports the emergence of gravitational effects from the Recognition Composition Law without additional postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.