Principal.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The stable noncoordinate polynomial and its fibers

The degree-five polynomial becomes a coordinate after adjoining one variable but is not a coordinate in four variables. Every complex fiber is affine three-space and has a nonrectifiable embedding in affine four-space.

theorem OAI.StableCoordinate.polynomial_package line 22
Source documentation
The exact polynomial has degree five, is one-stable, and is not a coordinate in its original four-variable polynomial algebra.
```
theorem polynomial_package : PolynomialPackage :=
…
```
Mentions: OAI.StableCoordinate.PolynomialPackage
theorem OAI.StableCoordinate.fiber_package line 27
Source documentation
Every complex fiber is affine three-space and its embedding in affine four-space is nonrectifiable.
```
theorem fiber_package : FiberPackage :=
…
```
Mentions: OAI.StableCoordinate.FiberPackage
theorem OAI.StableCoordinate.principal_package line 31
Source documentation
Both complete principal groups, with every required quantifier.
Distinct definitions of this name: ComparatorChallenges/StableCoordinateFour.lean:49 (same statement text; different proof or body). Qualify references as OAI.StableCoordinate.principal_package@path.
```
theorem principal_package : PrincipalPackage :=
…
```
Mentions: OAI.StableCoordinate.PrincipalPackage
theorem OAI.StableCoordinate.f_is_coordinate_in_polynomial_extension line 35
Source documentation
Literal polynomial-extension form of the unrestricted stabilization.
```
theorem f_is_coordinate_in_polynomial_extension :
    ∃ φ : Polynomial (R 4) ≃ₐ[ℂ] Polynomial (R 4),
      φ (Polynomial.C f) = Polynomial.C (MvPolynomial.X 0) :=
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.f
theorem OAI.StableCoordinate.stable_coordinate_conjecture_four_false line 42
Source documentation
The exact example disproves the stable-coordinate statement for four original variables and one independent added variable over ℂ.
```
theorem stable_coordinate_conjecture_four_false :
    ¬ (∀ g : R 4, IsOneStableCoordinate g →
      IsCoordinate (by decide : 0 < 4) g) := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.IsOneStableCoordinate, OAI.StableCoordinate.IsCoordinate
theorem OAI.StableCoordinate.abhyankar_sathaye_statement_four_false line 51
Source documentation
The dimension-four Abhyankar–Sathaye statement over ℂ fails for this exact polynomial. Its zero fiber already supplies the required counterexample; the stronger all-fiber statement is fiber_package.
```
theorem abhyankar_sathaye_statement_four_false :
    ¬ (∀ g : R 4,
      Nonempty ((R 4 ⧸ Ideal.span ({g} : Set (R 4))) ≃ₐ[ℂ] R 3) →
      IsCoordinate (by decide : 0 < 4) g) := by
…
```
Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.IsCoordinate
theorem OAI.StableCoordinate.all_fibers_geometric_conclusion line 69
Source documentation
The all-fiber result as actual schemes over Spec ℂ, with the actual closed hypersurface immersion and obstruction to every base-preserving ambient scheme automorphism. This is not merely a statement about sets of points.
```
theorem all_fibers_geometric_conclusion :
    ∀ t : ℂ,
      Nonempty (AffineGeometry.algebraSpec ℂ (FiberRing t) ≅
        Over.mk (AffineSpace (Fin 3) (Spec (CommRingCat.of ℂ)) ↘
          Spec (CommRingCat.of ℂ))) ∧
      IsClosedImmersion (GeometricInterpretation.fiberEmbedding t) ∧
      ¬ GeometricInterpretation.IsSchemeRectifiableFiber t :=
…
```
Mentions: OAI.StableCoordinate.AffineGeometry.algebraSpec, OAI.StableCoordinate.FiberRing, OAI.StableCoordinate.GeometricInterpretation.fiberEmbedding, OAI.StableCoordinate.GeometricInterpretation.IsSchemeRectifiableFiber