CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

$F_{p} (s, t) / F_{p} (s^{p}, t^{p})$ has degree $p^{2}$ , infinitely many intermediate fields, and no primitive element

Statement refuted

Every finite purely inseparable extension is simple.

Facts & Assumptions

Given: A prime $p$ , the field $F = F_{p} (s^{p}, t^{p})$ , and $E = F_{p} (s, t)$ .

[L1]

For every field $k$ , the rational function field $k (u)$ is the fraction field of $k [u]$ (For a field $F$ , $F (t) = Frac (F [t])$ is its rational function field; in particular $R (t) = Frac (R [t])$ ).

[L2]

A polynomial ring over a field is a unique factorization domain (For every field $F$ , $F [x]$ is a unique factorisation domain).

[L3]

In an exponent-one purely inseparable extension, a minimal generating family of length $r$ gives degree $p^{r}$ and the restricted-monomial basis (A minimal generating family in a finite exponent-one purely inseparable extension is a $p$ -basis and gives degree $p^{r}$ ).

[L4]

A finite extension is simple exactly when it has finitely many intermediate fields (A finite field extension is simple if and only if it has finitely many intermediate fields).

Counterexample

technique · direct

1.1

Write $u = s^{p}$ and $v = t^{p}$ . In the rational function field $F_{p} (v) (u)$ , the $u$ -adic valuation of a $p$ th power is divisible by $p$ , so $u$ is not a $p$ th power and $s \notin F$ . Likewise, in $F (s) = F_{p} (s) (v)$ , the $v$ -adic valuation shows that $v$ is not a $p$ th power and $t \notin F (s)$ . These valuation statements follow from reduced fractions in the UFDs of [L1] and [L2]. Every element of $E$ has its $p$ th power in $F$ , so $(s, t)$ is a minimal generating family for an exponent-one purely inseparable extension. By [L3], $[E : F] = p^{2}$ and ${s^{i} t^{j} : 0 \leq i, j < p}$ is an $F$ -basis.

L1L2L3algebra

2.1

The base field $F$ is infinite because it contains the rational function field $F_{p} (s^{p})$ from [L1]. For each $c \in F$ , put $u_{c} = s + c t$ . Then $u_{c}^{p} = s^{p} + c^{p} t^{p} \in F$ , while the basis in step 1.1 shows $u_{c} \notin F$ , so [L3] gives $[F (u_{c}) : F] = p$ .

step 1.1L1L3algebra

3.1

If $c \neq d$ and $F (u_{c}) = F (u_{d})$ , that common field contains $(u_{c} - u_{d}) / (c - d) = t$ and then $s = u_{c} - c t$ , so it equals $E$ . This contradicts its degree $p$ against $[E : F] = p^{2}$ . Hence the fields $F (u_{c})$ are pairwise distinct.

step 1.1step 2.1algebra

4.1

There are therefore infinitely many intermediate fields, and [L4] says that the finite extension $E / F$ is not simple. This refutes the stated universal claim.

step 2.1step 3.1L4∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 53 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

P. L. Clark, Field Theory, Chapter 5 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, Chapters 3 and 5 (standard reference, not scraped)

Fp(s,t)/Fp(sp,tp)Fp​(s,t)/Fp​(sp,tp) has degree p2p2, infinitely many intermediate fields, and no primitive element