spaceShift
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish that the J-action is invariant under the shift.
- Does not extend to time-dependent shifts or complex-valued trajectories.
- Does not compute the associated conserved quantity.
- Does not reference the specific form of the J-functional.
Lean usage
def isSpaceTranslationInvariant (S : RealAction → ℝ) : Prop := ∀ dx : ℝ, IsSymmetryOf (spaceShift dx) Sformal statement (Lean)
71def spaceShift (dx : ℝ) : RealAction → RealAction :=
proof body
Definition body.
72 fun γ t => γ t + dx
73
74/-- A J-action functional on real-valued trajectories is
75 space-translation invariant if shifting the trajectory by a constant
76 leaves the action unchanged. -/