OAI/NumberTheory/TwoPoint/Walks/ColumnSingletonDecay.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The singleton estimate on the column/padding catalog used by the good forest estimate. Prime factorization proves that the encoding is injective.

  1. theorem OAI.TwoPointCorrelations.eventually_prohibited_column_singleton_decay line 14