IsConservedAlong
plain-language theorem explainer
The definition states that a real-valued quantity Q on a space X is conserved along a one-parameter flow φ precisely when Q takes the same value at every point on any orbit of φ. Researchers deriving conservation laws from symmetries in Recognition Science's cost-stationarity formalism cite this predicate as the target property for Noether-type results. It is introduced directly via universal quantification over initial points and time pairs with no auxiliary lemmas.
Claim. A function $Q : X → ℝ$ is conserved along the flow $φ : ℝ → (X → X)$ if $Q(φ(t₁, x)) = Q(φ(t₂, x))$ for every $x ∈ X$ and all real $t₁, t₂$.
background
The QFT.NoetherTheorem module derives Noether's theorem from Recognition Science cost stationarity. A symmetry leaves the J-cost unchanged while conservation requires the associated charge to remain constant along solution orbits; the present definition isolates the conservation side as constancy on flow orbits. The module sets up the correspondence via ledger balance under continuous symmetries, with standard examples including time translation yielding energy and space translation yielding momentum.
proof idea
This is a direct definition, not a derived theorem. It encodes orbit constancy as a universal statement over x, t₁ and t₂; no lemmas or tactics are invoked beyond the primitive predicate.
why it matters
The definition supplies the target predicate for the noether_core theorem, which shows that invariance of J under a one-parameter group implies conservation along the flow. It is invoked to obtain energy conservation from time-translation invariance and momentum conservation from space-translation invariance. In the Recognition framework it realizes the cost-stationarity route to Noether's theorem, supporting the ledger-based derivation of standard conservation laws and closing one link in the forcing chain from T5 J-uniqueness through T8 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.