EnergyDistribution
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.
claimAn 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 in Recognition Science
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.
scope and limits
- Does not compute the explicit integral form of the potential.
- Does not restrict the spatial support or smoothness of the density.
- Does not incorporate time dependence or relativistic corrections.
- Does not derive the numerical value of G from the phi ladder.
formal statement (Lean)
79structure EnergyDistribution where
80 density : Position → ℝ
81 density_nonneg : ∀ h, 0 ≤ density h
82
83/-- The Newtonian potential sourced by an energy distribution.
84 In weak-field RS: ∇²Φ = 4πG·ρ, where ρ = J-cost density = energy density.
85 We model the 1D version: Φ(h) = -G ∫ ρ(h') |h - h'|⁻¹ dh' (schematic).
86 For the formal proof, we axiomatize the Poisson relation. -/