push_forward
plain-language theorem explainer
Push-forward aggregates probability mass from each fiber of φ to define a distribution on the codomain. Information theorists and statistical mechanicians cite the operation when reducing state spaces in monotonicity arguments. The definition is realized by direct summation that selects p(ω) exactly on the preimage of each target point.
Claim. Given a map $p : Ω → ℝ$ and a function $φ : Ω → Ω'$, the push-forward $p' : Ω' → ℝ$ is the function $p'(ω') := ∑_{ω : φ(ω)=ω'} p(ω)$.
background
The Free Energy Monotonicity module establishes that Recognition Free Energy is non-increasing under coarse-graining and equilibration, supplying the Recognition Science version of the Second Law. The push-forward supplies the concrete operation that sends distributions on a fine space Ω to distributions on a coarse space Ω' by collecting mass on each fiber. Preservation of non-negativity and total probability under this map are recorded in the immediately following theorems.
proof idea
The definition is given directly by the summation expression that adds p(ω) for every ω satisfying φ(ω) = ω'.
why it matters
The definition supplies the core operation for the data processing inequality and the coarse-graining decreases free energy theorem. Those results establish that free energy decreases under reduced state resolution and thereby define the arrow of time in the Recognition framework. The construction matches the standard push-forward used to derive the data processing inequality for KL divergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.