TimeTranslation
plain-language theorem explainer
The time translation symmetry on the real line is realized by the additive flow map sending each point x to x plus the group parameter t. Researchers deriving conservation laws from cost stationarity in the Recognition Science framework would cite this construction when instantiating the general Noether mechanism for energy. The definition satisfies the one-parameter group axioms by direct algebraic verification of the identity and composition properties.
Claim. The one-parameter group of time translations is the map sending each real number $x$ to $x + t$, equipped with the flow operation that obeys the identity condition at $t=0$ and the additive composition law.
background
OneParamGroup is the structure consisting of a flow map from reals to transformations on a space X, together with the two axioms that the zero-parameter flow is the identity and that the flow of a sum equals the composition of the individual flows. The module QFT-006 derives Noether's theorem from cost stationarity, where a symmetry is any transformation leaving the J-cost unchanged and conservation follows from ledger balance under that symmetry. Upstream, Energy is simply the type of real numbers in RS-native units, while the OneParamGroup structure itself supplies the abstract model used for all listed symmetries including time translation.
proof idea
The definition directly supplies the flow as ordinary addition on the reals. The identity axiom is discharged by ring simplification showing that adding zero leaves the point unchanged. The composition axiom is likewise discharged by ring simplification confirming that adding s then t is the same as adding their sum.
why it matters
This definition supplies the concrete symmetry instance required by the downstream theorem time_invariance_implies_conservation, which applies the noether_core lemma to conclude that any time-translation-invariant function is conserved along the flow. It therefore fills the time-translation row in the module's table of symmetries and conserved quantities, directly supporting the claim that energy is conserved under time invariance. The construction sits inside the broader Recognition Science program of obtaining Noether's theorem from ledger balance rather than from an independent action principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.