Fibers as left cosets of the stabilizer

Goal and scope

At point 0 the orbit has size 3 and stabilizer size 2; all three fibers are left cosets, giving 6=3*2.

The same complete finite action and point zero, with a two-way fiber/coset proof and translation bijections.

Givens and symbols

• calc

• G1 — G={e,r,r2,s,rs,r2s}, encoded respectively (0,0),(1,0),(2,0),(0,1),(1,1),(2,1), with (i,j)(k,l)=(i+(-1)^j*k mod3,j+l mod2). Points X={0,1,2,3}; (i,j) acts on x<3 by i+(-1)^j*x mod3 and fixes 3.

• G — six-element group carrier
• r,s — labels with r^3=e,s^2=e,sr=r^2s
• \phi_0 — action map at point zero
• H — stabilizer at the same point

Rules and sources

• calc · prerequisite — Assume exact arithmetic modulo 3 and 2, extensional finite-set equality, and definitions of groups/actions; this operation is not pre-assumed to be a group.
• mko_definition · cited — Fix the same fully certified action of G on X and point x. The action map phi_x(g)=g*x is surjective onto the orbit. If g0*x=y, its fiber over y is exactly the left coset g0*Stab_G(x); hence |G|=|G*x|*|Stab_G(x)|. The action need not be free, faithful or transitive. A proper group sample, a different point binding or a coincidentally equal numerical product is insufficient. · mko-orbit-stabilizer-theorem

Main derivation

G=\{e,r,r^2,s,rs,r^2s\}

\begin{array}{c|cccccc}*&e&r&r^2&s&rs&r^2s\\\hline e&e&r&r^2&s&rs&r^2s\\r&r&r^2&e&rs&r^2s&s\\r^2&r^2&e&r&r^2s&s&rs\\s&s&r^2s&rs&e&r^2&r\\rs&rs&s&r^2s&r&e&r^2\\r^2s&r^2s&rs&s&r^2&r&e\\\end{array}

(i,j)(k,l)=(i+(-1)^jk,j+l)\quad(\bmod(3,2))

((i,j)(k,l))(m,n)=(i+(-1)^jk+(-1)^{j+l}m,j+l+n)=(i,j)((k,l)(m,n));\quad e=(0,0);\quad(i,j)^{-1}=(-(-1)^ji,j)

X=\{0,1,2,3\}

\begin{array}{c|cccc}\cdot&0&1&2&3\\\hline e&0&1&2&3\\r&1&2&0&3\\r^2&2&0&1&3\\s&0&2&1&3\\rs&1&0&2&3\\r^2s&2&1&0&3\\\end{array}

\phi_0:G\to X,\quad\phi_0(g)=g\cdot0

\operatorname{im}\phi_0=O=\{0,1,2\},\quad H=\phi_0^{-1}(\{0\})=\{e,s\}

g=e,r,r^2,s,rs,r^2s

\phi_0^{-1}(0)=\{e,s\},\quad\phi_0^{-1}(1)=\{r,rs\},\quad\phi_0^{-1}(2)=\{r^2,r^2s\}

H=\{e,s\}

eH=\{e,s\},\quad rH=\{r,rs\},\quad r^2H=\{r^2,r^2s\}

g_0\cdot0=y

g\cdot0=y\iff(g_0^{-1}g)\cdot0=0\iff g_0^{-1}g\in H\iff g\in g_0H

L_{g_0}:H\to g_0H,\quad h\mapsto g_0h

L_{g_0}^{-1}(k)=g_0^{-1}k\Rightarrow|g_0H|=|H|=2

G=\phi_0^{-1}(0)\sqcup\phi_0^{-1}(1)\sqcup\phi_0^{-1}(2)

|G|=3\cdot2=|G\cdot0|\,|\operatorname{Stab}_G(0)|=6

Substeps and lemmas

No substeps in this guide.

Reverse audits

• S09 · premise_audit · G1, S04, S05, S08 — Neither freeness nor transitivity is needed: s fixes 0 and point 3 is outside its orbit.
• S08 · premise_audit · G1, S02, S06, S07 — Three observed pairs alone would not explain the mechanism; the inverse map supplies the bijection.
• S07 · inverse_equivalence · G1, S02, S03, S04, S06 — Conversely g=g0*h gives g*0=g0*(h*0)=g0*0, with h in the same H.
• S06 · premise_audit · G1, S01, S05 — These are left cosets g0*H; changing to H*g0 would change the order.
• S05 · premise_audit · G1, S04 — Every orbit point has a preimage, so phi0 is onto its orbit.
• S04 · premise_audit · G1, S03 — Point 3 also lies in X, but its stabilizer G cannot be substituted.
• S03 · premise_audit · G1, S02 — Every group-point pair has one value; the formula covers all 144 triples, not merely permutation rows.
• S02 · premise_audit · G1, S01 — The sign depends only on j+l modulo 2 since (-1)^2=1; the full inverse list is e,r^2,r,s,rs,r^2s.
• S01 · premise_audit · G1 — The six labels bind the six pairs; r^2 is not an additional seventh element.

Error controls and negative controls

Same group table

Bind every product, inverse and coset to this complete Cayley table.

Complete enumeration

Every universal finite property needs the full carrier or a universal formula, not a proper sample.

• Use Stab(3)=G with orbit 0 in the product. → reject — Mixing points gives 3*6=18, not 6.
• The theorem requires a free action. → reject — Nonidentity s fixes 0, yet the fiber certificate and 6=3*2 hold.
• Numerical 6=3*2 alone certifies any action. → reject — The same action/point needs full fibers and coset bijections, which arbitrary numbers do not supply.

Result and limitations

At point 0 the orbit has size 3 and stabilizer size 2; all three fibers are left cosets, giving 6=3*2.

Verification and source binding

1 declared checks for this guide; only the listed expressions are covered.

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: f78007176051f8883326c27cdfa614a2deb1ac3401d22f708d72381b178efd39
• original source SHA-256: f78007176051f8883326c27cdfa614a2deb1ac3401d22f708d72381b178efd39
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

Same-source full JSON (formulas, ASTs, controls and revision log)