LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The double-plus-simple cubic surface branch terminates

Statement

Assume AC and DC. Let $A$ be a rational Gorenstein normal local surface in the permitted canonical-module setting, with normal completion and generators $m = (x, y, z)$ . If $z^{2} + a x y^{2} \in z m^{2} + (x, y)^{4}$ for a unit $a$ , all its singular point-blowup branches terminate. A continuing square branch has unchanged residue field and the same $x$ defining every successive exceptional divisor.

Facts & Assumptions

Given: A rational Gorenstein normal local surface $A$ in the permitted canonical-module setting with normal completion and generators $m = (x, y, z)$ such that $z^{2} + a x y^{2} \in z m^{2} + (x, y)^{4}$ for a unit $a$ .

[F1]

def-axiom-of-choice. The Axiom of Choice (AC) is the following statement. > Every family of nonempty sets has a choice function > (def-choice-function). Written out: for every set $F$ all of whose members are nonempty, there exists a function $g$ with domain $F$ satisfying $g (S) \in S$ for all $S \in F$ . (The Axiom of Choice)

[F2]

def-dependent-choice. Let $X$ be a set and let $R \subseteq X \times X$ be a binary relation on $X$ . Call $R$ entire on $X$ when $for every x \in X there is y \in X with x R y .$ The Axiom of Dependent Choice, written $D C$ , is the following statement. (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain)

[F3]

lem-rational-singular-point-blowup-canonical-pullback-surjective. Assume AC and DC. For a nonregular rational normal local surface domain in the permitted regular-base dualizing setting, let $f : X \to Spec A$ be its ordinary point blowup, $E$ its exceptional divisor and $I = O_{X} (1)$ . Then $H^{1} (X, ω_{X} \otimes I^{n}) = 0$ for $n \geq 0$ and the canonical evaluation $f^{*} ω_{A} \to ω_{X}$ is surjective. (Canonical pullback is surjective after blowing up a rational singular point)

[F4]

lem-rational-surface-local-rings-propagate-by-point-sequence-spreading. Assume AC and DC. If a permitted normal local surface domain $A$ is rational and $A \subset B$ is a normal two-dimensional local domain with the same fraction field, essentially of finite type over $A$ , then $B$ is rational. (Rationality propagates to birational local surface rings)

[F5]

lem-square-tangent-conic-blowup-singularities-controlled-by-a-cubic. Assume AC and DC. For a rational Gorenstein normal local surface singularity with square tangent conic, choose $m = (x_{1}, x_{2}, z)$ and a relation $z^{2} = \sum a_{i j k} x_{i} x_{j} x_{k}$ . There is a nonzero homogeneous cubic $H \in κ [X_{1}, X_{2}]$ whose zero scheme on the reduced exceptional line contains all singular successors. (A square-conic blowup has cubic-controlled singular successors)

[F6]

lem-nonsquare-tangent-conic-rational-surface-blowups-terminate. Assume AC and DC. For a nonregular rational normal local surface domain in the permitted class with invertible canonical module and normal completion, if its tangent-conic quadratic is not a scalar times a square, repeatedly blowing up its singular points terminates in a regular model. (Nonsquare tangent-conic surface singularities terminate under point blowups)

[F7]

A fixed-coordinate point-blowup chain defines a formal arc: under AC and DC, an equicharacteristic Noetherian local domain with an infinite chain of local point-blowup rings having the same residue field and one fixed $t \in m$ with $m_{n} B_{n + 1} = t B_{n + 1}$ admits a nonsingular formal arc extended from a surjection $\hat{A} \to V$ . Here $V$ is a complete DVR with that residue field, the image of $t$ is a uniformizer, and its point-blowup centers are the given ones.

[F8]

lem-normal-complete-surface-nonsingular-formal-arc-blowups-terminate. Assume AC and DC. Let $A$ be a normal Noetherian local domain of dimension two with a surjection onto a complete DVR $V$ inducing its residue-field identification. The successive point blowups along this nonsingular arc become regular at the arc centre after finitely many steps. (A nonsingular formal arc on a normal Noetherian surface becomes regular)

[F9]

lem-surface-regular-fibres-preserve-normality. Assume AC and DC. A flat map of Noetherian rings with regular fibres carries normality of the base to normality of the target. Consequently a normal essentially finite-type local ring over a field or complete equicharacteristic Noetherian local base has normal maximal-adic completion, which is a domain. (Surface regular fibres preserve normality)

[F10]

