OAI/NumberTheory/Ostmann/Construction/DyadicTwoTailContradiction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The original contradiction with its integer parameters constructed

The endpoint scale, moment orders and Fourier cutoff are chosen explicitly. Only the actual two tails, populated dyadic prime block and small-prime masks remain as geometric data.

  1. theorem OAI.Ostmann.eventual_dyadic_two_tail_contradiction line 19