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.
Simple-root lifting and factor lifting produce the same root
Example
For the polynomial the residue class is a simple root of . Lifting that root directly or by first lifting the factor produces the same root.
Facts & Assumptions
Given: The complete local ring and the polynomial .
Complete local rings are Henselian (Complete local rings are Henselian).
In a Henselian local ring, every simple residue root lifts uniquely (Factor lifting implies simple-root lifting).
A Henselian local ring has the unique coprime factor-lifting property (Henselian pairs and Henselian local rings).
Verification
By [L1], the complete local ring is Henselian. Modulo , one has , so is a simple root. By [L2], there is a unique root with and . The first two correction stages give
The residue factorization is monic and coprime, so [L3] gives a factorization with . Evaluating at gives , so is another lift of the same simple residue root.
By uniqueness in [L2], one has . Equivalently, the root obtained from the lifted linear factor is exactly the same root obtained from the simple-root lifting procedure.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
7 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
- The Stacks Project, Section 10.153: Henselian local rings (standard reference, not scraped)