Rigidity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial orbit rigidity from the Mason–Stothers theorem.

lemma OAI.ComplexCancellation.Rigidity.isUnit_of_square_dvd line 14
Source documentation
A polynomial of degree at most one has no nonunit square divisor.
```
lemma isUnit_of_square_dvd {n t : k[X]} (hn : n ≠ 0) (hdeg : n.natDegree ≤ 1)
    (ht : t ^ 2 ∣ n) : IsUnit t := by
…
```
lemma OAI.ComplexCancellation.Rigidity.orbit_coprime line 28
Source documentation
Coprimality of the square and cube terms of an affine-linear orbit sum.
```
lemma orbit_coprime {a d u n : k[X]} (hn : n ≠ 0) (hdeg : n.natDegree ≤ 1)
    (heq : d ^ 2 + a ^ 2 * u ^ 3 = n) : IsCoprime (d ^ 2) (a ^ 2 * u ^ 3) := by
…
```
Mentions: OAI.ComplexCancellation.u

lemma OAI.ComplexCancellation.Rigidity.radical_orbit_bound line 46

Source documentation

The polynomial degree bound expressed with radicals.

lemma radical_orbit_bound [DecidableEq k] (a d u n : k[X]) :
    (radical (d ^ 2 * (a ^ 2 * u ^ 3) * (-n))).natDegree ≤
    d.natDegree + a.natDegree + u.natDegree + n.natDegree := by
…

Mentions: OAI.ComplexCancellation.u

theorem OAI.ComplexCancellation.Rigidity.orbit_constant line 74

Source documentation

A nonsquare obstruction over the coefficient field forces constant polynomial orbits.

theorem orbit_constant [CharZero k] {a d u n : k[X]}
    (ha : a ≠ 0) (hd : d ≠ 0) (hu : u ≠ 0) (hn : n ≠ 0)
    (hdeg : n.natDegree ≤ 1) (heq : d ^ 2 + a ^ 2 * u ^ 3 = n)
    (hns : ∀ z : k, z ^ 2 ≠ -(u.coeff 0) ^ 3) :
    a = C (a.coeff 0) ∧ d = C (d.coeff 0) ∧ u = C (u.coeff 0) := by
…

Mentions: OAI.ComplexCancellation.u

lemma OAI.ComplexCancellation.Rigidity.ratFunc_intDegree_pow line 127
theorem OAI.ComplexCancellation.Rigidity.ratFunc_X_cube_nonsquare line 137
Source documentation
The cube of the rational parameter is not the negative of a square.
```
theorem ratFunc_X_cube_nonsquare {K : Type*} [Field K] (z : RatFunc K) :
    z ^ 2 ≠ -(RatFunc.X : RatFunc K) ^ 3 := by
…
```