energy_processing_bridge

formal source

 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
 124    intro x hx hx1
 125    have h := Jcost_nonneg x hx
 126    rcases eq_or_lt_of_le h with h_eq | h_pos
 127    · exfalso; exact hx1 ((Jcost_zero_iff_one x hx).mp h_eq.symm)
 128    · exact h_pos
 129  quadratic_energy_bridge := Jcost_one_plus_exact
 130  energy_sources_processing := fun e G => ⟨energy_to_processing_field e G, rfl⟩
 131
 132/-! ## 4. Consequence: Any Energy Source Creates a Processing Field -/
 133
 134/-- An energy distribution with non-zero gradient at position h₀ creates a
 135    non-trivial processing field whose gradient can oppose gravity.
 136    This is the key bridge: energy → processing → gravitational modification. -/
 137theorem energy_distribution_creates_gravity_modifier
 138    (energy : EnergyDistribution) (G_eff : ℝ) (hG : 0 < G_eff)
 139    (h0 : Position)
 140    (h_diff : DifferentiableAt ℝ energy.density h0)
 141    (h_grad : deriv energy.density h0 ≠ 0) :
 142    ∃ pf : ProcessingField,
 143      pf = energy_to_processing_field energy G_eff ∧
 144      deriv pf.phi h0 ≠ 0 := by
 145  exact ⟨energy_to_processing_field energy G_eff, rfl,
 146    energy_creates_processing_gradient energy G_eff (ne_of_gt hG) h0 h_diff h_grad⟩
 147
 148end IndisputableMonolith.Gravity.EnergyProcessingBridge