zeroCharge
plain-language theorem explainer
The definition supplies the trivial topological charge that assigns zero to every configuration on an N-entry ledger. Researchers working on charge quantization in Recognition Science would cite it as the base case for conserved quantities arising from topology. The definition is a direct construction that satisfies the conserved predicate by reflexivity.
Claim. The trivial topological charge on an $N$-entry ledger is the map sending every configuration to the integer zero, which remains invariant under variational dynamics by reflexivity.
background
A topological charge on an $N$-entry ledger is an integer-valued function of the configuration that is invariant under the variational dynamics. Integer-valuedness is the formal content of charge quantization; it is structural, not imposed. The module formalizes the claim that conservation laws arise from topology (linking in $D=3$), not from continuous symmetries.
proof idea
The definition constructs the structure by setting the value field to the constant zero function and the conserved field to a reflexivity proof on the variational successor relation.
why it matters
This definition supplies the trivial instance in the module that derives conservation from topological linking numbers rather than Noether symmetries. It supports the registry item F-012 on the origin of conservation laws in the ledger and the distinction that topological charges are integer-valued and cannot change under continuous deformation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.