GiantReversalRows.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Coefficient rows of the giant reversals

At a reversal one current giant is retained and the other becomes (v * Hminus - w * Hplus) / u, with all three coefficients units modulo the internal prime. The two current giants remain independent linear forms in the top giants, so every subsequent numerator is a nonzero row.

structure OAI.Ostmann.GiantRows line 17
Source documentation
Coefficients of the two current giants in the two top giants.
```
@[ext] structure GiantRows (R : Type*) where
…
```
def OAI.Ostmann.GiantRows.identity line 27
def OAI.Ostmann.GiantRows.det line 29
def OAI.Ostmann.GiantRows.eval line 31
def OAI.Ostmann.GiantRows.reverse line 35
Source documentation
left = true retains the first giant; false retains the second.
```
def reverse (T : GiantRows R) (left : Bool) (v w u : Rˣ) : GiantRows R :=
…
```
Mentions: OAI.Ostmann.GiantRows
theorem OAI.Ostmann.GiantRows.eval_reverse line 43
theorem OAI.Ostmann.GiantRows.det_reverse line 55
theorem OAI.Ostmann.GiantRows.isUnit_det_reverse line 60

theorem OAI.Ostmann.GiantRows.numerator_nonzero line 69

Source documentation

Every numerator in an invertible current pair is a nonzero row.

theorem numerator_nonzero {K : Type*} [Field K] (T : GiantRows K)
    (hT : T.det ≠ 0) (v w : Kˣ) :
    (v : K) * T.c - (w : K) * T.a ≠ 0 ∨
      (v : K) * T.d - (w : K) * T.b ≠ 0 := by
…

Mentions: OAI.Ostmann.GiantRows

structure OAI.Ostmann.GiantReversal line 84
Source documentation
The data retained at one ancestor substitution.
```
structure GiantReversal (R : Type*) [CommRing R] where
…
```
def OAI.Ostmann.giantAncestorRows line 90
theorem OAI.Ostmann.giantAncestorRows_isUnit_det line 94
theorem OAI.Ostmann.giantAncestorRows_numerator_nonzero line 100