OAI/NumberTheory/TwoPoint/Bounds/CodedWitnessFiber.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual numerical main/witness segments satisfy the fixed-code reciprocal bound.

  1. theorem OAI.TwoPointCorrelations.CrudeWordCode.witness_fiber_reciprocal_bound line 13