PolynomialGiantRows.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Clearing denominators along the giant histories

The five integer polynomials below represent both coefficient rows with a common denominator. Each reversal uses only multiplication and subtraction; their degree grows by at most the degree of the new slot data.

structure OAI.Ostmann.PolynomialGiantRows line 17
def OAI.Ostmann.PolynomialGiantRows.identity line 25
def OAI.Ostmann.PolynomialGiantRows.reverse line 27
def OAI.Ostmann.PolynomialGiantRows.normalized line 37
Source documentation
Normalized coefficients after evaluating all small prime variables.
```
def normalized {K : Type*} [Field K] (T : PolynomialGiantRows σ)
    (φ : MvPolynomial σ ℤ →+* K) : GiantRows K :=
…
```
Mentions: OAI.Ostmann.PolynomialGiantRows, OAI.Ostmann.GiantRows
theorem OAI.Ostmann.PolynomialGiantRows.retained_quotient line 42
theorem OAI.Ostmann.PolynomialGiantRows.reversed_quotient line 46

theorem OAI.Ostmann.PolynomialGiantRows.normalized_reverse line 52

Source documentation

The polynomial recurrence evaluates to the actual rational reversal.

theorem normalized_reverse {K : Type*} [Field K] (T : PolynomialGiantRows σ)
    (φ : MvPolynomial σ ℤ →+* K) (left : Bool) (v w u : MvPolynomial σ ℤ)
    (hd : φ T.denominator ≠ 0) (hv : φ v ≠ 0) (hw : φ w ≠ 0) (hu : φ u ≠ 0) :
    (T.reverse left v w u).normalized φ =
      (T.normalized φ).reverse left (Units.mk0 (φ v) hv) (Units.mk0 (φ w) hw)
        (Units.mk0 (φ u) hu) := by
…

Mentions: OAI.Ostmann.PolynomialGiantRows, OAI.Ostmann.PolynomialGiantRows.normalized, OAI.Ostmann.PolynomialGiantRows.reverse

def OAI.Ostmann.PolynomialGiantRows.DegreeLE line 66
Source documentation
A simultaneous degree bound for the four cleared coefficients and denominator.
```
def DegreeLE (T : PolynomialGiantRows σ) (d : ℕ) : Prop :=
…
```
Mentions: OAI.Ostmann.PolynomialGiantRows
theorem OAI.Ostmann.PolynomialGiantRows.degreeLE_identity line 70
theorem OAI.Ostmann.PolynomialGiantRows.degreeLE_reverse line 73
structure OAI.Ostmann.PolynomialReversal line 95
def OAI.Ostmann.polynomialAncestorRows line 101
theorem OAI.Ostmann.polynomialAncestorRows_degree line 105