Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

Blocks containing a point correspond to intermediate subgroups

Statement

Let G act transitively on a set Ω, fix αΩ, and write Gα:={gG:gα=α}.

Then the assignments HHα:={hα:hH},BGB:={gG:gB=B} give mutually inverse bijections between

  1. subgroups H with GαHG, and
  2. blocks BΩ with αB.

Facts & Assumptions

Given: A transitive left action of G on Ω and a point αΩ.

[L1]

A block is a nonempty subset B such that for every gG one has either gB=B or (gB)B= (Blocks and block systems for a group action).

[L2]

Transitivity means that for every βΩ there is gG with gα=β (Left group actions, transitive actions, and faithful actions).

Proof

technique · direct
1.1

For the forward direction, let H satisfy GαHG and put BH:=Hα. If (gBH)BH, choose gh1α=h2α with h1,h2H. Then h21gh1GαH, so gH and therefore gBH=BH. Thus BH is a block, and clearly αBH.

L1choose
1.2

For the converse direction, let B be a block containing α, and let GB:={gG:gB=B}. If sGα, then sα=αB, so (sB)B; [L1] gives sB=B, hence GαGBG.

L1
1.3

For the converse direction, every gGB sends αB back into B, so GBαB. Conversely, if βB, choose gG with gα=β by [L2]. Then β(gB)B, so [L1] gives gB=B and therefore gGB. Hence β=gαGBα, so B=GBα.

L1L2choose
2.1

Step 1.3 shows that BGBGBα returns B. Step 1.1 gives Hα as a block containing α, and if gGHα then gαHα, so gα=hα for some hH; thus h1gGαH, and hence gH. Therefore GHα=H. The two assignments are mutually inverse.

step 1.1step 1.3

Depends on

Used by

Dependency tree · two levels

3 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