EnergyDistribution

formal source

  76/-- An energy distribution over space creates a processing field.
  77    In RS, energy IS J-cost, and J-cost IS the processing potential that sources gravity.
  78    This is the identity T⁰⁰ = J-cost density from EFE emergence. -/
  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. -/
  87def energy_to_processing_field (energy : EnergyDistribution) (G_eff : ℝ) : ProcessingField where
  88  phi h := G_eff * energy.density h
  89
  90/-- ANY energy concentration creates a non-trivial processing field.
  91    If the energy density has a non-zero gradient at some point,
  92    then the processing field has a non-zero gradient there. -/
  93theorem energy_creates_processing_gradient
  94    (energy : EnergyDistribution) (G_eff : ℝ) (hG : G_eff ≠ 0)
  95    (h0 : Position)
  96    (h_diff : DifferentiableAt ℝ energy.density h0)
  97    (h_grad : deriv energy.density h0 ≠ 0) :
  98    deriv (energy_to_processing_field energy G_eff).phi h0 ≠ 0 := by
  99  simp only [energy_to_processing_field]
 100  have : deriv (fun h => G_eff * energy.density h) h0 = G_eff * deriv energy.density h0 := by
 101    exact deriv_const_mul G_eff h_diff
 102  rw [this]
 103  exact mul_ne_zero hG h_grad
 104
 105/-! ## 3. The Bridge: Any Energy Source Gravitates -/
 106
 107/-- Structure packaging the energy-processing equivalence. -/
 108structure EnergyProcessingEquivalence where
 109  /-- J-cost at balance is zero (existence is free) -/