energy_creates_processing_gradient

formal source

  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) -/
 110  balance_zero_cost : Jcost 1 = 0
 111  /-- J-cost away from balance is positive (deviation costs) -/
 112  deviation_positive_cost : ∀ x : ℝ, 0 < x → x ≠ 1 → 0 < Jcost x
 113  /-- J-cost matches kinetic energy in weak field: J(1+ε) = ε²/(2(1+ε)) -/
 114  quadratic_energy_bridge : ∀ ε : ℝ, -1 < ε →
 115    Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε))
 116  /-- Energy creates processing field -/
 117  energy_sources_processing : ∀ (e : EnergyDistribution) (G : ℝ),
 118    ∃ pf : ProcessingField, pf = energy_to_processing_field e G
 119
 120/-- The energy-processing bridge is proved from RS first principles. -/
 121theorem energy_processing_bridge : EnergyProcessingEquivalence where
 122  balance_zero_cost := by unfold Jcost; simp
 123  deviation_positive_cost := by