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.

A localization of the integers at p need not be Henselian

Example

The local ring $Z_{(7)}$ is not Henselian.

Facts & Assumptions

Given: The localization $A = Z_{(7)}$ and the polynomial $f (T) = T^{2} - 2 \in A [T]$ .

[L1]

The localization at the prime $(7)$ is a local ring ( $R_{p}$ is local with unique maximal ideal $p R_{p}$ ).

[L2]

Its residue field is $F_{7}$ ( $R_{p} / p R_{p} ≅ Frac (R / p)$ is the residue field at $p$ , For every prime $p$ , the two operations on $Z / p$ make it a field).

[L3]

In a Henselian local ring, every simple residue root lifts (A local ring is Henselian exactly when simple residue roots lift uniquely).

Verification

technique · find a simple residue root that has no lift

1.1

By [L1] and [L2], the ring $A = Z_{(7)}$ is local with residue field $F_{7}$ . In that field, $\overline{f} (3) = 3^{2} - 2 = 7 \equiv 0 (m o d 7), {\overline{f}}^{'} (3) = 2 \cdot 3 = 6 \equiv̸ 0 (m o d 7),$ so $3$ is a simple residue root.

L1L2givenalgebra

2.1

Suppose $a / b \in Z_{(7)}$ with $7 ∤ b$ satisfies $(a / b)^{2} = 2$ . Then $a^{2} = 2 b^{2}$ in $Z$ . The $2$ -adic valuation of the left side is even, while the valuation of the right side is odd, impossible. Hence $2$ has no square root in $Q$ , and therefore no root in $Z_{(7)}$ .

step 1.1givenassume-contraalgebradischarge-contradiction

3.1

The simple residue root from step 1.1 does not lift, so [L3] shows that $A$ cannot be Henselian.

L3step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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

Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Chapter 22 (standard reference, not scraped)