OAI/NumberTheory/Ostmann/Characters/CharacterIterationContradiction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite character transfer and the final contradiction

All diagonal and final comparison bounds here are derived from the physical prime ranges and original harmonic priors. The initial amplitude is supplied by the separately proved fixed-bin endpoint statistic.

  1. theorem OAI.Ostmann.eventual_character_iteration_contradiction line 17