A quaternion subquandle attains the good-involution bound

Abstract

The conjugation subquandle {±i, ±j} of the quaternion group Q8 has four good involutions and eight automorphisms. Its generated subgroup has center of order two and two conjugation orbits, so the bound min(8, 2^2) = 4 is attained. This answers Lực Ta’s Problem 11.7 in the negative.

Definition 1.1 (Closure under conjugation).

$$\forall (G:\mathrm{Type})[\mathrm{Group}\left(G\right)][\mathrm{DecidableEq}\left(G\right)],(\forall X:\mathrm{Finset}\left(G\right),(\mathrm{ConjClosed}\left(X\right)\iff (\forall x:G,((x\in X)\Rightarrow (\forall y:G,((y\in X)\Rightarrow (x\cdot y\cdot x^{-1}\in X)))))))$$

Formalization. D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.ConjClosed (✓ std3).

Citation. Lực Ta (2025). Good involutions of conjugation subquandles. DOI: 10.48550/arXiv.2505.08090. URL: https://arxiv.org/abs/2505.08090v5.

Commentary.

Ta, Lemma 2.10, printed page 5: “For all subsets X ⊆ G, the pair Conj X := (X, s|_X) is a subquandle of Conj G if and only if X is closed under conjugation by elements of the subgroup ⟨X⟩ of G generated by X.” Here G is a group with decidable equality and X is a finite subset. ConjClosed uses the element-wise closure condition for conjugation by elements of X. For finite X these conjugation maps are injective self-maps and hence permutations; closure then extends to H = ⟨X⟩.

Definition 1.2 (The restricted conjugation operation).

$$\forall (G:\mathrm{Type})[\mathrm{Group}\left(G\right)][\mathrm{DecidableEq}\left(G\right)],(\forall X:\mathrm{Finset}\left(G\right),(\forall h:\mathrm{ConjClosed}\left(X\right),(\forall x:X,(\forall y:X,(s\left(h,x,y\right)=⟨\mathrm{val}\left(x\right)\cdot \mathrm{val}\left(y\right)\cdot \mathrm{val}{\left(x\right)}^{-1},h\left(\mathrm{val}\left(x\right),\mathrm{property}\left(x\right),\mathrm{val}\left(y\right),\mathrm{property}\left(y\right)\right)⟩)))))$$

Formalization. D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.s (✓ std3).

Citation. Lực Ta (2025). Good involutions of conjugation subquandles. DOI: 10.48550/arXiv.2505.08090. URL: https://arxiv.org/abs/2505.08090v5.

Commentary.

Ta, Example 2.6, printed page 5: “Let G be a group, and define s : G → S_G by sending each element g ∈ G to the conjugation map defined by s_g(h) := ghg⁻¹ for all h ∈ G. Then Conj G := (G, s) is a quandle called a conjugation quandle or conjugacy quandle. Note that s_g⁻¹ = s_{g⁻¹} for all g ∈ G.” The domain X in s is the subtype of elements of the finite subset; val forgets the membership proof and property supplies it. The argument h : ConjClosed X certifies that the displayed value belongs to X.

Definition 1.3 (Good involutions).

$$\forall (G:\mathrm{Type})[\mathrm{Group}\left(G\right)][\mathrm{DecidableEq}\left(G\right)],(\forall X:\mathrm{Finset}\left(G\right),(\forall h:\mathrm{ConjClosed}\left(X\right),(\mathrm{Good}\left(X,h\right)=\{\rho :X\to X\mid ((\forall y:X,(\rho \left(\rho \left(y\right)\right)=y))\wedge (\forall x:X,((\rho \circ s\left(h,x\right)=s\left(h,x\right)\circ \rho )\wedge ((\forall y:X,(s\left(h,\rho \left(x\right)\right)\left(s\left(h,x\right)\left(y\right)\right)=y))\wedge (\forall y:X,(s\left(h,x\right)\left(s\left(h,\rho \left(x\right)\right)\left(y\right)\right)=y))))))\})))$$

