NoetherCharge
NoetherCharge packages a real-valued map on ledger configurations of N entries together with the requirement that the map stays constant under every variational successor step. Researchers comparing symmetry-derived conservation to topological linking in three dimensions cite this structure to isolate the non-quantized case. The definition is a direct structure that encodes the value function and the invariance predicate with no auxiliary lemmas.
claimA Noether charge for $N$ ledger entries is a pair consisting of a function $v : C(N) → ℝ$ and the assertion that $v(c') = v(c)$ for every pair of configurations $c, c'$ such that $c'$ is a variational successor of $c$, where $C(N)$ denotes the set of positive-real-ratio configurations of size $N$.
background
The module formalizes the claim that conservation laws in the Recognition Science ledger arise from topological linking in dimension three rather than from continuous symmetries. A configuration of $N$ ledger entries is a structure whose entries field maps each index in Fin $N$ to a positive real number. The variational successor relation selects, among all feasible next states, the configuration that minimizes total defect while respecting the update rule.
proof idea
This declaration is a structure definition that directly assembles the real-valued map on configurations with the predicate requiring invariance under the variational successor relation.
why it matters in Recognition Science
The structure supplies the target type into which topological charges are embedded by sending integer values to reals, enabling the construction of logChargeAsNoether and the proof that Noether charges need not be quantized. It supports the F-012 certificate by providing the baseline against which the integer-valued, D=3-restricted topological charges are contrasted, confirming that quantization and exact conservation originate from linking numbers rather than symmetry.
scope and limits
- Does not require the charge value to be an integer.
- Does not derive the charge from a continuous symmetry group.
- Does not assert existence of nontrivial charges for every N.
- Does not apply to continuous-time flows outside discrete variational steps.
formal statement (Lean)
166structure NoetherCharge (N : ℕ) where
167 value : Configuration N → ℝ
168 conserved : ∀ (c next : Configuration N),
169 IsVariationalSuccessor c next → value next = value c
170
171/-- Log-charge is a Noether charge (conserved, real-valued). -/