RealAction
plain-language theorem explainer
RealAction denotes the space of all maps from the real line to itself, serving as the domain for J-action functionals when specializing the abstract Noether theorem to the Recognition Science cost setting. Researchers deriving energy or momentum conservation from translation symmetries cite this type when stating invariance hypotheses. The declaration is a direct one-line type abbreviation with no computational content or lemmas.
Claim. The domain for J-action functionals consists of all maps $γ : ℝ → ℝ$.
background
The module specializes the abstract noether_core theorem to J-action cost functionals on trajectories. RealAction supplies the underlying space of real-valued paths, with Time identified upstream as the real numbers to parameterize these paths. The J-action itself is the cost functional whose continuous symmetries produce conserved quantities along trajectories, following the paper companion in RS_Least_Action.tex on Noether conservation laws as corollaries.
proof idea
This declaration is a direct type abbreviation with no lemmas or tactics applied.
why it matters
The abbreviation supplies the domain for the downstream definitions of time-translation invariance and space-translation invariance, which feed directly into the theorems asserting energy conservation and momentum conservation via noether_core. It thereby realizes the main results of the module: time-translation invariance of the J-action yields energy conservation, while space-translation invariance yields momentum conservation. The construction sits inside the Recognition Science forcing chain by converting abstract Noether symmetries into concrete conservation statements for the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.