noether_charge_count
plain-language theorem explainer
Recognition Science counts its canonical Noether charges as D + 1. Researchers deriving conservation laws from symmetries of the recognition action cite this count when enumerating the four charges from J-translation, sigma-translation, Z-translation and theta-rotation. The declaration is a direct definition that immediately supports the equality theorem in the same module.
Claim. The number of canonical Noether charges equals $D + 1$, where $D$ is the number of spatial dimensions.
background
The module NoetherTheoremDeep derives conservation laws from continuous symmetries of the recognition action. Four symmetries are identified: J-translation yields the recognition budget integral, sigma-translation yields baryon number, Z-translation yields complexity, and theta-rotation yields phase. This definition fixes the total count at D + 1, with D drawn from the forcing chain that sets three spatial dimensions.
proof idea
The declaration is a direct definition that sets the count equal to D + 1. No lemmas are applied and no tactics are used; the body is a one-line assignment that unfolds immediately in dependent statements.
why it matters
This definition supplies the value required by the theorem four_charges and the structure NoetherTheoremDeepCert. It completes the first item listed in the module documentation: exactly four charges equal to D + 1. It anchors the structural theorem that connects to T8 forcing of D = 3 and the four symmetries enumerated in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.