StabilizationEmbedding.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The added variable is a genuine polynomial indeterminate

The target encodes R[w] as a polynomial algebra on five independent variables. Here that encoding is identified with the literal univariate polynomial ring over R 4, fixing all original variables. Conjugating algebra automorphisms through this equivalence shows that the target's stabilization criterion is exactly the one in the source, with no condition that the automorphism preserve the coefficient subring.

def OAI.StableCoordinate.stabilizationEquiv line 23
Source documentation
The last of five independent variables becomes the new indeterminate; the first four become coefficient variables.
```
noncomputable def stabilizationEquiv : R 5 ≃ₐ[ℂ] Polynomial (R 4) :=
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.stabilizationEquiv_X_castSucc line 28
theorem OAI.StableCoordinate.stabilizationEquiv_X_last line 33
theorem OAI.StableCoordinate.stabilizationEquiv_stabilize line 40
theorem OAI.StableCoordinate.stabilizationEquiv_symm_C line 49
theorem OAI.StableCoordinate.stabilize_injective line 55
Source documentation
Adjoining the variable does not identify distinct original polynomials.
```
theorem stabilize_injective : Function.Injective stabilize := by
…
```
Mentions: OAI.StableCoordinate.stabilize
theorem OAI.StableCoordinate.last_variable_not_mem_stabilize_range line 61
Source documentation
The added variable is not already in the original four-variable subring.
```
theorem last_variable_not_mem_stabilize_range :
    (X 4 : R 5) ∉ Set.range stabilize := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.stabilize
theorem OAI.StableCoordinate.isOneStableCoordinate_iff_polynomial line 71
Source documentation
Exact compatibility between the five-variable encoding and the literal R[w] automorphism criterion. Both automorphisms are arbitrary complex algebra automorphisms, not coefficient-algebra automorphisms.
```
theorem isOneStableCoordinate_iff_polynomial (g : R 4) :
    IsOneStableCoordinate g ↔
      ∃ φ : Polynomial (R 4) ≃ₐ[ℂ] Polynomial (R 4),
        φ (Polynomial.C g) = Polynomial.C (X 0) := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.IsOneStableCoordinate