topological_to_noether
plain-language theorem explainer
Every topological charge on an N-entry ledger, defined as an integer-valued function invariant under variational successors, induces a Noether charge by embedding its values into the reals while copying the conservation property. A researcher comparing topological invariants to symmetry-based conservation would cite this construction to separate integer quantization from real-valued charges. The definition is a direct structure builder that applies simplification to the inherited conserved predicate.
Claim. For any natural number $N$ and topological charge $Q$ (an integer-valued map from configurations to integers that remains unchanged under variational successors), the induced Noether charge is the real-valued map $cmapsto (Q(c):mathbb{R})$ equipped with the same conservation rule under variational successors.
background
The module establishes that conservation laws originate from topological linking in three dimensions rather than continuous symmetries. A topological charge is an integer-valued function on configurations that is invariant under variational dynamics, making quantization structural rather than imposed. A Noether charge is the analogous real-valued conserved quantity. This definition supplies the canonical embedding of the former into the latter via the inclusion of integers into reals.
proof idea
The definition constructs a NoetherCharge record by casting the integer-valued function to reals and discharging the conservation obligation with a single simplification step that reuses the topological charge's conserved predicate.
why it matters
The construction bridges the topological and Noether notions of charge, enabling the module's explicit statement that Noether charges need not be quantized. It supports the broader claim that conservation arises from linking numbers in D=3 rather than symmetry groups, consistent with the eight-tick octave and dimension-forcing results upstream. No downstream uses are recorded, leaving open how this embedding interacts with specific particle charges or the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.