MinorArcOriginGeometry.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Discrete interval origins: simultaneous prime windows occupy only a bounded number of origins once the first origin is fixed.

lemma OAI.TwoPointCorrelations.minor_arc_origin_bounds line 16
Source documentation
For factors in a dyadic block, all other origins lie within three interval lengths of the scaled first origin. This also applies to factors d*p, so the same geometry survives the multiplicative correction.
```
lemma minor_arc_origin_bounds (A B H k l m : ℕ) (hA : 0 < A)
    (hB : B ≤ 2 * A) (hk : k < A * m ∧ A * m ≤ k + H)
    (hl : l < B * m ∧ B * m ≤ l + H) :
    (B * k) / A - H ≤ l ∧ l ≤ (B * k) / A + 2 * H := by
…
```
lemma OAI.TwoPointCorrelations.minor_arc_origin_count line 41