NonnegativeWeights.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Nonnegative polynomial weights

The final step of the source rigidity argument uses the weights (1, 1, 0) on the algebraically independent generators a, d, u. This module proves that the resulting polynomial algebra has no nonzero homogeneous elements of negative weight. It does not assume or assert the geometric interfaces needed to identify this polynomial algebra inside the source quotient.

theorem OAI.StableCoordinate.monomial_weight_nonneg line 26
Source documentation
A monomial has nonnegative integral weight when all variable weights are nonnegative. Variables of weight zero are allowed.
```
theorem monomial_weight_nonneg (w : σ → ℤ) (hw : ∀ i, 0 ≤ w i)
    (d : σ →₀ ℕ) : 0 ≤ Finsupp.weight w d := by
…
```

theorem OAI.StableCoordinate.homogeneous_weight_nonneg line 34

Source documentation

Every nonzero homogeneous polynomial for nonnegative variable weights has nonnegative weight.

theorem homogeneous_weight_nonneg {w : σ → ℤ} (hw : ∀ i, 0 ≤ w i)
    {p : MvPolynomial σ K} (hp : p ≠ 0) {n : ℤ}
    (hn : p.IsWeightedHomogeneous w n) : 0 ≤ n := by
…

theorem OAI.StableCoordinate.eq_zero_of_homogeneous_negative line 43
Source documentation
No polynomial supported on nonnegative variable weights can be nonzero and homogeneous of negative weight.
```
theorem eq_zero_of_homogeneous_negative {w : σ → ℤ} (hw : ∀ i, 0 ≤ w i)
    {p : MvPolynomial σ K} {n : ℤ}
    (hn : p.IsWeightedHomogeneous w n) (hneg : n < 0) : p = 0 := by
…
```

theorem OAI.StableCoordinate.homogeneousComponent_negative line 50

Source documentation

The negative homogeneous components all vanish.

theorem homogeneousComponent_negative {w : σ → ℤ} (hw : ∀ i, 0 ≤ w i)
    (p : MvPolynomial σ K) {n : ℤ} (hneg : n < 0) :
    MvPolynomial.weightedHomogeneousComponent w n p = 0 := by
…

def OAI.StableCoordinate.rigidityPolynomialWeight line 61
Source documentation
The weights of the source polynomial subalgebra k[a,d,u]: index 0 is a, index 1 is d, and index 2 is u.
```
def rigidityPolynomialWeight (i : Fin 3) : ℤ := if i = 2 then 0 else 1
```
theorem OAI.StableCoordinate.rigidityPolynomialWeight_nonneg line 63
theorem OAI.StableCoordinate.rigidity_polynomial_weight_neg_two line 70
Source documentation
The precise impossibility used for the coefficient q in source §5: a polynomial in a,d,u of fiber weight -2 must vanish.
```
theorem rigidity_polynomial_weight_neg_two {K : Type*} [CommSemiring K]
    {q : MvPolynomial (Fin 3) K}
    (hq : q.IsWeightedHomogeneous rigidityPolynomialWeight (-2)) : q = 0 := by
…
```
Mentions: OAI.StableCoordinate.rigidityPolynomialWeight
theorem OAI.StableCoordinate.no_nonzero_rigidity_polynomial_weight_neg_two line 76
Source documentation
Contradiction form for the final source rigidity step.
```
theorem no_nonzero_rigidity_polynomial_weight_neg_two {K : Type*} [CommSemiring K]
    (q : MvPolynomial (Fin 3) K) (hq : q ≠ 0) :
    ¬ q.IsWeightedHomogeneous rigidityPolynomialWeight (-2) := by
…
```
Mentions: OAI.StableCoordinate.rigidityPolynomialWeight