OAI/NumberTheory/Ostmann/Construction/SelectedAnchorNaturalEnergy.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The code-preserving diagonal from actual selected-prime energy data
- theorem
OAI.Ostmann.uniform_selected_anchor_natural_energyline 12