Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04
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.

Coefficient fields need not be unique

Example

Let k be a field and let u be transcendental over k. In the complete local ring A=k(u)t, the obvious coefficient field k(u) is not the only one: the translated field k(u+t) is a different coefficient field with the same residue image.

Facts & Assumptions

Given: The complete local ring A=k(u)t.

[L1]

A formal power-series ring over a field is a local domain with maximal ideal generated by the indeterminate (For a field K, Kx is a domain and its nonunits form the unique maximal ideal xKx).

[L2]

Complete equicharacteristic local rings have coefficient fields (Complete equicharacteristic local rings have coefficient fields).

Verification

technique · compare the obvious coefficient field with a translated one
1.1

By [L1], A is local with maximal ideal (t) and residue field A/(t)k(u). The standard inclusion of k(u) into A is therefore a coefficient field, in line with [L2].

L1L2given
2.1

Consider the subfield K=k(u+t)A. For every nonzero polynomial q(Z)k[Z], the residue of q(u+t) modulo t is q(u), which is nonzero in k(u). Hence q(u+t) is a unit of A, so every rational function in u+t lies in A and K is indeed a subfield. Its residue image is again k(u) because u+tu.

L1step 1.1algebra
3.1

The two coefficient fields are distinct: if u+t lay in the constant field k(u), then subtracting u would place t in k(u), but every nonzero element of k(u) is a unit in A whereas t lies in the maximal ideal. Thus k(u+t)k(u).

L1step 2.1algebra
4.1

Therefore coefficient fields in a complete equicharacteristic local ring need not be canonical.

step 1.1step 3.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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