ExpandedScheduleHistory.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The prime-word and atom systems have identical valid histories

theorem OAI.Ostmann.expanded_schedule_history_iff line 11

theorem OAI.Ostmann.expandedRootTemplate_history_iff line 51

Source documentation

All initial constituent primes feed the actual atom products; the constructed finite coordinates impose no extra validity conditions.

theorem expandedRootTemplate_history_iff {I α : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (depth : ℕ) (words : CopyScheduleAtoms role depth → List α)
    (childBound pivotBound : ℕ → ℕ) (x : ExpandedScheduledVariable α depth → ℕ)
    (t : FrequencyTree ℤ depth) :
    ValidTransferHistory (wordTransferSystem (ExpandedScheduledVariable α depth)) depth
      ((expandedRootTemplate role depth words childBound pivotBound).state x) t ↔
    ValidTransferHistory (scheduleAtomSystem role childBound pivotBound) depth
      ⟨depth, fun i => (((words i).map Sum.inl).map x).prod⟩ t :=
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ExpandedScheduledVariable, OAI.Ostmann.FrequencyTree, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.wordTransferSystem, OAI.Ostmann.expandedRootTemplate, OAI.Ostmann.scheduleAtomSystem