energy_RS
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive an integral form for total conserved energy.
- Does not prove non-negativity or vanishing at equilibrium.
- Does not establish the count of four charges or other symmetries.
- Does not reference specific RS constants such as phi or the alpha band.
Lean usage
theorem energy_nonneg (r : ℝ) (hr : 0 < r) : 0 ≤ energy_RS r := Jcost_nonneg hrformal statement (Lean)
45def energy_RS (r : ℝ) : ℝ := Jcost r
proof body
Definition body.
46
47/-- Energy ≥ 0. -/