energy_zero_at_eq
The recognition energy vanishes exactly at the equilibrium scale r = 1. Researchers establishing conservation laws from J-cost symmetries cite this when confirming the ground-state minimum in the Recognition Science action. The proof is a direct one-line reduction to the unit lemma for the J-cost function.
claimThe energy functional defined by $E(r) := J(r)$ satisfies $E(1) = 0$, where $J$ is the J-cost function obeying $J(1) = 0$.
background
The module develops Noether's theorem for the recognition action, identifying four conserved charges from the canonical symmetries: J-translation, sigma-translation, Z-translation, and theta-rotation. Energy is defined directly as the recognition budget integral via energy_RS r := Jcost r, linking the energy functional to the J-cost. The upstream Jcost_unit0 lemma states that Jcost 1 = 0 by simplification of the squared-ratio expression for J.
proof idea
One-line wrapper that applies the Jcost_unit0 lemma from the Cost module, which asserts Jcost 1 = 0.
why it matters in Recognition Science
This declaration supplies the energy-zero-at-equilibrium field required by the NoetherTheoremDeepCert structure, which also records the exact count of four charges and energy non-negativity. It closes the ground-state property for the energy = J-cost integral identification in the structural theorem for conservation laws. The result aligns with the equilibrium point on the phi-ladder where recognition budget reaches its minimum.
scope and limits
- Does not derive the explicit squared-ratio form of the J-cost function.
- Does not prove energy non-negativity for r > 0.
- Does not address time-dependent or path-dependent symmetries.
- Does not count or classify the four Noether charges.
Lean usage
example : energy_RS 1 = 0 := energy_zero_at_eqformal statement (Lean)
52theorem energy_zero_at_eq : energy_RS 1 = 0 := Jcost_unit0
proof body
53