OAI/NumberTheory/Ostmann/Construction/SelectedNonanchorWitness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduled_matched_code_prime_ranges_at line 10
2. theorem OAI.Ostmann.selected_nonanchor_matching_witness line 76
3. theorem OAI.Ostmann.selected_nonanchor_prime_ranges line 107

   Source documentation

   The only word-prime range used is that of the selected bulk embedding. In particular no separation premise is imposed on the top label.

   theorem selected_nonanchor_prime_ranges {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (pivot : ℕ → I) (n m : ℕ)
       (bulk : Fin m ↪ I) (hbulk : ∀ i, role (bulk i) = .word)
       (e : Equiv.Perm (CopyScheduleH role (n + 1)))
       (he : e ∈ cellPreservingMatchings (selectedBulkLabel role (n + 1) m bulk hbulk) \
         selectedAnchorMatchingSet role (n + 1) m bulk hbulk)
       (small large : Fin (n + 1) → I)
       (hsmall : ∀ j, role (small j) = .anchor j) (hlarge : ∀ j, role (large j) = .anchor j)
       (hp : ∀ k < n + 1, role (pivot k) = .pivot k)
       (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p) (Q₀ : I → Finset ℕ)
       (hχsmall : ∀ j q, q ∈ Q₀ (small j) → χ (small j) q ^ 2 ≠ 1)
       (hχbulk : ∀ i q, q ∈ Q₀ (bulk i) → χ (bulk i) q ^ 2 ≠ 1)
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.cellPreservingMatchings, OAI.Ostmann.selectedBulkLabel, OAI.Ostmann.selectedAnchorMatchingSet