Linearization.lean`

41 declarations, 0 contain sorry, 0 declared as axioms

The determinant-one linear substitution in the stabilization construction

This module formalizes the L,N change of variables in Section 2 of the source. It uses six genuinely independent polynomial generators, in the order p,s,u,F,J,w. All results hold over any commutative coefficient ring.

abbrev OAI.StableCoordinate.Linearization.P line 21
def OAI.StableCoordinate.Linearization.x0 line 24
Source documentation
The part of the auxiliary quadratic not containing p.
```
def x0 : P k := X 1 ^ 2 - X 2 ^ 2
```
Mentions: OAI.StableCoordinate.Linearization.P
def OAI.StableCoordinate.Linearization.l line 27
Source documentation
The first new linear coordinate, denoted L in the manuscript.
```
def l : P k := x0 k ^ 2 * X 3 - (1 + 2 * X 1 * x0 k) * X 4
```
Mentions: OAI.StableCoordinate.Linearization.P, OAI.StableCoordinate.Linearization.x0
def OAI.StableCoordinate.Linearization.n line 30
Source documentation
The second new linear coordinate, denoted N in the manuscript.
```
def n : P k := (1 - 2 * X 1 * x0 k) * X 3 + 4 * X 1 ^ 2 * X 4
```
Mentions: OAI.StableCoordinate.Linearization.P, OAI.StableCoordinate.Linearization.x0
def OAI.StableCoordinate.Linearization.inverseF line 33
Source documentation
The inverse formula for F in terms of the slots now called L,N.
```
def inverseF : P k := 4 * X 1 ^ 2 * X 3 + (1 + 2 * X 1 * x0 k) * X 4
```
Mentions: OAI.StableCoordinate.Linearization.P, OAI.StableCoordinate.Linearization.x0
def OAI.StableCoordinate.Linearization.inverseJ line 36
Source documentation
The inverse formula for J in terms of the slots now called L,N.
```
def inverseJ : P k := -(1 - 2 * X 1 * x0 k) * X 3 + x0 k ^ 2 * X 4
```
Mentions: OAI.StableCoordinate.Linearization.P, OAI.StableCoordinate.Linearization.x0
def OAI.StableCoordinate.Linearization.forward line 39
Source documentation
Substitution F ↦ L, J ↦ N, fixing the other four generators.
```
def forward : P k →ₐ[k] P k :=
…
```
Mentions: OAI.StableCoordinate.Linearization.P
def OAI.StableCoordinate.Linearization.backward line 43
Source documentation
The inverse determinant-one substitution.
```
def backward : P k →ₐ[k] P k :=
…
```
Mentions: OAI.StableCoordinate.Linearization.P
theorem OAI.StableCoordinate.Linearization.forward_X line 46
theorem OAI.StableCoordinate.Linearization.backward_X line 50
theorem OAI.StableCoordinate.Linearization.forward_x0 line 54
theorem OAI.StableCoordinate.Linearization.backward_x0 line 57
theorem OAI.StableCoordinate.Linearization.backward_comp_forward line 60
theorem OAI.StableCoordinate.Linearization.forward_comp_backward line 64
def OAI.StableCoordinate.Linearization.equiv line 69
Source documentation
The exact determinant-one L,N change is a polynomial algebra automorphism.
```
def equiv : P k ≃ₐ[k] P k :=
…
```
Mentions: OAI.StableCoordinate.Linearization.P
theorem OAI.StableCoordinate.Linearization.equiv_apply line 73
theorem OAI.StableCoordinate.Linearization.equiv_symm_apply line 75
def OAI.StableCoordinate.Linearization.x line 78
Source documentation
The source's auxiliary quadratic including p F.
```
def x : P k := x0 k + X 0 * X 3
```
Mentions: OAI.StableCoordinate.Linearization.P, OAI.StableCoordinate.Linearization.x0
def OAI.StableCoordinate.Linearization.h line 81
Source documentation
The source hypersurface relation, extended by the independent variable w.
```
def h : P k := x k ^ 2 * X 3 - (1 + 2 * X 1 * x k) * X 4 - X 0 * X 4 ^ 2 - X 2
```
Mentions: OAI.StableCoordinate.Linearization.P, OAI.StableCoordinate.Linearization.x
def OAI.StableCoordinate.Linearization.q0 line 84
Source documentation
The polynomial remainder Q₀ in the source equation H = L-u+p Q₀.
```
def q0 : P k := 2 * x0 k * X 3 ^ 2 + X 0 * X 3 ^ 3 - 2 * X 1 * X 3 * X 4 - X 4 ^ 2
```
Mentions: OAI.StableCoordinate.Linearization.P, OAI.StableCoordinate.Linearization.x0
theorem OAI.StableCoordinate.Linearization.h_expansion line 87
Source documentation
The divisibility identity used to remove the nonlinear remainder.
```
theorem h_expansion : h k = l k - X 2 + X 0 * q0 k := by
…
```
Mentions: OAI.StableCoordinate.Linearization.h, OAI.StableCoordinate.Linearization.l, OAI.StableCoordinate.Linearization.q0
def OAI.StableCoordinate.Linearization.qTrans line 92
Source documentation
Q₀ written in the new linear coordinates.
```
def qTrans : P k :=
…
```
Mentions: OAI.StableCoordinate.Linearization.P
theorem OAI.StableCoordinate.Linearization.backward_q0 line 96
theorem OAI.StableCoordinate.Linearization.backward_l line 99
theorem OAI.StableCoordinate.Linearization.backward_n line 103
theorem OAI.StableCoordinate.Linearization.backward_h line 108
Source documentation
The source equation after the inverse L,N substitution.
```
theorem backward_h : backward k (h k) = X 3 - X 2 + X 0 * qTrans k := by
…
```
Mentions: OAI.StableCoordinate.Linearization.backward, OAI.StableCoordinate.Linearization.h, OAI.StableCoordinate.Linearization.qTrans
def OAI.StableCoordinate.Linearization.minusShear line 113
Source documentation
Subtract the transformed remainder from the independent new variable.
```
def minusShear : P k →ₐ[k] P k :=
…
```
Mentions: OAI.StableCoordinate.Linearization.P
def OAI.StableCoordinate.Linearization.plusShear line 117
Source documentation
Inverse shear, adding the transformed remainder.
```
def plusShear : P k →ₐ[k] P k :=
…
```
Mentions: OAI.StableCoordinate.Linearization.P
theorem OAI.StableCoordinate.Linearization.minusShear_X line 120
theorem OAI.StableCoordinate.Linearization.plusShear_X line 124
theorem OAI.StableCoordinate.Linearization.minusShear_qTrans line 128
theorem OAI.StableCoordinate.Linearization.plusShear_qTrans line 131
theorem OAI.StableCoordinate.Linearization.plusShear_comp_minusShear line 134
theorem OAI.StableCoordinate.Linearization.minusShear_comp_plusShear line 139
def OAI.StableCoordinate.Linearization.shearEquiv line 145
Source documentation
The independent-variable shear is a polynomial algebra automorphism.
```
def shearEquiv : P k ≃ₐ[k] P k :=
…
```
Mentions: OAI.StableCoordinate.Linearization.P
theorem OAI.StableCoordinate.Linearization.shearEquiv_apply line 149
def OAI.StableCoordinate.Linearization.normalization line 153
Source documentation
The full linearization automorphism, turning H+p w into an equation linear in the slot formerly called F, while fixing p.
```
def normalization : P k ≃ₐ[k] P k :=
…
```
Mentions: OAI.StableCoordinate.Linearization.P
theorem OAI.StableCoordinate.Linearization.normalization_p line 156
theorem OAI.StableCoordinate.Linearization.normalization_s line 159
theorem OAI.StableCoordinate.Linearization.normalization_u line 162
theorem OAI.StableCoordinate.Linearization.normalization_stabilized_h line 166
Source documentation
The exact polynomial equation needed for the final variable elimination.
```
theorem normalization_stabilized_h :
    normalization k (h k + X 0 * X 5) = X 3 - X 2 + X 0 * X 5 := by
…
```
Mentions: OAI.StableCoordinate.Linearization.normalization, OAI.StableCoordinate.Linearization.h