MovingSlotSystem.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The original recursive weight on moving-giant states

A reconstructed pivot is the composite u*p; only its quotient p becomes the new giant. The compensation primes remain in the regular child lists.

structure OAI.Ostmann.MovingSlotState line 15
def OAI.Ostmann.MovingSlotState.leftProduct line 21
def OAI.Ostmann.MovingSlotState.rightProduct line 26
def OAI.Ostmann.MovingSlotState.compensation line 31
def OAI.Ostmann.MovingSlotState.child line 36
def OAI.Ostmann.movingSlotSystem line 44
def OAI.Ostmann.movingSlotCutoff line 56
Source documentation
The extra support test is literal divisibility of the composite pivot by its sampled compensation product. All smooth and other support factors stay in extra.
```
noncomputable def movingSlotCutoff {σ : Type*} (value : σ → ℕ)
    (childBound pivotBound : ℕ → ℕ) (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    (x : MovingSlotState σ) (s v w : ℤ) : ℝ :=
…
```
Mentions: OAI.Ostmann.MovingSlotState
def OAI.Ostmann.MovingSlotData.Follows line 63
theorem OAI.Ostmann.MovingSlotData.Follows.root line 69
theorem OAI.Ostmann.buildMovingSlotData_follows line 75

theorem OAI.Ostmann.movingSlotWeight_nonzero_integral line 85

Source documentation

Nonzero original recursive coefficients force exactly the integral support of the concrete moving-giant sampler. This does not assign any prime law to its reconstructed integer pivot.

theorem movingSlotWeight_nonzero_integral {σ : Type*}
    (value : σ → ℕ) (childBound pivotBound : ℕ → ℕ)
    (leaf : MovingSlotState σ → ℤ → ℂ)
    (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
    (XL XR : ℕ)
    (hw : recursiveTransferWeight (movingSlotSystem value childBound pivotBound) leaf
      (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, XL, XR⟩ t ≠ 0) :
    T.Integral value XL XR := by
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingSlotCutoff