push_forward_sum_one
plain-language theorem explainer
The theorem shows that pushing a normalized probability distribution forward under any map to a coarser state space preserves the total mass of one. Researchers establishing monotonicity of Recognition Free Energy under coarse-graining cite it as a basic normalization fact. The argument is a short term-mode calculation that unfolds the push-forward definition, commutes the sums, and simplifies the indicator terms to recover the input hypothesis.
Claim. Let $p : Ω → ℝ$ satisfy $∑_{ω} p(ω) = 1$. For any map $φ : Ω → Ω'$, the push-forward distribution satisfies $∑_{ω'} (∑_{ω : φ(ω)=ω'} p(ω)) = 1$.
background
This lemma sits inside the FreeEnergyMonotone module, whose goal is to prove that Recognition Free Energy is non-increasing under coarse-graining and equilibration, the Recognition Science version of the Second Law. The push-forward aggregates probability mass over preimages of φ, modeling loss of state resolution. Upstream results supply the cost function as the derived cost of a multiplicative recognizer comparator and as the J-cost of a recognition event; these ensure the free-energy expressions remain well-defined on the underlying landscape.
proof idea
The proof is a direct term-mode verification. It unfolds the definition of push_forward, rewrites the double sum by commuting the order of summation, simplifies the ite expressions via membership in the finite universe, and concludes by exact application of the given normalization hypothesis.
why it matters
The result supplies the normalization step required by the downstream theorem coarse_graining_decreases_free_energy, which establishes that free energy cannot increase when states are aggregated. It thereby supports the data-processing inequality for KL divergence in the Recognition setting and the definition of the arrow of time via dF_R/dt ≤ 0. The lemma closes a basic consistency requirement in the thermodynamic-stability arguments of the Recognition-Science-Full-Theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.