OAI/NumberTheory/Ostmann/Construction/WordUnitReplay.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.HistoryUnitGuard line 11
2. def OAI.Ostmann.HistoryUnitGuard.Holds line 15
3. def OAI.Ostmann.WordRange.toUnitGuard line 19
4. theorem OAI.Ostmann.WordRange.toUnitGuard_holds line 23
5. def OAI.Ostmann.WordRangeDecoration.UnitsAt line 43

   Source documentation

   The same word lists that specify ranges also specify product-unit tests. The interval endpoints are irrelevant for this additional support family.

   noncomputable def WordRangeDecoration.UnitsAt {σ : Type*} :
       {n : ℕ} → WordRangeDecoration σ n → WordTransferTemplate σ n →
         (σ → ℕ) → FrequencyTree ℤ n → Prop
     | 0, .leaf ranges, .leaf _, x, v => ∀ r ∈ ranges, ((r.word.map x).prod).Coprime v.natAbs
     | n + 1, .node ranges L R, .node d l r, x, t =>
         let P := historyPivot (wordTransferSystem σ) ((WordTransferTemplate.node d l r).state x)
   …

   Mentions: OAI.Ostmann.WordRangeDecoration, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.historyPivot, OAI.Ostmann.wordTransferSystem

6. def OAI.Ostmann.WordRangeDecoration.unitGuards line 54
7. theorem OAI.Ostmann.WordRangeDecoration.unitGuards_iff line 67

   Source documentation

   The quotient residues retain every inherited frequency-unit condition, including at terminal leaves and at previously reconstructed pivots.

   theorem WordRangeDecoration.unitGuards_iff {σ : Type*} {n : ℕ}
       (D : WordRangeDecoration σ n) (template : WordTransferTemplate σ n)
       (t : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t)
       (env : σ → HistoryFormula σ) (a : σ → ℤ) (x : σ → ℕ)
       (henv : ∀ i, (env i).value (fun j => (a j : ℚ)) = (x i : ℚ))
       (hv : ValidTransferHistory (wordTransferSystem σ) n (template.state x) t) :
       (∀ g ∈ D.unitGuards template t ht env, g.Holds a) ↔ D.UnitsAt template x t := by
   …

   Mentions: OAI.Ostmann.WordRangeDecoration, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.HistoryFormula, OAI.Ostmann.ValidTransferHistory, OAI.Ostmann.wordTransferSystem

8. theorem OAI.Ostmann.WordRangeDecoration.unitGuards_length line 89
9. theorem OAI.Ostmann.WordRangeDecoration.unitGuards_formulas line 100