zeroCharge
The zero topological charge supplies the constant integer function zero on configurations of any ledger size N. It serves as the base case for the family of topological charges in Recognition Science. The definition constructs the required structure directly by setting the value map to zero and confirming invariance via reflexivity on the successor relation.
claimThe zero topological charge on an $N$-entry ledger is the integer-valued function that maps every configuration to 0 and remains invariant under any variational successor step.
background
TopologicalCharge is a structure on an $N$-entry ledger consisting of an integer-valued function on configurations that remains invariant under the variational dynamics: if one configuration is a variational successor of another then their charges agree. This encodes the claim that conservation laws originate in topological invariants rather than continuous symmetries. The module TopologicalConservation formalizes that in three spatial dimensions linking numbers provide quantized charges such as baryon and lepton numbers which cannot change under continuous deformations of the ledger. Upstream results include the definition of the active edge count A and the actualization operator which together ensure the variational dynamics are well-defined.
proof idea
This is a direct definition that constructs the TopologicalCharge structure by supplying the constant-zero value function and proving conservation via the reflexivity tactic on the equality of integers.
why it matters in Recognition Science
This definition supplies the trivial element in the space of topological charges serving as the zero element for the additive structure implicit in the conservation laws of the Recognition framework. It anchors the results on charge quantization and the existence of exactly three independent charges at D=3. The module distinguishes topological conservation from Noether's theorem by emphasizing integer values arising from linking in three dimensions.
scope and limits
- Does not assert the existence of non-zero charges.
- Does not derive charges from linking numbers.
- Does not restrict to D=3.
- Does not apply outside the variational dynamics of the ledger.
formal statement (Lean)
94def zeroCharge (N : ℕ) : TopologicalCharge N where
95 value := fun _ => 0
proof body
Definition body.
96 conserved := fun _ _ _ => rfl
97
98/-- A constant topological charge. -/