isSpaceTranslationInvariant
plain-language theorem explainer
Defines space-translation invariance for any J-action functional S on real trajectories. Workers deriving momentum conservation via Noether's theorem in the Recognition Science setting cite this predicate. The definition quantifies over all real shifts dx and requires the action to be unchanged under the corresponding spaceShift map.
Claim. A functional $S$ on trajectories of type $ℝ → ℝ$ is space-translation invariant when $S(γ(·) + dx) = S(γ)$ for every real $dx$, where the shifted trajectory is obtained by adding the constant $dx$ at each time.
background
RealAction is the type of real-valued trajectories, i.e., functions $ℝ → ℝ$. The spaceShift family adds a fixed real displacement $dx$ to every point of a trajectory. IsSymmetryOf, taken from the abstract QFT.NoetherTheorem module, asserts that a map $T$ leaves a functional $J$ unchanged: $J(T x) = J x$ for all $x$ in the domain.
proof idea
One-line definition that applies the IsSymmetryOf predicate directly to the spaceShift family for every real $dx$.
why it matters
Supplies the spatial-invariance hypothesis required by the momentum-conservation corollary in the same module. It mirrors the time-translation case and completes the set of continuous symmetries whose conserved currents follow from the abstract noether_core theorem. The module states that all three (time, space, phase) are direct corollaries of that core result applied to the J-action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.