noetherTheoremDeepCert
plain-language theorem explainer
The definition constructs the master certificate NoetherTheoremDeepCert by populating its three fields with the four-charge count and the two energy properties. Researchers citing conservation laws in Recognition Science would reference this to confirm the structural result on J-cost symmetries. It is assembled as a record definition that directly references the supporting theorems for each field.
Claim. The certificate asserts that the number of Noether charges equals 4, that energy_RS(r) ≥ 0 for all r > 0, and that energy_RS(1) = 0.
background
The module derives Noether's theorem from continuous symmetries of the J-cost action, yielding four canonical charges: Q_J from J-translation, Q_σ from σ-translation (baryon number), Q_Z from Z-translation (complexity), and Q_Θ from Θ-rotation (phase). The local setting is a structural theorem with zero axioms or sorries, proving exactly four charges as D+1 with D=3 and energy as the recognition budget integral. Upstream results include four_charges proved by unfolding noether_charge_count and normalizing, energy_nonneg via Jcost_nonneg, and energy_zero_at_eq via Jcost_unit0.
proof idea
The definition is a record constructor that assigns four_charges to the theorem four_charges, energy_nonneg to energy_nonneg, and energy_zero_at_eq to energy_zero_at_eq. It is a direct one-line wrapper referencing the three supporting results.
why it matters
This supplies the master certificate NoetherTheoremDeepCert used to prove Nonempty NoetherTheoremDeepCert. It completes the module's structural theorem on the four charges from symmetries of the recognition action, consistent with the framework's T0-T8 chain and RCL. It touches the derivation of conservation laws without open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.