charge_at_any_tick
plain-language theorem explainer
Topological charges on an N-entry ledger remain constant along any variational trajectory at arbitrary ticks. A physicist deriving conservation laws from linking numbers in three dimensions would cite this to obtain time-independent integer charges without continuous symmetries. The argument is a one-line wrapper applying the trajectory conservation result at each of the two times.
Claim. Let $Q$ be a topological charge on an $N$-entry ledger (an integer-valued function on configurations that is invariant under variational successors). For any trajectory traj following the variational dynamics and any times $t_1, t_2$, the charge satisfies $Q(traj(t_1)) = Q(traj(t_2))$.
background
The module establishes that conservation laws arise from topological linking in D = 3 rather than Noether symmetries. Charges are integer-valued invariants under the ledger dynamics, with baryon and lepton numbers realized as linking numbers that cannot change under continuous deformation.
proof idea
This is a one-line wrapper that rewrites both sides using the upstream theorem topological_charge_trajectory_conserved applied at t1 and at t2, equating each to the value at tick zero.
why it matters
The result shows charges are invariant at every tick, completing the topological conservation argument in F-012. It rests on the exact conservation along trajectories and supports downstream claims such as three independent charges at D = 3. In the Recognition Science framework it aligns with the forcing of D = 3 for non-trivial linking and quantized integer charges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.