Six Birds Verified XIII: Time, Charge and Currency

Abstract

One number can look like three things: the generator of time evolution, a conserved charge, and a currency that crosses a boundary. These are an operator, a state function and a ledger entry. We show which structure links them, over the rationals. A skew factor makes a generator conserve a quadratic storage; for nondegenerate storage these are all the conserving generators. When defined, the Cayley step is an exact discrete time action that conserves the storage exactly when the generator does; for positive-definite storage it always exists. Ports turn the storage into a ledger: every midpoint step balances exactly, dissipation enters as a booked loss, and coupled systems cancel internal supply for every output exactly when the coupling is skew. For m oscillators the conserved quadratic forms have dimension at least m, more when frequencies coincide, so the generator alone fixes the energy up to scale only for one oscillator. Six examples show each link failing without its structure. Against dominating dissipation, supply plus storage depletion must cover a loss proportional to the midpoint storage, and repairs have a cost floor under a fixed positive gain and a gain-per-cost bound. All results are formalized in Lean 4.