CandidateRing.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The completed surface cone

The explicit Kummer surface construction of OpenAI's A Complete Local Domain without a Small Cohen–Macaulay Module (2026) gives a complete normal Noetherian local domain of dimension three over ℂ.

theorem OAI.SmallCM.candidate_ring_properties line 16
Source documentation
Ring-theoretic properties of the completed surface cone.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, CommRing, IsDomain, IsNoetherianRing, IsIntegrallyClosed, IsLocalRing, Algebra, Complex, And, IsAdicComplete, IsLocalRing.maximalIdeal, Eq, WithBot, ENat, ringKrullDim, OfNat.ofNat, Nat, Function.Bijective, IsLocalRing.ResidueField, RingHom and 1 more
Proof uses: Subtype, PowerSeries, AlgebraicClosure, OAI.KummerLines.K, OAI.KummerLines.R, Finsupp, Fin, Membership.mem, IntermediateField, OAI.ExplicitCone.L, Subalgebra, Unit, nonZeroDivisors, OAI.ExplicitCone.completedRing, OAI.ExplicitCone.actualCompletion_noetherian, Exists.intro, inferInstance, And.intro, OAI.ExplicitCone.completedRing_dimension, OAI.ExplicitCone.completedRing_residue_bijective
93 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: ComparatorChallenges/SurfaceConeCandidateSupport.lean:8 (same statement text; different proof or body). Qualify references as OAI.SmallCM.candidate_ring_properties@path.
Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem candidate_ring_properties :
    ∃ (R : Type) (_ : CommRing R) (_ : IsDomain R) (_ : IsNoetherianRing R)
      (_ : IsIntegrallyClosed R) (_ : IsLocalRing R) (_ : Algebra ℂ R),
      IsAdicComplete (IsLocalRing.maximalIdeal R) R ∧
      ringKrullDim R = 3 ∧
      Function.Bijective (algebraMap ℂ (IsLocalRing.ResidueField R)) := by
…
```