Prime-Power and Finite-Quotient Separation for A5

Abstract

Prime-power quotient observations of A5 are strictly weaker than all finite quotients.

Theorem 1.1 (Prime-power observations of A5 are completely blind).

$$\begin{array}{c}(\forall p\in \mathbb{N},\mathrm{Prime}(p)\Rightarrow \mathrm{pGroupResidual}(p,A_5)=\mathrm{topSubgroup}(A_5))\wedge \\ \mathrm{primePowerResidual}(A_5)=\mathrm{topSubgroup}(A_5)\wedge \\ \mathrm{primePowerQuotientObserver}(A_5)=1\wedge \\ (\exists H\in \mathrm{FiniteQuotientIndex}(A_5),\mathrm{kernel}(H)=\mathrm{trivialSubgroup}(A_5))\wedge \\ \mathrm{finiteResidual}(A_5)=\mathrm{trivialSubgroup}(A_5)\wedge \\ \mathrm{finiteResidual}(A_5)<\mathrm{primePowerResidual}(A_5).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Factorization/PrimePowers/AlternatingFiveResidualSeparation.alternating_five_residual_separation (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every prime p, the fixed-prime residual constructed from all finite p-group quotient channels is the whole alternating group A5. The canonical residual over all primes is likewise the whole group, and its canonical joint observer is the trivial map.

The all-finite quotient family contains a channel whose kernel is the trivial subgroup, representing the identity finite quotient. Consequently its canonical residual is trivial and is strictly smaller than the prime-power residual.

References

• Truth anchor: D5/S3/Factorization/PrimePowers/AlternatingFiveResidualSeparation.alternating_five_residual_separation
• Dependency: D5/S3/Factorization/PrimePowers/FinitePrimePowerQuotientCompleteness
• Dependency: D5/S3/Factorization/PrimePowers/SimpleToPGroupTrivial