OAI/NumberTheory/TwoPoint/Bounds/BoundedWitnessDecay.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The singleton saving absorbs all record lengths, including the empty-word case.

  1. lemma OAI.TwoPointCorrelations.PrimeWordEncoding.Witnesses.length_pos line 12
  2. lemma OAI.TwoPointCorrelations.witnessLengthRecord_cost line 26
  3. theorem OAI.TwoPointCorrelations.eventually_bounded_witness_decay line 44