OAI/NumberTheory/Ostmann/Construction/ScheduledNodeEquations.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduledActualSourceScheme_left_natCast line 8
2. theorem OAI.Ostmann.scheduledActualSourceScheme_right_natCast line 30
3. theorem OAI.Ostmann.scheduled_scaled_history_equations line 54

   Source documentation

   Every equation is derived from the valid full arithmetic history. The fixed coefficients depend on the remaining word factors and ancestor pivots.

   theorem scheduled_scaled_history_equations {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (childBound pivotBound : ℕ → ℕ)
       (i : I) (hi : role i = .word) (S : Finset ℤ) (n : ℕ)
       (C : CopyScheduleAtoms role n → ℕ) (x : TreeLeafIndex n → ℕ)
       (t : FrequencyTree S n)
       (hu : ∀ k < n, ∀ a b, role a = .pivot k → role b = .pivot k → a = b)
       (hv : ValidTransferHistory (scheduleAtomSystem role childBound pivotBound) n
         ⟨n, wordLeafScale role i hi n C x⟩ (frequencyTreeMap Subtype.val n t)) :
       let p := transferPivotArray (scheduleAtomSystem role childBound pivotBound) n
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.FrequencyTree, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.scheduleAtomSystem, OAI.Ostmann.wordLeafScale, OAI.Ostmann.frequencyTreeMap, OAI.Ostmann.transferPivotArray