MovingResidueTests.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Three explicit residue tests at each original moving node

def OAI.Ostmann.MovingFormulaNode.testFormulas line 10
def OAI.Ostmann.MovingFormulaNode.testModuli line 13
def OAI.Ostmann.MovingFormulaNode.residueTests line 16
theorem OAI.Ostmann.formula_integral_small_test line 21
theorem OAI.Ostmann.MovingFormulaNode.residueTests_iff line 30
def OAI.Ostmann.MovingFormulaNode.residuePeriod line 39
Source documentation
The actual common period is built from the cleared formula denominators and the two retained frequency moduli.
```
noncomputable def MovingFormulaNode.residuePeriod (f : MovingFormulaNode) : ℕ :=
…
```
Mentions: OAI.Ostmann.MovingFormulaNode
theorem OAI.Ostmann.MovingFormulaNode.residuePeriod_pos line 42
theorem OAI.Ostmann.MovingFormulaNode.test_period_dvd line 52

theorem OAI.Ostmann.MovingFormulaNode.residueTests_modEq line 60

Source documentation

All three tests are constant on the constructed residue classes.

theorem MovingFormulaNode.residueTests_modEq (f : MovingFormulaNode)
    (a b : Bool → ℤ) (h : ∀ i, a i ≡ b i [ZMOD f.residuePeriod]) :
    f.residueTests a ↔ f.residueTests b := by
…

Mentions: OAI.Ostmann.MovingFormulaNode

def OAI.Ostmann.movingGiantUpdate line 69

theorem OAI.Ostmann.MovingFormulaNode.holds_polynomials line 74

Source documentation

At a fixed residue class, the remaining arithmetic support uses only three explicit polynomial inequalities and fixed frequency bounds.

theorem MovingFormulaNode.holds_polynomials (f : MovingFormulaNode)
    (a : Bool → ℤ) (coord : Bool) (z : ℤ) :
    (f.guard.ValidAt (movingGiantUpdate a coord z) ∧ f.newGiant.IntegralAt (movingGiantUpdate a coord z)) ↔
      f.residueTests (movingGiantUpdate a coord z) ∧ f.guard.frequencyBounds ∧
        ∀ j, 0 ≤ (f.guard.polynomials a coord j).eval (z : ℝ) := by
…

Mentions: OAI.Ostmann.MovingFormulaNode, OAI.Ostmann.movingGiantUpdate