constCharge
plain-language theorem explainer
The declaration builds a topological charge that returns the fixed integer n for every configuration on an N-entry ledger. Researchers modeling quantized invariants in the Recognition Science ledger cite it when constructing trivial conserved quantities independent of dynamics details. The construction is a direct structure definition that sets the value map to the constant function and confirms invariance by reflexivity on the successor predicate.
Claim. For natural number $N$ and integer $n$, the constant topological charge is the structure whose value map sends every configuration to $n$ and whose conservation property holds identically under any variational successor.
background
The module establishes that conservation laws in Recognition Science originate from topological linking in dimension 3 rather than continuous symmetries. TopologicalCharge is the structure consisting of an integer-valued function on configurations together with the requirement that this function is invariant under the variational successor relation. The module imports DimensionForcing to enforce D=3 as the unique dimension permitting nontrivial linking and uses the ledger factorization from DAlembert to ground the dynamics.
proof idea
The definition constructs the TopologicalCharge record by assigning the constant function returning n to the value field and discharging the conserved field with the reflexivity tactic on the equality of integers.
why it matters
It supplies the simplest example of a quantized topological charge, supporting the module's enumeration of independent charges at D=3 and the contrast with Noether charges that need not be integers. The parent results include three_charges_at_D3 and topological_charge_quantized, which rely on the existence of such constant instances to count linking numbers per coordinate plane of Q3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.