WordTransferPeriods.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A common residue period derived from the actual branching frequencies

def OAI.Ostmann.internalFrequencyList line 13

Source documentation

Only internal frequencies enter the denominators of reconstructed words.

def internalFrequencyList : (n : ℕ) → FrequencyTree ℤ n → List ℤ
  | 0, _ => []
  | n + 1, t => t.1 :: (internalFrequencyList n t.2.1 ++ internalFrequencyList n t.2.2)

Mentions: OAI.Ostmann.FrequencyTree

theorem OAI.Ostmann.internalFrequencyList_length line 17
theorem OAI.Ostmann.internalFrequencyList_nonzero line 26
theorem OAI.Ostmann.WordTransferTemplate.branching_frequencies_dvd line 38

theorem OAI.Ostmann.WordTransferTemplate.branching_denominator_period line 93

Source documentation

This is the actual small-frequency modulus, not a new periodicity assumption.

theorem WordTransferTemplate.branching_denominator_period {σ : Type*} {n : ℕ}
    (template : WordTransferTemplate σ n) (t : FrequencyTree ℤ n)
    (hn : NonzeroInternalFrequencies n t) (B : ℕ) (hB : 1 ≤ B)
    (hwords : template.WordsBounded B) (s : ℤ)
    (hs : s ∣ (historyFrequencyBase (internalFrequencyList n t) : ℤ)) :
    (∀ z ∈ (template.branching t hn).formulaLeaves .prime,
      z.2.cleared.denominator * s ∣
        (historyFrequencyPeriod (internalFrequencyList n t) (B ^ (n + 1) + 1) : ℤ)) ∧
    (∀ F ∈ (template.branching t hn).pivotFormulas .prime,
      F.cleared.denominator * s ∣
        (historyFrequencyPeriod (internalFrequencyList n t) (B ^ (n + 1) + 1) : ℤ)) := by
…

Mentions: OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.historyFrequencyBase, OAI.Ostmann.internalFrequencyList, OAI.Ostmann.historyFrequencyPeriod