OAI/NumberTheory/TwoPoint/Bounds/TraceIntervalError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite word-comparison error absorbs the full physical trace catalog, including every initial vertex and both words of the pair.

  1. lemma OAI.TwoPointCorrelations.trace_interval_error_le_one line 10