constCharge
plain-language theorem explainer
A definition constructing a topological charge that assigns the fixed integer n to every configuration of an N-entry ledger. Researchers modeling quantized conservation from topology would cite it to exhibit trivial conserved quantities. The definition is a direct structure instantiation whose invariance clause holds by reflexivity.
Claim. Let TopologicalCharge$_N$ denote the structure of maps $v$ from configurations of an $N$-entry ledger to integers such that $v$ is invariant under any variational successor step. The constant charge of value $n$ is the element of this structure whose map sends every configuration to the integer $n$.
background
The TopologicalConservation module formalizes conservation laws as topological invariants arising from linking in three spatial dimensions rather than from continuous symmetries. A topological charge on an $N$-entry ledger is an integer-valued function on configurations that remains unchanged whenever one configuration is a variational successor of another; integer-valuedness supplies the quantization automatically from the codomain.
proof idea
The definition populates the two fields of the TopologicalCharge structure by setting the value map to the constant function returning $n$ and discharging the invariance requirement by reflexivity of equality.
why it matters
This supplies the constant-charge example among the sibling definitions that illustrate quantized topological charges and feed the module's main results on charge count in dimension 3. It supports the F-012 claim that conservation originates from linking numbers rather than Noether symmetries, consistent with the eight-tick octave and $D=3$ forcing in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.