LemmaStatement: Literature-sourcedProof: 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 translates of a block partition its orbit

Statement

Let $G$ act on $Ω$ , and let $B \subseteq Ω$ be a block. Then the family $T_{B} : = {g \cdot B : g \in G}$ has pairwise equal-or-disjoint members, its union is $G \cdot B : = {g \cdot b : g \in G, b \in B},$ and it is preserved by the action of $G$ . Hence $T_{B}$ is a $G$ -invariant partition of $G \cdot B$ .

Facts & Assumptions

Given: A left action of $G$ on $Ω$ and a block $B \subseteq Ω$ .

[L1]

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

Proof

technique · direct

1.1L1choose

If $g \cdot B$ meets $h \cdot B$ , choose $x \in (g \cdot B) \cap (h \cdot B)$ . Then $h^{- 1} \cdot x \in (h^{- 1} g) \cdot B \cap B$ , so [L1] gives $(h^{- 1} g) \cdot B = B$ .

1.2givenalgebra

By definition every point of $⋃ T_{B}$ has the form $g \cdot b$ with $g \in G$ and $b \in B$ , and every such point lies in the translate $g \cdot B$ . So $⋃ T_{B} = G \cdot B$ .

2.1step 1.1

From step 1.1, $g \cdot B = h \cdot B$ whenever the two translates meet. Thus distinct translates are disjoint.

3.1step 2.1step 1.2algebra∎

For $k \in G$ one has $k \cdot (g \cdot B) = (k g) \cdot B$ , which is again in $T_{B}$ . Hence $G$ permutes the members of $T_{B}$ , and steps 2.1 and 1.2 make it a $G$ -invariant partition of $G \cdot B$ .

Depends on

Blocks and block systems for a group action

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

2 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, Transitive Group Actions (standard reference, not scraped)