逐步主鏈
S01 · implies
操作前
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}條件:無
規則:calc · 依賴:G1
葉節點依據:calc
將給定配對公式逐36對展開,全部輸出在同一六元素載體,沒有缺格。
S02 · implies
操作前
(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)條件:無
規則:calc · 依賴:G1, S01
葉節點依據:calc
兩種括號的座標公式相同,證全部216 triples結合律;(0,0)兩側中性,列出的逆元兩側乘回(0,0)。
S03 · implies
操作前
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}條件:無
規則:calc · 依賴:G1, S02
葉節點依據:calc
全部24個作用值由同一公式展開。對x<3,g·(h·x)=i+(−1)^j k+(−1)^{j+l}x=(gh)·x;3兩邊皆固定。e逐點固定。
S04 · implies
操作前
g^{-1}(g\cdot x)=(g^{-1}g)\cdot x=e\cdot x=x操作後
x\mapsto g\cdot x\text{ has inverse }x\mapsto g^{-1}\cdot x條件:無
規則:calc · 依賴:G1, S02, S03
葉節點依據:calc
已證作用公理與群逆元提供每列的逆函數,所以每個g確實誘導排列。
S05 · implies
操作前
s\ne e,\quad s\cdot0=0
操作後
\text{the action is not free}條件:無
規則:calc · 依賴:G1, S01, S03
葉節點依據:calc
非單位s固定point0,直接否證free所需的無非單位固定元。
S06 · implies
操作前
g\cdot0\in\{0,1,2\}\quad\forall g\in G操作後
3\notin G\cdot0\Rightarrow\text{not transitive}條件:無
規則:calc · 依賴:G1, S03
葉節點依據:calc
0-column完整只有0、1、2,無g能把0送到3,故非transitive。
S07 · implies
操作前
K=\{e,u\},\ u^2=e,\quad Y=\{0,1\}操作後
\begin{array}{c|cc}*&e&u\\\hline e&e&u\\u&u&e\end{array}\quad\begin{array}{c|cc}\cdot&0&1\\\hline e&0&1\\u&0&1\end{array}條件:無
規則:calc · 依賴:G1, S03, S04
葉節點依據:calc
另列C₂完整群表與trivial作用表:所有元素作用恒等,所以作用相容,但u≠e也誘導恒等,非faithful。
S08 · implies
操作前
e\cdot x=x,\quad(gh)\cdot x=g\cdot(h\cdot x)\text{ for all indices}操作後
G\curvearrowright X\text{ is qualified; free/faithful/transitive require separate certificates}條件:無
規則:mko_definition · 依賴:G1, S03, S04, S05, S06, S07
葉節點依據:mko_definition
同一完整模型已核單位與相容兩責任;額外性質不可自動加上。