OneParamGroup
plain-language theorem explainer
OneParamGroup encodes a continuous one-parameter family of transformations on a space X that satisfy the group properties of identity at t=0 and additivity in the parameter. Physicists modeling symmetries in QFT or classical mechanics cite this structure when deriving conservation laws from invariance under cost stationarity. The declaration is a pure structure definition with no computational content or proof obligations.
Claim. A one-parameter group on a space $X$ consists of a flow map $φ: ℝ → (X → X)$ such that $φ(0,x)=x$ for all $x$ and $φ(s+t,x)=φ(s,φ(t,x))$ for all real $s,t,x$.
background
In the QFT-006 module, Noether's theorem is derived from Recognition Science cost stationarity: a symmetry leaves the J-cost unchanged while ledger balance enforces conservation. OneParamGroup supplies the model for continuous symmetries generated by a single real parameter, such as time or space shifts on RealAction. Upstream structures calibrate the J-cost via ledger factorization and phi-forcing, while the module imports Mathlib for real arithmetic together with Constants and Cost.
proof idea
This is a direct structure definition. The three fields encode the flow map and the two group axioms with no lemmas or tactics applied.
why it matters
OneParamGroup is the carrier structure for all subsequent Noether results in the module, including noether_core (invariance implies conservation along the flow), invariant_is_noether_charge, and the concrete timeTranslationFlow and spaceTranslationFlow that recover energy and momentum conservation. It realizes the paper proposition on Noether from ledger structure and feeds the summary theorem that lists the standard-model conservation laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.