GraphScalarRegularity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A dense small-projection graph transfers its planar ball bound to the actual scalar reference set, with half the planar exponent.