OAI/NumberTheory/Ostmann/Construction/ConstituentScheduleEquiv.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.copyConstituentEquiv line 11

   Source documentation

   The copied constituent labels are the current atom labels paired with an original index inside that atom. No new prime slots appear.

   noncomputable def copyConstituentEquiv {I : Type*} (size : I → ℕ) : (n : ℕ) →
       CopyScheduleVertex (Σ i, Fin (size i)) n ≃
         (Σ v : CopyScheduleVertex I n, Fin (size (copyScheduleOrigin n v)))
     | 0 => Equiv.refl _
     | n + 1 =>
       let e := copyConstituentEquiv size n
   …

   Mentions: OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.copyScheduleOrigin

2. theorem OAI.Ostmann.copyConstituentEquiv_atom line 42
3. theorem OAI.Ostmann.constituentForget_injective line 52
4. def OAI.Ostmann.survivingConstituentEquiv line 64

   Source documentation

   Surviving constituent slots are exactly a surviving atom and one of its original prime positions.

   noncomputable def survivingConstituentEquiv {I : Type*} (role : I → CopyScheduleRole)
       (size : I → ℕ) (n : ℕ) :
       {v : CopyScheduleVertex (Σ i, Fin (size i)) n //
         CopyScheduleSurvives (role ∘ Sigma.fst) n v} ≃
       (Σ v : {v : CopyScheduleVertex I n // CopyScheduleSurvives role n v},
         Fin (size (copyScheduleOrigin n v.val))) where
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.copyScheduleOrigin