ConstituentCopyEntries.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Grouping constituents commutes with the actual H/Y copy operation

theorem OAI.Ostmann.constituent_copy_entry line 11
theorem OAI.Ostmann.constituent_retained_entry line 19

theorem OAI.Ostmann.constituent_copy_product line 29

Source documentation

The H atom in either branch is exactly the product of that branch's copied original prime positions.

theorem constituent_copy_product {I : Type*} (role : I → CopyScheduleRole) (size : I → ℕ)
    (n : ℕ) (b : Bool) (v : CopyScheduleH role n)
    (q : CopyScheduleVertex (Σ i, Fin (size i)) (n + 1) → ℕ) :
    ((scheduleConstituentWord role size (n + 1) (scheduledOutputVertex role n (.inl (b, v)))).map
        (fun i => q i.val)).prod =
    ∏ k : Fin (size (copyScheduleOrigin n v.val)),
      q (.inl (b, ((survivingConstituentEquiv role size n).symm
        ⟨⟨v.val, v.property.1⟩, k⟩).val)) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.scheduleConstituentWord, OAI.Ostmann.scheduledOutputVertex, OAI.Ostmann.copyScheduleOrigin, OAI.Ostmann.survivingConstituentEquiv

theorem OAI.Ostmann.constituent_retained_product line 41

Source documentation

A Y atom keeps exactly the same constituent indices.

theorem constituent_retained_product {I : Type*} (role : I → CopyScheduleRole) (size : I → ℕ)
    (n : ℕ) (v : CopyScheduleY role n)
    (q : CopyScheduleVertex (Σ i, Fin (size i)) (n + 1) → ℕ) :
    ((scheduleConstituentWord role size (n + 1) (scheduledOutputVertex role n (.inr v))).map
        (fun i => q i.val)).prod =
    ∏ k : Fin (size (copyScheduleOrigin n v.val)),
      q (.inr ((survivingConstituentEquiv role size n).symm
        ⟨⟨v.val, v.property.1⟩, k⟩).val) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.scheduleConstituentWord, OAI.Ostmann.scheduledOutputVertex, OAI.Ostmann.copyScheduleOrigin, OAI.Ostmann.survivingConstituentEquiv