OAI/NumberTheory/Ostmann/Construction/WordTransferGuard.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.HistoryFormula.integerValue line 11
2. theorem OAI.Ostmann.HistoryFormula.smallDivisionTest_of_value line 14
3. theorem OAI.Ostmann.HistoryFormula.smallDivisionTest_iff line 23
4. structure OAI.Ostmann.WordTransferGuard line 35
5. def OAI.Ostmann.WordTransferGuard.ValidAt line 44
6. def OAI.Ostmann.wordTransferGuard line 53
7. theorem OAI.Ostmann.wordTransferGuard_iff line 65

   Source documentation

   All original node conditions are represented: both coprimality tests, integrality, positive bounded pivot, child-frequency bounds and strict gap.

   theorem wordTransferGuard_iff {σ : Type*} {n : ℕ} (d : WordTransferNode σ)
       (l r : WordTransferTemplate σ n) (s v w : ℤ) (hs : s ≠ 0)
       (env : σ → HistoryFormula σ) (a : σ → ℤ) (x : σ → ℕ)
       (henv : ∀ i, (env i).value (fun j => (a j : ℚ)) = (x i : ℚ)) :
       (wordTransferGuard d s v w hs env).ValidAt a ↔
         ∃ P, ValidTransferNode (wordTransferSystem σ)
           ((WordTransferTemplate.node d l r).state x) s v w P := by
   …

   Mentions: OAI.Ostmann.WordTransferNode, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.HistoryFormula, OAI.Ostmann.wordTransferGuard, OAI.Ostmann.ValidTransferNode, OAI.Ostmann.wordTransferSystem