OAI/NumberTheory/TwoPoint/Bounds/ResidueNumericalWitnesses.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nonzero singleton centering produces the numerical event counted by witness metadata.

  1. theorem OAI.TwoPointCorrelations.selected_residue_numerical_witnesses line 13