MovingSlotRealization.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Integer realization of the source-ordered slot rows

def OAI.Ostmann.MovingSlotReversal.naturalProduct line 13
Source documentation
Each list is evaluated as its actual natural product, with multiplicities.
```
def naturalProduct {σ : Type*} (value : σ → ℕ) (slots : List σ) : ℕ :=
…
```
theorem OAI.Ostmann.MovingSlotReversal.coefficient_nat_eval line 16
def OAI.Ostmann.MovingSlotReversal.naturalPivot line 28
def OAI.Ostmann.MovingSlotReversal.naturalStep line 33
def OAI.Ostmann.MovingSlotReversal.IntegralAt line 38
Source documentation
This is exactly the integer equation at a supported reversal.
```
def IntegralAt {σ : Type*} (s : MovingSlotReversal σ) (value : σ → ℕ)
    (pair : ℕ × ℕ) : Prop :=
…
```
Mentions: OAI.Ostmann.MovingSlotReversal
def OAI.Ostmann.MovingSlotReversal.naturalReduction line 46
theorem OAI.Ostmann.MovingSlotReversal.polynomial_step_integer line 50
def OAI.Ostmann.movingSlotNaturalPath line 83
Source documentation
A path is written with its newest reversal first, matching the cleared row recursion. Each step is performed over the integers before reduction.
```
def movingSlotNaturalPath {σ : Type*} (value : σ → ℕ) :
    List (MovingSlotReversal σ) → (ℕ × ℕ) → ℕ × ℕ
  | [], pair => pair
  | s :: path, pair => s.naturalStep value (movingSlotNaturalPath value path pair)
```
Mentions: OAI.Ostmann.MovingSlotReversal
def OAI.Ostmann.MovingSlotPathIntegral line 88

theorem OAI.Ostmann.movingSlotNaturalPath_realized line 96

Source documentation

The polynomial ancestor pair is the reduction of the actual integer reversal path, rather than an unrelated invertible linear system.

theorem movingSlotNaturalPath_realized {σ : Type*} {q : ℕ} [Fact q.Prime]
    (value : σ → ℕ) (path : List (MovingSlotReversal σ)) (pair : ℕ × ℕ)
    (hvalid : MovingSlotPathIntegral value path pair)
    (hunit : ∀ s ∈ path,
      MovingSlotReversal.naturalReduction q value s.polynomial.v ≠ 0 ∧
      MovingSlotReversal.naturalReduction q value s.polynomial.w ≠ 0 ∧
      MovingSlotReversal.naturalReduction q value s.polynomial.u ≠ 0) :
    let φ := MvPolynomial.eval₂Hom (Int.castRingHom (ZMod q))
…

Mentions: OAI.Ostmann.MovingSlotReversal, OAI.Ostmann.MovingSlotPathIntegral, OAI.Ostmann.MovingSlotReversal.naturalReduction