OAI/NumberTheory/TwoPoint/Walks/CanonicalRawSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite prime-defect tails supply the required numerical phase selection for the canonical graph at every sufficiently large auxiliary scale.

  1. theorem OAI.TwoPointCorrelations.canonical_raw_pair_selection line 15