ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

The Frattini subgroup of a nontrivial cyclic $p$ -group

Example

If $P = ⟨ g ⟩$ has order $p^{n}$ with $n \geq 1$ , then $Φ (P) = ⟨ g^{p} ⟩$ and $d (P) = 1$ . For $n = 1$ , this says $Φ (P) = 1$ .

Facts & Assumptions

Given: A cyclic group $P = ⟨ g ⟩$ of order $p^{n}$ with $n \geq 1$ .

[L1]

For every finite $p$ -group $P$ , $Φ (P) = P^{'} P^{p}$ ( $Φ (P) = P^{'} P^{p}$ for a finite $p$ -group).

[L2]

If $G = ⟨ g ⟩$ has finite order $m$ , then $ord (g^{a}) = m / \gcd (a, m)$ (In a cyclic group of order $m$ , $g^{a}$ has order $m / \gcd (a, m)$ ).

[F1]

The subgroup generated by a subset is the smallest subgroup containing it, and a group is cyclic when it is generated by one element (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

[L3]

Every subgroup of a cyclic group is cyclic (Every subgroup of a cyclic group is cyclic; the least positive exponent in a nontrivial subgroup supplies a generator).

[F2]

The generator rank $d (P)$ is the common size of a basis of $P / Φ (P)$ (The generator rank $d (P)$ of a finite $p$ -group).

Verification

technique · direct

1.1givenL2F1L3algebra

Every $p$ th power in $P$ is a power of $g^{p}$ , and conversely $g^{p}$ is a $p$ th power, so [F1] gives $P^{p} = ⟨ g^{p} ⟩$ . The group is abelian, so $P^{'} = 1$ . By [L2], $⟨ g^{p} ⟩$ has order $p^{n - 1}$ , including order one at $n = 1$ , and [L3] is consistent with this cyclic subgroup description.

2.1step 1.1L1F2algebra∎

Formula [L1] gives $Φ (P) = ⟨ g^{p} ⟩$ . The quotient has order $p$ , so its nonidentity coset $g Φ (P)$ is a one-vector basis; hence [F2] gives $d (P) = 1$ .

Depends on

Used by

Dependency tree · two levels

25 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

K. Conrad, Generating Sets, Example 6.9 (standard reference, not scraped)

The Frattini subgroup of a nontrivial cyclic pp-group