OAI/NumberTheory/TwoPoint/Bounds/AffineWeightedWordComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The existing signed word comparison on each fixed progression class. All state, circuit and coefficient budgets remain unchanged.

  1. theorem OAI.TwoPointCorrelations.BravermanDepth22Input.eventually_affine_weighted_word_comparison line 13