HeavyCellRegularity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Heavy-cell selection supplies the local point regularity used in the coarse-direction projection argument, with the complete loss displayed.