partition_function_preserved
plain-language theorem explainer
The partition function of a recognition system equals the sum of Boltzmann factors over coarse states when the effective cost on each coarse state absorbs the fiber sum under a surjective map. Researchers deriving monotonicity of free energy or the data-processing inequality in information-theoretic thermodynamics would cite this result. The proof unfolds the definitions, verifies positivity of each fiber sum via surjectivity, simplifies the exponent algebraically, and interchanges summation order to collapse indicators.
Claim. Let $Z = ∑_ω exp(-J(X(ω))/T)$ be the partition function of a recognition system at temperature $T$. For any surjective coarse-graining map $φ$, $Z = ∑_{ω'} exp(-J_{eff}(ω')/T)$, where the effective cost $J_{eff}(ω')$ is defined so that $exp(-J_{eff}(ω')/T)$ recovers the sum of $exp(-J(X(ω))/T)$ over the preimage fiber $φ^{-1}(ω')$.
background
The module establishes monotonicity of Recognition Free Energy under coarse-graining and relaxation, providing the Recognition Science formulation of the second law. The partition function is the sum of Boltzmann factors $exp(-Jcost(X ω)/TR)$ over microstates, while the effective cost on a coarse state is the negative-temperature logarithm of the fiber sum of those factors. Surjectivity of the coarse-graining map ensures every macrostate has at least one preimage, so no fiber sum vanishes.
proof idea
The tactic proof first unfolds partition_function and effective_cost. It sets s to the fiber sum, proves s > 0 by picking a preimage via surjectivity and bounding the sum from below by a single positive term, then simplifies the exponent via field_simp and ring. The main calculation applies Finset.sum_comm followed by Finset.sum_ite_eq to interchange sums and collapse the indicator functions, yielding the desired equality.
why it matters
This theorem supplies the scale-invariance step needed for the data-processing inequality on relative entropy and for coarse_graining_decreases_free_energy in the same module. It thereby supports the arrow-of-time result rs_arrow_of_time and the overall claim that free energy is non-increasing under Recognition dynamics. The result aligns with the Recognition Composition Law by preserving the partition function across the eight-tick octave and three-dimensional spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.