topological_charge_quantized
plain-language theorem explainer
Every topological charge on an N-entry ledger evaluates to an integer at any configuration. Researchers deriving conservation from topology in Recognition Science cite this to establish quantization as structural. The proof is a one-line term that uses the codomain of the value map being the integers.
Claim. For every natural number $N$, every topological charge $Q$ on configurations of size $N$, and every configuration $c$, there exists an integer $n$ such that the value of $Q$ at $c$ equals $n$.
background
The TopologicalConservation module derives conservation from topological linking in D=3 rather than Noether symmetries. A configuration is a structure of N positive real ledger entries. A topological charge is a structure whose value map sends configurations to integers and whose conserved field requires invariance under variational successors.
proof idea
The proof is a one-line term proof. It supplies the witness Q.value c directly from the structure definition and closes the existential with reflexivity.
why it matters
This result anchors the module's claim that quantization is automatic for topological charges. It supports the module's main results on trajectory conservation and the count of three independent charges at D=3. In the Recognition Science framework it realizes the topological origin of integer charges tied to the forced dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.