negCharge
plain-language theorem explainer
Negation of a topological charge Q on an N-entry ledger, defined by flipping the sign of its integer-valued map while retaining invariance under variational steps. Researchers modeling charge conjugation or signed linking numbers in D=3 topological theories would cite this construction. The definition is a direct structural wrapper that reuses the original conservation property via a single rewrite.
Claim. For any topological charge $Q$ on configurations of size $N$, the negated charge is the map $cmapsto -Q(c)$ from configurations to integers that satisfies the same invariance: if configuration $c$ is a variational successor of $c'$, then $(-Q)(c')=(-Q)(c)$.
background
TopologicalCharge is the structure whose value field is a map from Configuration N to integers and whose conserved field is a proof that this map is unchanged under any IsVariationalSuccessor step. Integer codomain supplies the quantization statement automatically. The module frames conservation as a consequence of linking numbers in three dimensions rather than continuous symmetries, with the table contrasting topological invariants (integer, deformation-invariant) against Noether charges (real-valued, symmetry-dependent).
proof idea
The definition builds a fresh TopologicalCharge instance by setting the value field to the pointwise negation of the input Q and supplying the conserved field through a rewrite that directly invokes the conserved field of the original Q.
why it matters
The construction closes the set of topological charges under sign reversal, supporting the module claim that charges behave as integer invariants arising from D=3 linking. It aligns with the framework distinction between topological and Noether conservation and with the listed main results on quantization and trajectory invariance. No downstream uses are recorded, yet the operation is a prerequisite for treating charges as an additive group in later ledger arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.