four_charges
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive explicit expressions for the individual charges Q_J, Q_σ, Q_Z, Q_Θ.
- Does not prove the conservation statements that follow from each symmetry.
- Does not treat non-canonical or higher-dimensional symmetries.
- Does not supply numerical values or particle-physics identifications beyond the module's naming.
Lean usage
have h : noether_charge_count = 4 := four_chargesformal statement (Lean)
42theorem four_charges : noether_charge_count = 4 := by unfold noether_charge_count D; norm_num
proof body
Term-mode proof.
43
44/-- Energy conservation: energy = recognition budget integral. -/