Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.PositiveExcessDefectSquare

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

Positive-excess weighted response-defect-square estimate

This proof-internal file owns the final positive-excess estimate needed after squaring the weak-norm maximizer RHS.