DeterminantLeadingReduction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Leading locally nilpotent reduction on the actual determinant ring

This is the auxiliary-grading step in the source's rigidity argument. The input is a nonzero locally nilpotent derivation on the concrete determinant quotient preserving fiber weights and killing the exact obstruction v. The output is a nonzero locally nilpotent derivation with the same fiber weight property fixing a, d, and u. All finite generation, grading, domain, characteristic, and nonvanishing premises are discharged for this quotient; none is added to the conclusion as an unproved interface.

theorem OAI.StableCoordinate.Obstruction.exists_nonzero_lnd_fixing_a_d_u line 32
Source documentation
The actual leading-component reduction in the determinant quotient.
Auxiliary degrees -1 and 2 of the two parts of v are kept separate, and compatibility with the second grading retains the fiber weights. Factorial closure then splits the nonzero difference-of-squares factors.
```
theorem exists_nonzero_lnd_fixing_a_d_u
    (D : Derivation k (C k) (C k))
    (hD : D ≠ 0) (hln : IsLocallyNilpotent D)
    (hpres : ∀ (n : ℤ) (x : C k), x ∈ fiberPiece k n → D x ∈ fiberPiece k n)
    (hv : D (v k) = 0) :
    ∃ E : Derivation k (C k) (C k), E ≠ 0 ∧ IsLocallyNilpotent E ∧
      (∀ (n : ℤ) (x : C k), x ∈ fiberPiece k n → E x ∈ fiberPiece k n) ∧
      E (cX k 0) = 0 ∧ E (cX k 1) = 0 ∧ E (cX k 4) = 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.IsLocallyNilpotent, OAI.StableCoordinate.Obstruction.fiberPiece, OAI.StableCoordinate.Obstruction.v, OAI.StableCoordinate.Obstruction.cX