ScheduledFinalPrimeRanges.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The final one-sided pair retains its actual anchor and word origins

theorem OAI.Ostmann.copyScheduleOrigin_outside line 9
theorem OAI.Ostmann.copyScheduleOrigin_anchor line 15
theorem OAI.Ostmann.scheduled_final_pair_interaction_word line 27
theorem OAI.Ostmann.scheduled_final_relative_origins line 71

theorem OAI.Ostmann.scheduled_final_relative_prime_ranges line 98

Source documentation

The actual one-sided pair lies in the small anchor and long word ranges. These are the precise prime sets used by the original independent priors.

theorem scheduled_final_relative_prime_ranges {I : Type*} (role : I → CopyScheduleRole)
    (pivot : ℕ → I) (n m : ℕ) (word : Fin m ≃ {i : I // role i = .word})
    (anchor : Fin (n + 1) → I) (ha : ∀ j, role (anchor j) = .anchor j)
    (hp : ∀ k < n + 1, role (pivot k) = .pivot k)
    (Q : I → Finset ℕ) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
    (lower : ℝ) (Bq A E : ℕ)
    (hsquare : ∀ j q, q ∈ Q (anchor j) → χ (anchor j) q ^ 2 ≠ 1)
    (hanchor : ∀ j q, q ∈ Q (anchor j) → lower ≤ (q : ℝ) ∧ q ≤ Bq)
    (hword : ∀ i, role i = .word → ∀ p ∈ Q i, 2 * A ≤ p ∧ p ≤ E)
    (e f : FinalParityReassignments n m) (hef : e ≠ f) :
    ∃ a b : CopyScheduleAtoms role (n + 1), a ≠ b ∧
      (∀ q ∈ Q (copyScheduleOrigin (n + 1) a.val), lower ≤ (q : ℝ) ∧ q ≤ Bq) ∧
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.copyScheduleOrigin