RowRegularity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative 2s-regularity of the union of the tube pencils on one regular row, as used in the product-structure projection argument.