thm-blowup-base-change-flat. Assume the Axiom of Choice as inherited from the relative Proj construction. Let $g ⁣ : X^{'} \to X$ be a flat morphism of schemes and $I$ a quasi-coherent ideal sheaf of finite type on $X$ . (Flat base change for blowups, and failure without flatness)

[F11]

lem-surface-completion-base-change-preserves-closed-fibre-local-completions. Assume AC. Let $(A, m)$ be a Noetherian local ring, $\hat{A}$ its maximal-adic completion, and $X$ a scheme locally of finite type over $A$ . Put $Y = X \times_{Spec A} Spec \hat{A}$ . The closed fibres of $X$ and $Y$ are canonically isomorphic. (Completion base change preserves completed local rings on the closed fibre)

[F12]

thm-completion-preserves-regular-local-rings. Assume the Axiom of Choice (The Axiom of Choice). A nonzero Noetherian local ring $R$ is regular if and only if its maximal-adic completion $\hat{R}$ is regular. (completion preserves regular local rings)

[F13]

Rational normal surface singularities and bounded modification cohomology restricts the standing rational class to normal two-dimensional Noetherian local domains essentially of finite type over a field or complete equicharacteristic local base.

[F14]

The tangent conic of a rational Gorenstein surface singularity gives that the ordinary point blowup of a nonregular rational Gorenstein surface in the permitted setting is normal with trivial canonical module.

Proof

1.1F3F4F9F13F14given

The rational-domain definition puts $A$ essentially of finite type over a field or a complete equicharacteristic local base. In positive characteristic this forces both $A$ and its residue field to have that prime characteristic. In characteristic zero the base contains $Q$ : for a complete equicharacteristic local base every nonzero integer has nonzero residue and is a unit. Its images remain units in $A$ and every residue field. Hence $A$ is equicharacteristic; this premise comes from the rationality class. At each singular step the ordinary point blowup is normal with trivial canonical module. Each singular successor is a two-dimensional local domain essentially of finite type over $A$ , with the same fraction field. Rationality propagates by the modification supplier, and the successor remains in the same base class, so the regular-fibre normality supplier gives its normal completion. Thus every singular successor remains rational Gorenstein in the same permitted setting.

2.1F5givenstep 1.1

Absorbing the terms $z^{2} m$ into the unit coefficient and dividing by it turns the hypothesis into the exact relation $z^{2} + a x y^{2} + b x^{2} z + c x y z + d y^{2} z + e x^{4} + f x^{3} y + g x^{2} y^{2} + h x y^{3} + i y^{4} = 0$ ; the reduced controlling cubic is $\overset{ˉ}{a} X Y^{2}$ , whose simple zero $X = 0$ has a nonsquare successor resolved by the nonsquare lemma, while its only possible continuing square successor is the $κ$ -rational point $u = y / x = v = z / x = 0$ of the $x$ -chart.

3.1F6step 2.1

In the $x$ -chart put $u = y / x$ , $v = z / x$ ; dividing the exact relation by $x^{2}$ gives $v^{2} + a x u^{2} + b x v + c x u v + d x u^{2} v + e x^{2} + f x^{2} u + g x^{2} u^{2} + h x^{2} u^{3} + i x^{2} u^{4} = 0$ , whose successor quadratic is $P (X, V) = V^{2} + \overset{ˉ}{b} X V + \overset{ˉ}{e} X^{2}$ ; if $P$ is nonsquare the nonsquare-conic termination lemma applies to that successor.

4.1F5step 3.1

If $P$ is a square, choose $δ \in A$ lifting its residue square coefficient with $\overset{ˉ}{b} = 2 \overset{ˉ}{δ}$ and $\overset{ˉ}{e} = {\overset{ˉ}{δ}}^{2}$ (valid in every characteristic, with no division by two), put $w = v + δ x$ , and set $b^{'} = b - 2 δ \in m$ , $e^{'} = e - b δ + δ^{2} \in m$ , so $b^{'} = x B$ and $e^{'} = x E$ on the chart. Substitution gives $w^{2} + a x u^{2} + c x u w + d x u^{2} w + x^{2} [B w + (f - c δ) u + (g - d δ) u^{2} + h u^{3} + i u^{4}] + x^{3} (E - δ B) = 0$ . Its cubic modulo $w$ is $C (X, U) = X (\overset{ˉ}{a} U^{2} + ρ X U + σ X^{2})$ with $\overset{ˉ}{a} \neq 0$ . The zero $X = 0$ is simple; a multiple closed zero means a repeated prime factor over $κ$ , so its degree is one and there is at most one. It is at $(X : U) = (1 : ε)$ with $ε \in κ$ , characterized by $\overset{ˉ}{a} ε^{2} + ρ ε + σ = 0$ and $2 \overset{ˉ}{a} ε + ρ = 0$ .

5.1F4step 4.1

Replacing $u$ by $u - ε x$ leaves $x$ unchanged, keeps the tangent square $w^{2}$ , changes the cubic restriction to $\overset{ˉ}{a} X u^{2}$ , and puts all remaining cubic terms in $w (m^{'})^{2}$ and all higher terms in $w (m^{'})^{2} + (x, u)^{4}$ ; hence the successor again satisfies the invariant $z^{2} + a x y^{2} \in z m^{2} + (x, y)^{4}$ with unit coefficient, and every continuing square step uses the $x$ -chart, has the same residue field $κ$ , and has the same element $x$ generating the pullback of its centre ideal.

6.1F7F8F9step 1.1step 5.1

If the continuing branch were infinite, the fixed-coordinate helper would produce a nonsingular formal arc, that is a surjection from the completion of $A$ onto a complete discrete valuation ring with uniformizer the image of $x$ and the given centres. The completion is a normal Noetherian local domain of dimension two, so the formal-arc termination helper makes its point blowups regular at the arc centre after finitely many steps.

7.1F6F10F11F12step 6.1

Blowup flat base change identifies the completed blowups with the blowups of the completion, and equality of the closed-fibre local completions together with preservation and reflection of regularity by completion transfers that regularity back to the original chain, contradicting an infinite singular branch; all simple-root side branches terminate by the nonsquare lemma, so all singular point-blowup branches of this class terminate.

8.1F1F2step 7.1∎

The Axiom of Choice and the Axiom of Dependent Choice are inherited from the cited suppliers; the exact coefficient expansions and the chart normalization above involve no division by two or three.

Remarks

The invariant (S) is broader than the earlier restrictive persistence class: terms like $x^{2} z$ and $y^{2} z$ are retained throughout.
The same element $x$ defines every centre in a continuing square branch, which is exactly what the fixed-coordinate arc helper needs.

Depends on

Used by

Dependency tree · two levels

72 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Joseph Lipman, Rational singularities (1969), §24, pp.264–268, relations (5)/(5′): full text read; omitted chart details proved locally (standard reference, not scraped)
Joseph Lipman, Desingularization of two-dimensional schemes (1978), pp.171–174, (1.29) and fixed-coordinate termination (standard reference, not scraped)