OAI/NumberTheory/TwoPoint/Bounds/SingletonWordEnvelope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every nonzero full-word envelope supplies the same bounded numerical witness record.

  1. theorem OAI.TwoPointCorrelations.singleton_envelope_has_padding_witness line 13