OAI/NumberTheory/TwoPoint/Bounds/ActualPrimeWordComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The literal prime supply and bounded padding catalog satisfy every parameter of the actual finite-origin word comparison.

  1. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_prime_word_comparison line 15