OAI/NumberTheory/Ostmann/Construction/HistoryResidueGate.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.smallDivisionTest line 14
2. theorem OAI.Ostmann.smallDivisionTest_modEq line 17
3. theorem OAI.Ostmann.integerPolynomial_eval_modEq line 36
4. theorem OAI.Ostmann.cleared_history_test_residue_invariant line 44
5. def OAI.Ostmann.clearedHistoryResidueGate line 51
6. theorem OAI.Ostmann.clearedHistoryResidueGate_norm line 58
7. theorem OAI.Ostmann.clearedHistoryResidueGate_exact line 67

   Source documentation

   The original conjunction of integer divisibility and frequency-unit checks is exactly a bounded function of the surviving prime residue.

   theorem clearedHistoryResidueGate_exact {σ I : Type*} [Fintype I]
       (P : I → MvPolynomial σ ℤ) (d : I → ℤ) (s : I → ℕ)
       (a : σ → ℤ) (i : σ) (M : ℕ) [NeZero M]
       (hd : ∀ j, d j ≠ 0) (hdiv : ∀ j, d j * s j ∣ (M : ℤ)) (x : ℤ) :
       clearedHistoryResidueGate P d s a i M (x : ZMod M) =
         if ∀ j, smallDivisionTest
           (MvPolynomial.eval₂ (RingHom.id ℤ) (Function.update a i x) (P j)) (d j) (s j)
           then 1 else 0 := by
   …

   Mentions: OAI.Ostmann.clearedHistoryResidueGate, OAI.Ostmann.smallDivisionTest