MovingGiantRows.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Ordered coefficient rows for the moving-giant reversal

In the manuscript's order both children put the inserted giant first. The left child is therefore the exchanged version of the retained-first reversal. This exchange preserves the nonvanishing determinant used in the line bounds.

def OAI.Ostmann.GiantRows.swap line 18
theorem OAI.Ostmann.GiantRows.eval_swap line 20
theorem OAI.Ostmann.GiantRows.det_swap line 23
def OAI.Ostmann.GiantRows.movingReverse line 28
Source documentation
Both source children order their giants as (new, retained).
```
def movingReverse (T : GiantRows R) (left : Bool) (v w u : Rˣ) : GiantRows R :=
…
```
Mentions: OAI.Ostmann.GiantRows
theorem OAI.Ostmann.GiantRows.eval_movingReverse line 31
theorem OAI.Ostmann.GiantRows.isUnit_det_movingReverse line 38

theorem OAI.Ostmann.GiantRows.movingReverse_integer_node line 47

Source documentation

An exact integer node gives the actual child giant pair under reduction.

theorem movingReverse_integer_node {q : ℕ} [Fact q.Prime]
    (T : GiantRows (ZMod q)) (left : Bool) (v w u : (ZMod q)ˣ)
    (x y : ZMod q) (XL XR p CL CR ML MR comp : ℕ) (s fv fw : ℤ)
    (hpair : T.eval x y = ((XL : ZMod q), (XR : ZMod q)))
    (hv : (v : ZMod q) = (fv : ZMod q) * ((CR * MR : ℕ) : ZMod q))
    (hw : (w : ZMod q) = (fw : ZMod q) * ((CL * ML : ℕ) : ZMod q))
    (hu : (u : ZMod q) = (s : ZMod q) * (comp : ZMod q))
    (hnode : fv * ((XR * CR * MR : ℕ) : ℤ) -
      fw * ((XL * CL * ML : ℕ) : ℤ) = s * ((comp * p : ℕ) : ℤ)) :
    (T.movingReverse left v w u).eval x y =
      ((p : ZMod q), if left then (XL : ZMod q) else (XR : ZMod q)) := by
…

Mentions: OAI.Ostmann.GiantRows, OAI.Ostmann.GiantRows.eval

def OAI.Ostmann.movingGiantAncestorRows line 71
Source documentation
The full path retains the same determinant invariant in the source order.
```
def movingGiantAncestorRows {R : Type*} [CommRing R] : List (GiantReversal R) → GiantRows R
  | [] => GiantRows.identity
  | s :: steps => (movingGiantAncestorRows steps).movingReverse s.left s.v s.w s.u
```
Mentions: OAI.Ostmann.GiantReversal, OAI.Ostmann.GiantRows, OAI.Ostmann.GiantRows.identity
theorem OAI.Ostmann.movingGiantAncestorRows_isUnit_det line 75
theorem OAI.Ostmann.movingGiantAncestorRows_numerator_nonzero line 81
def OAI.Ostmann.PolynomialGiantRows.swap line 93
def OAI.Ostmann.PolynomialGiantRows.movingReverse line 96
theorem OAI.Ostmann.PolynomialGiantRows.normalized_swap line 100
theorem OAI.Ostmann.PolynomialGiantRows.normalized_movingReverse line 103
theorem OAI.Ostmann.PolynomialGiantRows.degreeLE_movingReverse line 112