OAI/NumberTheory/Ostmann/Construction/WordUnitPeriod.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.WordRangeDecoration.formulas_frequencies_dvd line 11
2. theorem OAI.Ostmann.WordRangeDecoration.formulas_denominator_period line 56
3. theorem OAI.Ostmann.WordRangeDecoration.unitGuards_modulus line 76
4. theorem OAI.Ostmann.WordRangeDecoration.unitGuards_period line 103

   Source documentation

   The extra inherited unit gates use the same explicit modulus as the node integrality gates; no new periodicity input is assumed.

   theorem WordRangeDecoration.unitGuards_period {σ : Type*} {n : ℕ}
       (D : WordRangeDecoration σ n) (template : WordTransferTemplate σ n)
       (t : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t)
       (B : ℕ) (hB : 1 ≤ B) (hwords : template.WordsBounded B) (hD : D.WordsBounded B) :
       ∀ g ∈ D.unitGuards template t ht .prime,
         g.formula.cleared.denominator * (g.modulus : ℤ) ∣ (wordTransferFullPeriod n t B : ℤ) := by
   …

   Mentions: OAI.Ostmann.WordRangeDecoration, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.wordTransferFullPeriod