IsConservedAlong'
plain-language theorem explainer
Defines an alternative formulation of conservation for a quantity Q along a one-parameter flow φ by the direct requirement that Q composed with φ at any time t equals the original Q. Researchers deriving Noether charges from cost stationarity in Recognition Science cite this when switching between orbit-wise and time-fixed statements. The declaration is introduced as a functional equation without lemmas or reductions.
Claim. Let $Q : X → ℝ$ be a real-valued quantity on a space $X$ and let $φ : ℝ → X → X$ be a flow. Then $Q$ is conserved along $φ$ when $Q ∘ φ_t = Q$ holds for every real $t$.
background
In the QFT-006 module on Noether's theorem from cost stationarity, a symmetry is a transformation that leaves the J-cost unchanged while conservation means the associated charge remains constant along solutions, arising from ledger balance. The sibling definition IsConservedAlong requires $Q(φ t_1 x) = Q(φ t_2 x)$ for all $x ∈ X$ and all times $t_1, t_2$, expressing constancy on orbits. The present definition supplies the equivalent pointwise condition $Q(φ t x) = Q(x)$ for all $t$. Upstream structures such as LedgerFactorization supply the underlying J-cost and ledger balance, while PhiForcingDerived and SpectralEmergence provide the convex minimization and gauge content that motivate these conservation notions.
proof idea
This declaration is a direct definition. It encodes the alternative conservation condition exactly as the functional equation ∀ t : ℝ, Q ∘ (φ t) = Q.
why it matters
This definition supports the equivalence theorem conserved_iff_conserved' in the same module, which links the orbit-constant and time-fixed versions under the assumption that φ 0 acts as the identity. It supplies a convenient formulation inside the derivation of Noether's theorem from ledger structure, where time-translation symmetry yields energy conservation. Within Recognition Science it connects to the eight-tick octave and J-cost minimization that force continuous symmetries and the associated conserved charges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.