RegularGraphObstruction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The scalar projection theorem rules out the actual family of refined planar graphs, with all numerical losses displayed for later scale absorption.