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, K⟦x⟧ is a domain and its nonunits form the unique maximal ideal xK⟦x⟧).

[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.1L1L2given

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].

2.1L1step 1.1algebra

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+t↦u.

3.1L1step 2.1algebra

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).

4.1step 1.1step 3.1∎

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

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