MovingNodeGuards.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomial and residue tests for the actual moving-giant node

def OAI.Ostmann.movingNodeWord line 11
def OAI.Ostmann.movingNodeGuard line 20
Source documentation
The two word entries are the complete current child products, including all regular factors. The reconstructed pivot here is the composite u*p.
```
noncomputable def movingNodeGuard (CL CR : ℕ) (s v w : ℤ) (hs : s ≠ 0)
    (childBound pivotBound : ℕ) (L R : HistoryFormula Bool) : WordTransferGuard Bool :=
…
```
Mentions: OAI.Ostmann.HistoryFormula, OAI.Ostmann.WordTransferGuard

theorem OAI.Ostmann.movingNodeGuard_iff line 27

Source documentation

Identification with the original validity predicate, before any arithmetic restriction is removed.

theorem movingNodeGuard_iff {σ : Type*} (value : σ → ℕ)
    (childBound pivotBound : ℕ → ℕ) {n : ℕ} (s : ℤ) (CL CR u : List σ)
    (left right : MovingSlotData σ n) (hs : s ≠ 0) (XL XR : ℕ)
    (L R : HistoryFormula Bool) (a : Bool → ℤ)
    (hL : L.value (fun b => (a b : ℚ)) = (XL : ℚ))
    (hR : R.value (fun b => (a b : ℚ)) = (XR : ℚ)) :
    (movingNodeGuard (MovingSlotReversal.naturalProduct value CL)
      (MovingSlotReversal.naturalProduct value CR) s left.frequency right.frequency hs
      (childBound (n + 1)) (pivotBound (n + 1)) L R).ValidAt a ↔
    ∃ P, ValidTransferNode (movingSlotSystem value childBound pivotBound)
      ⟨n + 1, .node s CL CR u left right, XL, XR⟩ s left.frequency right.frequency P := by
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.HistoryFormula, OAI.Ostmann.movingNodeGuard, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.ValidTransferNode, OAI.Ostmann.movingSlotSystem

theorem OAI.Ostmann.movingNodeGuard_polynomials line 69

Source documentation

At an actual moving node all non-residue validity tests are exactly three polynomial inequalities in the chosen top giant coordinate.

theorem movingNodeGuard_polynomials {σ : Type*} (value : σ → ℕ)
    (childBound pivotBound : ℕ → ℕ) {n : ℕ} (s : ℤ) (CL CR u : List σ)
    (left right : MovingSlotData σ n) (hs : s ≠ 0) (XL XR : ℕ)
    (L R : HistoryFormula Bool) (a : Bool → ℤ) (coord : Bool) (z : ℤ)
    (hL : L.value (fun b => (Function.update a coord z b : ℚ)) = (XL : ℚ))
    (hR : R.value (fun b => (Function.update a coord z b : ℚ)) = (XR : ℚ)) :
    let g := movingNodeGuard (MovingSlotReversal.naturalProduct value CL)
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.HistoryFormula, OAI.Ostmann.movingNodeGuard, OAI.Ostmann.MovingSlotReversal.naturalProduct