# Normality of rotations from every conjugate

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-finite-normal-subgroup/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-finite-normal-subgroup-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

N={e,r,r2} is normal; H={e,s} is a subgroup but is not normal.

Complete subgroup, all-g conjugation and left/right coset checks; quotient multiplication is not constructed here.





## 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).


- G — six-element group carrier
- r,s — labels with r^3=e,s^2=e,sr=r^2s
- N,H — normal and nonnormal subgroups





## 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 — The complete Cayley table must certify G, and H must first pass identity, product and inverse closure. Normality then requires gHg^(-1)=H for every g in G, equivalently gH=Hg for every g. One explicit g,h with h in H but g*h*g^(-1) outside H refutes normality. Trivial and whole subgroups are normal. Finiteness, sampled conjugates or generator checks without a proved generation obligation are insufficient. Well-defined quotient multiplication is not yet claimed here. · mko-finite-normal-subgroup





## Main derivation

S01 · impliesBefore

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

After

\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}

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

Expand the pair formula for all 36 products; every output belongs to the same six-element carrier and no cell is missing.



S02 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Both bracketings have identical coordinates, proving associativity for all 216 triples; (0,0) is a two-sided identity and the inverse formula multiplies back on both sides.



S03 · impliesBefore

N=\{e,r,r^2\}

After

\begin{array}{c|ccc}*&e&r&r^2\\\hline e&e&r&r^2\\r&r&r^2&e\\r^2&r^2&e&r\\\end{array}

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

All nine products in N remain in N, and e belongs to N.



S04 · impliesBefore

e^{-1}=e,\quad r^{-1}=r^2,\quad(r^2)^{-1}=r

After

N^{-1}=N\Rightarrow N\le G

Conditions: none

Rule: calc · Uses: G1, S02, S03

Leaf basis: calc

All three inverses lie in N, completing subgroup qualification.



S05 · impliesBefore

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

After

\begin{array}{c|ccc}gng^{-1}&e&r&r^2\\\hline e&e&r&r^2\\r&e&r&r^2\\r^2&e&r&r^2\\s&e&r^2&r\\rs&e&r^2&r\\r^2s&e&r^2&r\\\end{array}

Conditions: none

Rule: calc · Uses: G1, S01, S02, S04

Leaf basis: calc

The full 18-entry conjugation table fixes r,r^2 for rotations and swaps them for reflections; every row set equals N.



S06 · impliesBefore

N=\{e,r,r^2\},\quad B=\{s,rs,r^2s\}

After

gN=Ng=N\ (g=e,r,r^2);\qquad gN=Ng=B\ (g=s,rs,r^2s)

Conditions: none

Rule: calc · Uses: G1, S01, S04, S05

Leaf basis: calc

Left and right cosets agree for each of the six elements, providing another normality check.



S07 · impliesBefore

N\le G,\quad\forall g:\ gNg^{-1}=N

After

N\trianglelefteq G

Conditions: none

Rule: mko_definition · Uses: G1, S04, S05, S06

Leaf basis: mko_definition

Both subgroup and universal conjugation obligations are complete, so N is normal.



S08 · impliesBefore

H=\{e,s\}

After

ee=e,es=s,se=s,ss=e;\quad e^{-1}=e,s^{-1}=s\Rightarrow H\le G

Conditions: none

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

First check all four products and two inverses for H, establishing it is a subgroup too.



S09 · impliesBefore

g=r,\quad h=s\in H

After

r s r^{-1}=r^2s\notin H\Rightarrow H\not\trianglelefteq G

Conditions: none

Rule: calc · Uses: G1, S01, S02, S08

Leaf basis: calc

One explicit escaping conjugate suffices to refute universal normality.



S10 · impliesBefore

g\in G

After

g\{e\}g^{-1}=\{e\},\quad gGg^{-1}=G

Conditions: none

Rule: calc · Uses: G1, S02, S07, S09

Leaf basis: calc

The trivial and whole subgroups are normal; conjugation of G is onto because its inverse is conjugation by g inverse.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S10 · premise_audit · G1, S02, S07, S09 — These boundaries do not make every other subgroup normal.
- S09 · premise_audit · G1, S01, S02, S08 — r inverse is r^2 from the same table; product order cannot be reversed.
- S08 · premise_audit · G1, S01, S02 — The upcoming witness refutes normality, not H's subgroup status.
- S07 · premise_audit · G1, S04, S05, S06 — No quotient table or first-isomorphism theorem is claimed here.
- S06 · premise_audit · G1, S01, S04, S05 — Each coset uses all three parent-table products, not a single representative image.
- S05 · premise_audit · G1, S01, S02, S04 — All six g values are checked rather than testing r,s without a generation proof.
- S04 · premise_audit · G1, S02, S03 — Normality has not yet been proved; finiteness or an index number alone is not used to upgrade it.
- S03 · premise_audit · G1, S01 — Subgroup closure must be checked first; size 3 alone is insufficient.
- 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 tableBind every product, inverse and coset to this complete Cayley table.

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


- H has size 2 dividing 6, hence normal. → reject — r*s*r inverse=r^2s lies outside H.
- Product closure of N alone proves normality. → reject — Closure addresses subgroup status; all conjugations remain necessary, as subgroup H is not normal.
- Testing conjugation by identity suffices. → reject — Identity conjugation fixes every subset and cannot detect H's r witness.





## Result and limitations

N={e,r,r2} is normal; H={e,s} is a subgroup but is not normal.







## Verification and source binding

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


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

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-finite-normal-subgroup-01.json)