ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26

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 imprimitive wreath product preserves its fiber blocks

Example

Let $H$ act on a nonempty set $B$ , and let $H ≀_{Σ} K$ act on $B \times Σ$ in the imprimitive action of The imprimitive wreath product of permutation groups. For each $σ \in Σ$ , the fiber $F_{σ} : = B \times {σ}$ is a block. If $∣ B ∣ > 1$ and $∣ Σ ∣ > 1$ , these fibers form a nontrivial block system.

Facts & Assumptions

Given: A nonempty $H$ -set $B$ and the imprimitive wreath product action of $H ≀_{Σ} K$ on $B \times Σ$ .

[L1]

In the imprimitive wreath action, $(f, k) \cdot (b, σ) = (f (k \cdot σ) \cdot b, k \cdot σ) .$ (The imprimitive wreath product of permutation groups).

[L2]

A block is a nonempty subset $B$ such that for every group element $g$ , either $g \cdot B = B$ or $(g \cdot B) \cap B = \emptyset$ (Blocks and block systems for a group action).

Verification

technique · direct

1.1L1

For $(f, k) \in H ≀_{Σ} K$ , the image of the fiber $F_{σ}$ is exactly $F_{k \cdot σ}$ by [L1]. Hence every group element sends a fiber to a fiber.

2.1L2step 1.1given

Each fiber is nonempty because $B$ is nonempty, and two distinct fibers are disjoint, so [L2] makes each $F_{σ}$ a block. The collection of all fibers partitions $B \times Σ$ .

3.1step 2.1∎

If $∣ B ∣ > 1$ and $∣ Σ ∣ > 1$ , then each fiber is a proper non-singleton subset. So the fiber partition is a nontrivial block system.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

J. S. Milne, Group Theory, Chapter 4 (standard reference, not scraped)
K. Conrad, Semidirect Products (standard reference, not scraped)