Formalization. D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.Good (✓ std3).

Citation. Lực Ta (2025). Good involutions of conjugation subquandles. DOI: 10.48550/arXiv.2505.08090. URL: https://arxiv.org/abs/2505.08090v5.

Commentary.

Ta, Definition 3.8, printed page 7: “Let R = (X, s) be a rack. A good involution of R is an involution ρ ∈ S_X that satisfies the equalities ρ s_x = s_x ρ, s_{ρ(x)} = s_x⁻¹ for all x ∈ X. We denote the set of good involutions of R by Good R.” Good X h is the subtype of functions ρ : X → X satisfying these conditions. Involutive means ρ(ρ(y)) = y for every y; it implies bijectivity. The two displayed inverse identities encode Function.LeftInverse and Function.RightInverse, respectively, without requiring x⁻¹ ∈ X. The fixed parameter h certifies closure.

Definition 1.4 (Automorphisms).

$$\forall (G:\mathrm{Type})[\mathrm{Group}\left(G\right)][\mathrm{DecidableEq}\left(G\right)],(\forall X:\mathrm{Finset}\left(G\right),(\forall h:\mathrm{ConjClosed}\left(X\right),(\mathrm{Aut}\left(X,h\right)=\{\varphi :X\to X\mid ((\mathrm{Bijective}\left(\varphi \right))\wedge (\forall x:X,(\forall y:X,(\varphi \left(s\left(h,x,y\right)\right)=s\left(h,\varphi \left(x\right),\varphi \left(y\right)\right)))))\})))$$

Formalization. D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.Aut (✓ std3).

Citation. Lực Ta (2025). Good involutions of conjugation subquandles. DOI: 10.48550/arXiv.2505.08090. URL: https://arxiv.org/abs/2505.08090v5.

Commentary.

Ta, Definition 2.17, printed page 6: “Given two racks (X, s) and (Y, t), we say that a map φ : X → Y is a rack homomorphism if φs_x = t_{φ(x)}φ for all x ∈ X. A rack isomorphism is a bijective rack homomorphism, and a rack automorphism of a rack R is a rack isomorphism from R to itself.” Definition 2.20, printed page 6: “We denote the automorphism group of a rack R = (X, s) by Aut R.” Aut X h is the subtype of bijections satisfying the homomorphism identity pointwise for all x and y.

Definition 1.5 (The number of conjugation orbits).

$$\forall (G:\mathrm{Type})[\mathrm{Group}\left(G\right)][\mathrm{DecidableEq}\left(G\right)],(\forall X:\mathrm{Finset}\left(G\right),(\mathrm{orbitCount}\left(X\right)=\mathrm{FinsetCard}\left(\mathrm{image}\left((x\mapsto \mathrm{filter}\left((y\mapsto \exists g:G,((g\in \mathrm{closure}\left((X:\mathrm{Set}\left(G\right))\right))\wedge (g\cdot x\cdot g^{-1}=y))),X\right)),X\right)\right)))$$

Formalization. D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.orbitCount (✓ std3).

Citation. Lực Ta (2025). Good involutions of conjugation subquandles. DOI: 10.48550/arXiv.2505.08090. URL: https://arxiv.org/abs/2505.08090v5.

Commentary.

Ta, section 6.3.1, printed page 14: “In the following, let X/H denote the set of orbits of X under the action of H by conjugation.” Corollary 6.12 begins: “Let k(X) := |X/H|.” Here H = Subgroup.closure (X : Set G). The image sends each x ∈ X to the finite subset of y ∈ X of the form g x g⁻¹ for some g ∈ H. Its cardinality counts distinct orbit subsets, with duplicates removed by Finset.image. The existential variable g has type G; membership in H is an explicit conjunct. filter and image have the predicate/function first and the finite subset second.

Definition 1.6 (The strictness question).

