total_charge_always_zero
plain-language theorem explainer
Any topological charge on a variational trajectory that begins at zero value stays zero at every subsequent tick. Recognition Science modelers cite this to establish that initial neutrality propagates without invoking continuous symmetries. The proof is a one-line rewrite that substitutes the trajectory conservation lemma into the initial condition.
Claim. Let $Q$ be an integer-valued function on configurations of an $N$-entry ledger that is invariant under each variational successor step. Let $traj$ be a sequence of configurations such that each consecutive pair satisfies the variational update rule, and suppose $Q(traj(0)) = 0$. Then $Q(traj(t)) = 0$ for every natural number $t$.
background
TopologicalCharge is a structure whose value map sends each configuration to an integer and whose conserved field asserts invariance under every IsVariationalSuccessor step. Trajectory is the type of functions from ticks to configurations; IsVariationalTrajectory requires that every consecutive pair obeys the variational update rule. The module sets the local setting as F-012, where conservation laws arise from linking numbers in D = 3 rather than from Noether symmetries. Upstream, topological_charge_trajectory_conserved states that for any such Q and variational trajectory, the value at tick t equals the value at tick 0.
proof idea
The term proof opens with intro t to fix an arbitrary tick, then rewrites the goal using the upstream lemma topological_charge_trajectory_conserved applied to Q, traj and the hypothesis h, after which the initial-condition hypothesis h_init discharges the resulting equality.
why it matters
This result closes the loop on F-012 by showing that topological charges (linking numbers) are conserved along any variational path once the ledger starts neutral. It sits downstream of the D = 3 forcing in DimensionForcing and the variational dynamics definitions, confirming that integer charge conservation requires no extra symmetry group. The declaration supports the broader claim that conservation is topological rather than Noetherian, with no open scaffolding remaining in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.