EnergyDistribution
plain-language theorem explainer
An energy distribution is a non-negative real function on positions that encodes J-cost density as the source for gravitational processing fields. Gravity modelers in Recognition Science cite this when deriving Newtonian potentials from recognition events. The declaration is a direct structure with a density map and non-negativity constraint.
Claim. An energy distribution is a map $ρ: ℝ → ℝ$ with $ρ(h) ≥ 0$ for all positions $h$, where $ρ$ is the J-cost density that sources the Newtonian potential via $∇²Φ = 4πG ρ$.
background
J-cost is the recognition cost of a state deviation from unity, defined as $J(x) = (x + x^{-1})/2 - 1$. Positions come from the CoherenceFall module as the spatial domain. The structure packages density together with its non-negativity to act as the T^{00} source term in the energy-processing bridge.
proof idea
Direct structure definition. It introduces the density field and attaches the non-negativity axiom as a field; no lemmas or tactics are invoked.
why it matters
This supplies the energy-density input to downstream results energy_creates_processing_gradient and energy_distribution_creates_gravity_modifier. It encodes the identity that energy equals J-cost density, which sources gravity in the Recognition framework. It sits at the T8 step where spatial dimensions and the gravitational constant G (derived as phi^5 / pi in native units) enter the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.