topological_charge_trajectory_conserved
plain-language theorem explainer
The declaration shows that any topological charge remains constant along every variational trajectory in the ledger. Researchers deriving conservation laws from discrete topology in three dimensions rather than Noether symmetries would cite this when establishing time-independence of charges. The argument is a direct induction on the tick index that applies the charge's built-in conservation property at each successor step.
Claim. Let $Q$ be an integer-valued map on configurations of an $N$-entry ledger that is unchanged under each variational successor. Let $γ : ℕ → Configuration_N$ be a trajectory such that every consecutive pair obeys the variational update rule. Then $Q(γ(t)) = Q(γ(0))$ for every natural number $t$.
background
This module derives conservation from topological linking in D = 3 rather than continuous symmetries. A topological charge is a structure whose value map sends configurations to integers and whose conserved field asserts invariance under any variational successor. A trajectory is a function from natural numbers (ticks) to configurations; it is variational precisely when every consecutive pair satisfies the successor relation.
proof idea
The proof is by induction on the time index $t$. The base case at zero is reflexivity. The successor step rewrites the target equality via the inductive hypothesis and applies the conserved field of the charge to the pair of configurations at steps $n$ and $n+1$, using the trajectory assumption to supply the required successor relation.
why it matters
This supplies the exact invariance used by charge_at_any_tick and total_charge_always_zero, and it is a required step in the F-012 certificate that conservation is topological, integer-valued, and yields exactly three independent charges only in D = 3. It closes the link between the dimension-forcing result and the emergence of conserved quantities such as baryon and lepton number.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.