conserved_iff_conserved'
plain-language theorem explainer
The two characterizations of a conserved quantity along a flow are equivalent once the flow fixes every initial point. Researchers deriving Noether's theorem from cost stationarity cite this equivalence to move freely between orbit-constant and composition-constant statements of charges. The proof is a direct biconditional via constructor, function extensionality, and the supplied initial condition.
Claim. Let $Q: X → ℝ$ and let $φ: ℝ → X → X$ satisfy $φ(0,x)=x$ for all $x$. Then $Q(φ(t_1,x))=Q(φ(t_2,x))$ for all $x,t_1,t_2$ if and only if $Q ∘ φ_t = Q$ for every real $t$.
background
In the QFT module on Noether's theorem from cost stationarity, conservation along a flow is introduced in two equivalent forms. IsConservedAlong requires that $Q$ takes the same value at every point on an orbit: $Q(φ t_1 x)=Q(φ t_2 x)$ for all times and states. The companion definition requires invariance under each time slice of the flow via composition. The module derives the classical Noether correspondence (energy from time translation, momentum from space translation) from ledger balance under symmetries that leave the J-cost unchanged. Upstream lemmas supply the composition law for automorphisms and the actualization operator that selects realized configurations from possibilities.
proof idea
The term proof opens with constructor to split the biconditional. One direction applies funext, rewrites via the initial condition $φ 0 x = x$, and uses the supplied composition assumption. The converse extracts the two time slices with congr_fun, then rewrites both sides under the orbit assumption using the composition lemma from CostAlgebra.
why it matters
The result removes a definitional ambiguity inside the cost-stationarity derivation of Noether's theorem, letting later steps in the same module (noether_core and invariant_is_noether_charge) invoke whichever form is convenient. It directly supports the framework claim that every continuous symmetry of the action yields a conserved charge, consistent with the Recognition Composition Law and the emergence of energy, momentum, and charge from the eight-tick structure. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.