MovingClearedRows.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact cleared rows before reduction modulo prime squares

The row identities hold over the integers before any division or reduction. This permits the same occurrence line to be used modulo a prime square.

theorem OAI.Ostmann.PolynomialGiantRows.cleared_movingReverse line 16

theorem OAI.Ostmann.movingSlotNaturalPath_cleared line 46

Source documentation

The actual natural path multiplied by the cleared denominator equals its polynomial rows over any ring, in particular over ℤ and ZMod (p²).

theorem movingSlotNaturalPath_cleared {σ R : Type*} [CommRing R]
    (value : σ → ℕ) (path : List (MovingSlotReversal σ)) (pair : ℕ × ℕ)
    (hvalid : MovingSlotPathIntegral value path pair) :
    let φ := MvPolynomial.eval₂Hom (Int.castRingHom R) (fun i => (value i : R))
…

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

theorem OAI.Ostmann.movingSlotLine_cleared_numerator line 79

Source documentation

The single cleared line is the exact current numerator times the ancestor denominator. No unit or primality hypotheses enter this identity.

theorem movingSlotLine_cleared_numerator {σ R : Type*} [CommRing R]
    (value : σ → ℕ) (path : List (MovingSlotReversal σ))
    (current : MovingSlotReversal σ) (XL XR : ℕ)
    (hvalid : MovingSlotPathIntegral value path (XL, XR)) :
    let φ := MvPolynomial.eval₂Hom (Int.castRingHom R) (fun i => (value i : R))
…

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