Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6-sol)audited 2026-09-27
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.

A cuspidal plane curve is standard smooth away from the cusp

Example

Let k be a field of characteristic different from two and let A=k[x,y]/(y2−x3), with y denoting the class of the variable. Then S=Ay is a standard smooth k-algebra of relative dimension one, presented by the single equation y2−x3 in the variables y,x with the 1×1 minor ∂(y2−x3)∂y=2y, which is a unit of S because y is inverted and 2≠0 in k. The chart therefore covers the open set D(y) of the cuspidal curve; at the origin ∂yf=2y and ∂xf=−3x2 both vanish, so this single equation exhibits no invertible minor there.

Facts & Assumptions

Given: A field k with 2≠0, the polynomial ring k[x,y], the element f=y2−x3, the quotient A=k[x,y]/(f) and the localisation S=Ay at the powers of the class y.

[F1]

Standard smooth presentations and locally standard smooth maps: a standard smooth presentation of an R-algebra S consists of n≥c≥0, equations f1,…,fc∈R[x1,…,xn] and g with S≅(R[x1,…,xn]/(f1,…,fc))g such that some c×c Jacobian minor has image a unit of S; n−c is the relative dimension, and the invertible minor may be assumed to be the leading one in the first c columns.

[F2]

Differentials of a polynomial quotient and the Jacobian cokernel: for k[x,y] the partial derivatives are computed on the monomial basis, df=∂xf dx+∂yf dy, and (∂xf,∂yf) is the Jacobian row governing the cokernel presentation of Ωk[x,y]/(f)/k; no injectivity of the conormal map is asserted.

Verification

1.1

The chart on D(y). Take R=k, n=2, c=1, the ordered variables (x1,x2)=(y,x), the equation f1=y2−x3 and g=y; then S=Ay≅(k[x1,x2]/(f1))g by construction [F1]. By [F2] the Jacobian row of the single equation is (∂yf,∂xf)=(2y,−3x2), and its first entry is 2y, a product of the unit 2∈k and the unit y of S=Ay; hence the leading 1×1 minor is a unit of S and the presentation is standard smooth of relative dimension 2−1=1. This proves the claim on the whole open set D(y)={y≠0}⊆Spec⁡A.

F1F2algebra
2.1

Complements. The hypothesis on the characteristic is exactly what the unit computation uses: if 2=0 in k then 2y=0 is not a unit of S. At the origin both partial derivatives 2y and −3x2 vanish, so the displayed single equation gives no invertible minor there, and the chart of step 1.1 covers precisely the points with y≠0, not the cusp at the origin.

F2step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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