HeightAlignment.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Alignment of prime heights, including the largest prime.

lemma OAI.TotientAsymptotic.height_bounds_factor_order line 15
lemma OAI.TotientAsymptotic.alignment_of_height_bounds line 51

theorem OAI.TotientAsymptotic.actual_surviving_alignment line 75

Source documentation

The concrete good collision lists are aligned also when their first unequal prime is index zero. No extra comparison input is used.

theorem actual_surviving_alignment : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i p q : ℕ, i ≤ R x H → L x H < m x → R x H < L x H → p.Prime →
    ∀ η ξ : RemainderDatum (L x H), IsBasicRemainder x H η → IsBasicRemainder x H ξ →
    GoodWitnessConditions p η → GoodWitnessConditions q ξ →
    tupleValue (witnessTuple p η)=tupleValue (witnessTuple q ξ) →
    wholeWitnessPrime p η i ≠ wholeWitnessPrime q ξ i →
    (∀ j < i, wholeWitnessPrime p η j=wholeWitnessPrime q ξ j) → ∀ y : ℝ,
    1<y → 0<B y → (87/100 : ℝ)*fordBandScale x i≤B y → B y≤2*fordBandScale x i →
    y^(9/10 : ℝ)≤wholeWitnessPrime p η i → y^(9/10 : ℝ)≤wholeWitnessPrime q ξ i →
    (∀ r : Fin (collisionSurvivors p q η ξ i (collisionLastIndex x i)).card,
      ((survivingPair p q η ξ i (collisionLastIndex x i)).left r-1 : ℕ)≤y ∧
      ((survivingPair p q η ξ i (collisionLastIndex x i)).right r-1 : ℕ)≤y) →
…