logChargeAsNoether
Log-charge, the sum of logarithms over configuration entries, is equipped with the structure of a Noether charge under variational dynamics. Researchers examining the separation between topological and symmetry-based conservation in Recognition Science would cite this construction. The definition is a direct wrapper that assigns the log-ratio function to the value field and verifies conservation by the successor relation.
claimFor any natural number $N$, the function sending a configuration $c$ of $N$ positive reals to $c_i$ to the sum of their logarithms defines a Noether charge: its real value remains unchanged whenever one configuration is a variational successor of another.
background
The module contrasts conservation arising from topological linking in three dimensions with conservation arising from continuous symmetries. A Noether charge is a real-valued function on configurations that stays constant along any variational successor step, as defined by the structure with fields value and conserved. The upstream log_charge supplies the concrete map as the sum of Real.log over all entries of the configuration. This sits inside the ledger's variational dynamics, where successor steps preserve positivity and the total log-ratio.
proof idea
The definition directly instantiates the NoetherCharge structure by setting value to log_charge. The conserved predicate is supplied by a lambda that takes the successor hypothesis and extracts its first component, which encodes preservation of the sum under the dynamics.
why it matters in Recognition Science
It provides the explicit real-valued example required by the downstream theorem noether_not_necessarily_quantized, which shows that Noether charges need not be integers. This sharpens the module's distinction between topological charges (integer-valued via linking in D=3) and Noether charges (real-valued). The construction supports the F-012 registry item on the origin of conservation laws by exhibiting a concrete invariant that follows from the variational flow rather than from topology.
scope and limits
- Does not derive the charge from linking numbers or D=3 topology.
- Does not prove that the charge takes integer values.
- Does not address quantization or spin-statistics consequences.
- Does not extend the construction beyond the ledger's discrete variational steps.
Lean usage
use 1, logChargeAsNoether 1formal statement (Lean)
172noncomputable def logChargeAsNoether (N : ℕ) : NoetherCharge N where
173 value := log_charge
proof body
Definition body.
174 conserved := fun _ _ h => h.1
175
176/-- Every topological charge induces a Noether charge by ℤ ↪ ℝ. -/