addCharges
plain-language theorem explainer
The definition equips topological charges on an N-entry ledger with an addition operation by summing their integer-valued functions on configurations. Researchers modeling conservation laws from linking numbers in three dimensions would cite it when superposing independent charges such as baryon and lepton numbers. The construction directly specifies the summed value map and derives conservation from the separate invariance properties of the summands via rewriting.
Claim. Let $Q_1$ and $Q_2$ be topological charges on an $N$-entry ledger, each an integer-valued map from configurations to integers that is invariant under variational successor steps. Their sum is the topological charge whose value on any configuration $c$ equals $Q_1(c) + Q_2(c)$.
background
In the Recognition Science framework, topological charges arise as linking numbers in three spatial dimensions, providing integer-valued invariants that are automatically conserved under the variational dynamics of the ledger. The structure TopologicalCharge formalizes this as a pair consisting of a value function mapping configurations to integers and a proof that this value is invariant along variational trajectories. This module contrasts topological conservation with Noether's theorem by emphasizing that quantization and exact conservation follow from the topology of D = 3 rather than from continuous symmetries.
proof idea
The definition populates the TopologicalCharge structure by setting the value component to the pointwise sum of the two input value functions. Conservation is established by a single rewrite step that invokes the conserved property of the first charge followed by that of the second, using the additivity of integer addition.
why it matters
This definition supports the main results of the module on topological conservation laws, including the quantization of charges and the existence of exactly three independent charges at D = 3. It directly implements the claim that conservation laws originate from topological linking rather than symmetry, as stated in the module documentation for F-012. By enabling the addition of charges, it prepares the ground for constructing the full charge lattice used in particle generation and nucleosynthesis models downstream in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.