TupleDegreeDeletion.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Sum the tuple-degree deletion before normalization. One reciprocal prime factor remains for each selected tuple coordinate, and every padding choice contributes its exact u(q)/q mass.

theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_integer_tuple_degree_deletion line 15