spaceShift
plain-language theorem explainer
spaceShift supplies the constant spatial displacement operator on real trajectories in the J-action setting. Researchers deriving Noether conservation laws for momentum from spatial symmetries cite this construction. It is realized as a direct functional definition that adds dx to the trajectory value at each time.
Claim. The space translation by a real number $dx$ maps a trajectory $γ : ℝ → ℝ$ to the shifted trajectory $t ↦ γ(t) + dx$.
background
In the Noether module for the J-action, RealAction denotes the type of real-valued trajectories $γ : ℝ → ℝ$ on which the cost functional acts. The module specializes the abstract Noether theorem from QFT.NoetherTheorem.noether_core to this setting, yielding conserved quantities from continuous symmetries of the action. Upstream, the definition of RealAction provides the domain for the shift operator.
proof idea
This is a one-line definition that constructs the shifted trajectory by pointwise addition of the constant dx.
why it matters
This definition is the building block for isSpaceTranslationInvariant, which states that the J-action is unchanged under spaceShift, and for spaceTranslationFlow, which equips it with a one-parameter group structure. It directly supports the derivation of momentum conservation from space-translation invariance of the J-action, as a corollary of the abstract noether_core theorem. In the Recognition Science chain this corresponds to the spatial symmetry sector at D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.