OAI/NumberTheory/Ostmann/Construction/ScheduledPrimePhase.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledPrimePhase line 13
2. theorem OAI.Ostmann.copiedSlotCharacter_schedule line 23
3. theorem OAI.Ostmann.scheduledPrimePhase_step line 33

   Source documentation

   The copied local phase is exactly the next phase on all surviving slots, with the same original character attached to every copied prime coordinate.

   theorem scheduledPrimePhase_step {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
       (g : I → I → ℤ) (pivot : ℕ → I) (initial : I → ℤ → ℕ → ℂ)
       (n : ℕ) (t : FrequencyTree ℤ (n + 1))
       (q : (Bool × CopyScheduleH role n) ⊕ CopyScheduleY role n → ℕ)
       [∀ i, Fact (q i).Prime] (center : ∀ p : ℕ, ZMod p) :
       directedPrimePhase q
         (fun i => copiedSlotCharacter (fun h => χ (copyScheduleOrigin n h.val))
           (fun y => χ (copyScheduleOrigin n y.val)) i (q i))
         (fun i => center (q i))
         (copiedSlotUnary q (fun h => χ (copyScheduleOrigin n h.val))
           (scheduledRetainedGraph role g pivot n)
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FrequencyTree, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.directedPrimePhase, OAI.Ostmann.copiedSlotCharacter, OAI.Ostmann.copyScheduleOrigin, OAI.Ostmann.copiedSlotUnary, OAI.Ostmann.scheduledRetainedGraph

4. theorem OAI.Ostmann.copiedDirectedPhase_scheduled line 83

   Source documentation

   The copied phase appearing in the exact arithmetic off-diagonal is already the actual next schedule phase.

   theorem copiedDirectedPhase_scheduled {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
       (g : I → I → ℤ) (pivot : ℕ → I) (initial : I → ℤ → ℕ → ℂ)
       (n : ℕ) (t : FrequencyTree ℤ (n + 1))
       (L R : CopyScheduleH role n → ℕ) (U : CopyScheduleY role n → ℕ)
       [∀ h, Fact (L h).Prime] [∀ h, Fact (R h).Prime] [∀ y, Fact (U y).Prime]
       (center : ∀ p : ℕ, ZMod p) :
       letI := transferredPrimeFact L R U
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FrequencyTree, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.transferredPrimeFact