TheoremStatement: 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.

Orbits on ordered pairs correspond to suborbits

Statement

Let $G$ act transitively on $Ω$ , and fix $α \in Ω$ . Then the assignment $G \cdot (α, β) ⟼ G_{α} \cdot β$ is a bijection from the $G$ -orbits on $Ω \times Ω$ to the suborbits of the action at $α$ .

Facts & Assumptions

Given: A transitive action of $G$ on $Ω$ and a point $α \in Ω$ .

[L1]

A suborbit at $α$ is an orbit of the stabilizer $G_{α}$ on $Ω$ (Rank, suborbits, and subdegrees of a transitive action).

[L2]

A transitive action sends any chosen point to any other point by some element of $G$ (Left group actions, transitive actions, and faithful actions).

Proof

technique · direct

1.1L2choose

Every $G$ -orbit on $Ω \times Ω$ contains some pair $(α, β)$ : for $(x, y)$ choose $g \in G$ with $g \cdot x = α$ by [L2], and then $(g \cdot x, g \cdot y) = (α, g \cdot y)$ .

1.2L1choose

The assignment is well defined. If $(α, β_{1})$ and $(α, β_{2})$ lie in the same $G$ -orbit, choose $g \in G$ with $g \cdot (α, β_{1}) = (α, β_{2})$ . Then $g \in G_{α}$ , so $β_{2} = g \cdot β_{1}$ and the two second coordinates lie in the same suborbit.

1.3L1

The assignment is surjective because every suborbit has the form $G_{α} \cdot β$ , and it is the image of the orbital $G \cdot (α, β)$ .

1.4L1choose

The assignment is injective. If $G_{α} \cdot β_{1} = G_{α} \cdot β_{2}$ , choose $g \in G_{α}$ with $g \cdot β_{1} = β_{2}$ . Then $g \cdot (α, β_{1}) = (α, β_{2})$ , so the two pairs lie in the same $G$ -orbit.

2.1step 1.2step 1.3step 1.4∎

Steps 1.2, 1.3, and 1.4 show that orbital classes on ordered pairs correspond bijectively to suborbits at $α$ .

Depends on

Used by

A transitive action on more than one point is doubly transitive exactly when it has rank two Corollary

Dependency tree · two levels

4 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)