OAI/NumberTheory/TwoPoint/Bounds/ActualWitnessRecord.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Encode an actual attached witness family without adding any numerical choices.

  1. theorem OAI.TwoPointCorrelations.actual_witness_has_encoded_record line 13