energy_RS
plain-language theorem explainer
energy_RS identifies the recognition energy in RS with the J-cost evaluated at a real parameter r. It is cited when establishing energy non-negativity and the master certificate for Noether conservation laws. The definition is a direct abbreviation to the Jcost function imported from the Cost module.
Claim. For a real parameter $r$, the RS energy is defined by $E(r) := J(r)$, where $J$ denotes the J-cost function that encodes the recognition budget.
background
The NoetherTheoremDeep module derives conservation laws from symmetries of the J-cost action. It lists four canonical charges: Q_J from J-translation (the recognition budget integral), Q_σ as baryon number, Q_Z as complexity, and Q_Θ as phase. Energy is obtained specifically from time-translation symmetry as the J-cost integral, here realized pointwise.
proof idea
This is a one-line definition that directly equates energy_RS r to Jcost r. No lemmas or tactics are invoked beyond the abbreviation itself.
why it matters
The definition supplies the energy field inside the NoetherTheoremDeepCert structure, which also records the count of four charges together with non-negativity and zero-at-equilibrium properties. It fills the energy_from_time_translation step stated in the module documentation and grounds the conserved charge arising from time symmetry in the J-cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.