$$claim\iff (\forall (G:\mathrm{Type})[\mathrm{Group}\left(G\right)][\mathrm{Fintype}\left(G\right)][\mathrm{DecidableEq}\left(G\right)],(\forall X:\mathrm{Finset}\left(G\right),(\forall h:\mathrm{ConjClosed}\left(X\right),((2\le \mathrm{NatCard}\left(\mathrm{center}\left(\mathrm{closure}\left((X:\mathrm{Set}\left(G\right))\right)\right)\right))\Rightarrow ((2\le \mathrm{orbitCount}\left(X\right))\Rightarrow (\mathrm{FintypeCard}\left(\mathrm{Good}\left(X,h\right)\right)<\min \left(\mathrm{FintypeCard}\left(\mathrm{Aut}\left(X,h\right)\right),\mathrm{NatCard}{\left(\mathrm{center}\left(\mathrm{closure}\left((X:\mathrm{Set}\left(G\right))\right)\right)\right)}^{\mathrm{orbitCount}\left(X\right)}\right)))))))$$

Formalization. D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.claim (✓ std3).

Citation. Lực Ta (2025). Good involutions of conjugation subquandles. DOI: 10.48550/arXiv.2505.08090. URL: https://arxiv.org/abs/2505.08090v5.

Commentary.

Ta, Problem 11.7, printed page 27: “In the setting of Corollary 6.12, suppose that |Z(H)|, |X/H| ≥ 2 (so, in particular, Conj X is not connected). Is the upper bound on |Good(Conj X)| in Corollary 6.12 always strict?” Corollary 6.12, printed page 14: “Let k(X) := |X/H|. Then |Good(Conj X)| ≤ min(|Aut(Conj X)|, |Z(H)|^{k(X)}). If X is not closed under inverses, then the bound |Good(Conj X)| < |Z(H)|^{k(X)} is strict.” The encoding quantifies over G : Type, each group structure, finite enumeration and decidable equality on G, every finite subset X, and every closure proof h. The binder names group, finite and eq denote these implicit Lean instances. DecidableEq is implementation structure, available classically. H = ⟨X⟩, k = orbitCount X, and z = Nat.card (Subgroup.center H); The displayed FintypeCard on Good and Aut is Fintype.card, NatCard is Nat.card, and FinsetCard is Finset.card. closure, center and Bijective denote Subgroup.closure, Subgroup.center and Function.Bijective, respectively. The displayed center cardinality and orbit count are expressions, rather than extra parameters. This is the finite-group strictness reading: a finite counterexample suffices to refute the unrestricted question. No assertion about infinite cardinal arithmetic is made.

Theorem 1.7 (The bound is attained).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.result (✓ std3). ∎

Resolves. Problems/ta-2025-problem-11-7-good-involution-bound-refutation (refuted) by D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.result.

Source. Repository-derived.

Acknowledgement. Lực Ta (2025). Good involutions of conjugation subquandles. DOI: 10.48550/arXiv.2505.08090. URL: https://arxiv.org/abs/2505.08090v5.

Commentary.

Take G = QuaternionGroup 2 and X = {a 1, a 3, xa 0, xa 2} = {±i, ±j}. The inverse of a 1 is a 3 and the inverse of xa 0 is xa 2; a 1 and xa 0 do not commute. Conjugation preserves X, and a 1 and xa 0 generate G. The center has order two. The conjugation orbits are {a 1, a 3} and {xa 0, xa 2}, so k = 2. The four good involutions independently exchange or fix the two elements in each orbit. There are eight automorphisms. Thus |Good| = 4 = min(8, 2^2), which contradicts the proposed strict inequality.

References

• Truth anchor: D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.Aut
• Truth anchor: D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.ConjClosed
• Truth anchor: D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.Good
• Truth anchor: D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.claim
• Truth anchor: D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.orbitCount
• Truth anchor: D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.result
• Truth anchor: D5/S0/Certificates/Groups/TaGoodInvolutionBoundRefutation.s