noether_charge_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit functional form of any individual charge.
- Does not prove conservation for each symmetry.
- Does not address the mass formula or phi-ladder.
Lean usage
theorem four_charges : noether_charge_count = 4 := by unfold noether_charge_count D; norm_numformal statement (Lean)
39def noether_charge_count : ℕ := D + 1
proof body
Definition body.
40
41/-- `noether_charge_count = 4`. -/