four_charges
plain-language theorem explainer
The theorem asserts that the number of canonical Noether charges equals four. Researchers assembling the structural certificate for conservation laws from J-cost symmetries would cite this result when verifying the count of charges arising from the four canonical symmetries. The proof is a one-line wrapper that unfolds the charge-count definition and normalizes the arithmetic.
Claim. The number of canonical Noether charges equals four, where the count is defined as the spatial dimension plus one.
background
In the Recognition Science setting the J-cost functional supplies the recognition budget whose continuous symmetries generate conserved charges. The module lists four such charges: the integral of J under time translation, baryon number from σ-translation, complexity from Z-translation, and phase from Θ-rotation. The upstream definition sets the charge count to D + 1 with D the spatial dimension fixed at three by the eight-tick octave construction.
proof idea
The proof is a one-line wrapper that unfolds the definition of noether_charge_count (which expands to D + 1) and applies numerical normalization to obtain the value 4.
why it matters
This supplies the four_charges field of the NoetherTheoremDeepCert structure, which also records non-negativity and equilibrium vanishing of the energy functional. It completes the first item in the module's enumerated list of structural results and confirms that the four symmetries predicted by the J-cost action and D = 3 yield exactly four charges. The certificate is referenced by the master deep-Noether theorem in the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.