zeroCharge
plain-language theorem explainer
The zeroCharge definition supplies the trivial topological charge on an N-entry ledger by mapping every configuration to the integer zero. Researchers constructing the charge sector in the Recognition Science ledger would cite it as the baseline case when enumerating conserved linking numbers. It is realized by a direct definition that populates the value field with the constant-zero function and discharges the conservation requirement by reflexivity.
Claim. For any natural number $N$, the zero topological charge is the structure whose value map sends every configuration of the $N$-entry ledger to the integer $0$ and whose conservation clause holds identically under any variational successor relation.
background
TopologicalCharge is the structure whose fields are an integer-valued map from configurations to ℤ together with a proof that the map is invariant under IsVariationalSuccessor steps. Integer codomain supplies the automatic quantization of charge. The module sets this structure inside the claim that conservation originates from topological linking in D=3 rather than from continuous symmetries.
proof idea
Direct definition that instantiates the TopologicalCharge structure. The value field is the constant function returning 0. The conserved field is witnessed by a lambda abstraction that returns reflexivity on any pair of configurations related by a variational successor.
why it matters
This definition anchors the trivial sector inside F-012, the registry item on the topological origin of conservation laws. It supplies the zero element against which non-trivial linking numbers (baryon and lepton charges) are later contrasted. The surrounding module uses it to separate topological conservation, which is integer-valued and deformation-invariant, from Noether charges that need not be quantized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.