DegreeCostComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-interval transfer of the literal prime-degree deletion. The padding-divisor indicator is kept, so its reciprocal saving is available in the residue-model bound.

theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_degree_cost_comparison line 15