Coarse-graining support: Support.Book.Ch05.Theorems.Section54.Common

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Section 5.4 common imports

This file is the shared import surface for the current-manuscript Section 5.4 formalization. It deliberately re-exports only the established Section 5.2 surface; the first three Section 5.4 results must remain independent of Section 5.3.