121theorem energy_processing_bridge : EnergyProcessingEquivalence where 122 balance_zero_cost := by unfold Jcost; simp
proof body
Tactic-mode proof.
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. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.