OAI/NumberTheory/Ostmann/Construction/WordPrimeReplay.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.HistoryPrimeCheck line 11
2. def OAI.Ostmann.HistoryPrimeCheck.Holds line 15
3. theorem OAI.Ostmann.HistoryFormula.integerValue_of_value line 19
4. inductive OAI.Ostmann.WordPrimeDecoration line 26
5. def OAI.Ostmann.WordPrimeDecoration.ValidAt line 31
6. def OAI.Ostmann.WordPrimeDecoration.checks line 42
7. theorem OAI.Ostmann.wordTransfer_pivot_formula_value line 53
8. theorem OAI.Ostmann.WordPrimeDecoration.checks_iff line 65

   Source documentation

   The tests use original prime values, unchanged by the pivot updates.

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

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

9. def OAI.Ostmann.WordPrimeDecoration.count line 86
10. theorem OAI.Ostmann.WordPrimeDecoration.checks_length line 90
11. theorem OAI.Ostmann.WordPrimeDecoration.check_formula_mem line 103

    Source documentation

    Each check is attached to one of the actual pivot formulas, so it inherits the already proved degree and small-denominator bounds.

    theorem WordPrimeDecoration.check_formula_mem {σ V : Type*} {n : ℕ}
        (D : WordPrimeDecoration V n) (template : WordTransferTemplate σ n)
        (t : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t) (env : σ → HistoryFormula σ) :
        ∀ g ∈ D.checks template t ht env,
          g.formula ∈ (template.branching t ht).pivotFormulas env := by
    …

    Mentions: OAI.Ostmann.WordPrimeDecoration, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.HistoryFormula