Stabilization.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Stabilization assembly

The exponential shift is transported through the principal hypersurface ideal. The final assembly will combine this with the polynomial presentation and the linear elimination isomorphisms. No statement here assumes the principal target.

def OAI.StableCoordinate.Stabilization.presentationIdeal line 22
def OAI.StableCoordinate.Stabilization.shiftedIdeal line 25
abbrev OAI.StableCoordinate.Stabilization.PresentationRing line 28
abbrev OAI.StableCoordinate.Stabilization.ShiftedRing line 29
def OAI.StableCoordinate.Stabilization.shiftQuotientEquiv line 32
Source documentation
The explicit exponential substitution identifies the two hypersurface rings.
```
noncomputable def shiftQuotientEquiv : PresentationRing ≃ₐ[ℂ] ShiftedRing :=
…
```
Mentions: OAI.StableCoordinate.Stabilization.PresentationRing, OAI.StableCoordinate.Stabilization.ShiftedRing
theorem OAI.StableCoordinate.Stabilization.shiftQuotientEquiv_mk line 43
theorem OAI.StableCoordinate.Stabilization.shiftQuotientEquiv_p line 47
def OAI.StableCoordinate.Stabilization.normalizationQuotientEquiv line 56
Source documentation
Normalize the shifted equation to the monic linear equation F-u+p*w.
```
noncomputable def normalizationQuotientEquiv : ShiftedRing ≃ₐ[ℂ] StabilizedQuotient.A :=
…
```
Mentions: OAI.StableCoordinate.Stabilization.ShiftedRing, OAI.StableCoordinate.StabilizedQuotient.A
theorem OAI.StableCoordinate.Stabilization.normalizationQuotientEquiv_mk line 66
def OAI.StableCoordinate.Stabilization.eliminateQuotientEquiv line 72
Source documentation
The shifted hypersurface is a five-variable polynomial ring, with p as its first coordinate. This is the explicit final variable elimination.
```
noncomputable def eliminateQuotientEquiv : ShiftedRing ≃ₐ[ℂ] R 5 :=
…
```
Mentions: OAI.StableCoordinate.Stabilization.ShiftedRing, OAI.StableCoordinate.R
theorem OAI.StableCoordinate.Stabilization.eliminateQuotientEquiv_p line 75
def OAI.StableCoordinate.Stabilization.stablePresentationEquiv line 81
Source documentation
The original presented hypersurface, after adjoining w, is a polynomial ring in which the distinguished p is the first coordinate.
```
noncomputable def stablePresentationEquiv : PresentationRing ≃ₐ[ℂ] R 5 :=
…
```
Mentions: OAI.StableCoordinate.Stabilization.PresentationRing, OAI.StableCoordinate.R
theorem OAI.StableCoordinate.Stabilization.trans_apply_eq line 84
theorem OAI.StableCoordinate.Stabilization.stablePresentationEquiv_p line 91
theorem OAI.StableCoordinate.Stabilization.oneStable_of_presentations line 100
Source documentation
Composition interface: two polynomial presentations of the same algebra, with the specified images of one element, produce the required automorphism. This is only a supporting theorem; its hypotheses must be discharged by the explicit presentation and elimination constructions.
```
theorem oneStable_of_presentations {A : Type*} [CommRing A] [Algebra ℂ A]
    (p : A) (present eliminate : A ≃ₐ[ℂ] R 5)
    (hpresent : present p = stabilize f) (heliminate : eliminate p = X 0) :
    IsOneStableCoordinate f := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.stabilize, OAI.StableCoordinate.f, OAI.StableCoordinate.IsOneStableCoordinate
theorem OAI.StableCoordinate.f_isOneStableCoordinate line 112
Source documentation
The exact degree-five polynomial of the paper is a coordinate after adjoining one independent variable. The witnessing automorphism is built from explicit matrix, exponential, and linear/shear polynomial substitutions.
```
theorem f_isOneStableCoordinate : IsOneStableCoordinate f := by
…
```
Mentions: OAI.StableCoordinate.IsOneStableCoordinate, OAI.StableCoordinate.f