noetherTheoremDeepCert_inhabited
plain-language theorem explainer
The declaration proves existence of the master certificate for the deep Noether theorem by direct construction. A researcher deriving conserved charges from J-cost symmetries would cite it to invoke the packaged properties on charge count and energy. The proof is a one-line term that supplies the pre-built certificate definition.
Claim. The record type $NoetherTheoremDeepCert$ is inhabited, where $NoetherTheoremDeepCert$ asserts that the number of Noether charges equals 4, that the recognition-science energy satisfies $0 < r → 0 ≤ energy_{RS}(r)$ for all real $r$, and that $energy_{RS}(1) = 0$.
background
The module realizes Noether's theorem via continuous symmetries of the J-cost action, producing four conserved charges: J-translation charge, baryon number $Q_σ$, complexity $Q_Z$, and phase $Q_Θ$. These arise as the canonical charges of the recognition action in RS-native units where $c=1$ and $hbar=phi^{-5}$ (MODULE_DOC). The certificate structure packages three concrete properties that together certify the structural theorem with zero axioms or sorries.
proof idea
The proof is a one-line term that applies the Nonempty constructor to the explicit definition noetherTheoremDeepCert. That definition in turn assembles the three fields directly from the sibling lemmas four_charges, energy_nonneg, and energy_zero_at_eq.
why it matters
This supplies the master certificate NoetherTheoremDeepCert that certifies the deep Noether theorem in the foundation layer. It closes the structural claims on four charges and energy non-negativity before any downstream use of individual charges such as energy from time translation. The result sits inside the Recognition Science derivation of conservation laws from J-cost symmetries and the four canonical Noether charges listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.