SurvivingAlignment.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Normality aligns the actual surviving shifted-prime lists.

theorem OAI.TotientAsymptotic.surviving_largest_factor_alignment line 16

Source documentation

The canceled witness identity, separated bands and small residual primes supply every hypothesis of the factor-count alignment argument.

theorem surviving_largest_factor_alignment : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i p q : ℕ, 1 ≤ i → 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 ξ →
    tupleValue (witnessTuple p η)=tupleValue (witnessTuple q ξ) →
    wholeWitnessPrime p η i ≠ wholeWitnessPrime q ξ i →
    (∀ j < i, wholeWitnessPrime p η j=wholeWitnessPrime q ξ j) →
    GoodWitnessConditions p η → GoodWitnessConditions q ξ → ∀ y : ℝ,
    1 < normalityScale x i → 0 ≤ B (normalityScale x i) → normalityScale x i ≤ y →
    0 < B y → B y ≤ 2*fordBandScale x 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) →
…

lemma OAI.TotientAsymptotic.normalized_alignment_bound line 77