C6: properness and the unproved output estimate

XIII-B proves properness for support-preserving extensions in the existing compact graph closure XIIIB. The widened contacts retain that closure. Properness is therefore available once the relevant graph distributions exist. It cannot define an undefined distribution product.