LongPrimeSaving.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Every fixed power saving for the literal free prime, with the polynomial norm-twist and excluded-prime costs already absorbed.