noether_not_necessarily_quantized
plain-language theorem explainer
Noether charges are real-valued maps from ledger configurations to reals that remain invariant under variational successors. A researcher distinguishing symmetry-based from topology-based conservation in Recognition Science cites this to show quantization is not forced for Noether charges. The proof constructs an explicit example with N equal to 1, the log-charge map, and a constant configuration of value 2, then derives a contradiction from 0 less than log 2 less than 1.
Claim. There exists a natural number $N$, a real-valued conserved quantity $Q$ on configurations of size $N$, and a configuration $c$ of $N$ positive real entries, such that $Q(c)$ is not equal to any integer.
background
The TopologicalConservation module derives conservation from topological linking in D equals 3 rather than continuous symmetries. A NoetherCharge consists of a real-valued function on configurations together with a proof of invariance under variational successors. A Configuration is a structure holding an array of N positive real ledger ratios, as defined in InitialCondition.
proof idea
The proof proceeds by explicit construction. It sets N to 1 and Q to logChargeAsNoether 1, then builds a configuration whose single entry equals 2. Assuming the value equals an integer n leads to 0 less than n less than 1 via Real.log_pos, comparison of log 2 to log(exp 1) using lt_trans and Real.log_lt_log, followed by linarith and omega to contradict the integer bounds.
why it matters
This result feeds the topological_conservation_certificate by supplying the required contrast that Noether charges need not be integers. It completes the module's F-012 argument that conservation arises from linking numbers in D equals 3, which are necessarily quantized, while Noether charges remain real-valued. The declaration sharpens the distinction between symmetry-based and topological origins of conservation laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.