OAI/NumberTheory/TwoPoint/Walks/ProhibitedNumericalSingletonDecay.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Singleton decay on the same fixed-length numerical catalog as the other trace classes. The list encoding introduces no multiplicity.

  1. theorem OAI.TwoPointCorrelations.eventually_prohibited_numerical_singleton_decay line 14