pith. machine review for the scientific record. sign in
structure definition def or abbrev

EnergyProcessingEquivalence

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.