OAI/NumberTheory/TwoPoint/Bounds/ActualWordComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual signed closed word has the finite-origin error required by the matrix trace argument. Only the published Braverman input is used for this transfer; the residue expectation is unchanged.

  1. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.pair_primeFactors_card line 21
  2. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_actual_word_comparison line 31