EnergyProcessingEquivalence
plain-language theorem explainer
The EnergyProcessingEquivalence structure encodes that J-cost vanishes at unit balance, is strictly positive for deviations, reproduces the weak-field kinetic energy quadratic, and that any energy distribution sources a processing field. A researcher closing the energy-to-gravity bridge in recognition-derived models would cite this packaging. The structure is defined directly from the J-cost definition and the energy_to_processing_field map.
Claim. The structure asserts four properties of the J-cost functional $J(x) = (x + x^{-1})/2 - 1$: $J(1) = 0$, $J(x) > 0$ for all $x > 0$ with $x ≠ 1$, the quadratic bridge $J(1 + ε) = ε² / (2(1 + ε))$ for $ε > -1$, and that every energy distribution $e$ with constant $G$ sources a processing field via $energy_to_processing_field(e, G)$.
background
J-cost is defined as $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$, the unique cost functional forced by the Recognition Composition Law. EnergyDistribution is the structure carrying a nonnegative density function from positions to reals, representing energy as J-cost density that sources gravity via the Newtonian potential in the weak-field limit.
proof idea
This is a bare structure definition with empty proof body. Its fields are instantiated in the companion theorem energy_processing_bridge by unfolding the Jcost definition and applying the nonnegativity result Jcost_nonneg for the cost axioms, then directly invoking the energy_to_processing_field constructor.
why it matters
The structure supplies the energy-is-processing step required by UnconditionalLevitationCert as its gap1_energy_is_processing field. It realizes the Recognition Science identity that energy equals J-cost density sourcing gravity, consistent with T5 J-uniqueness and emergence of D = 3 from the forcing chain. It leaves open the explicit superposition of processing fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.