theorem Q2Presentation.Induction.sec7_mstage_cochainData_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (hrad : ∀ (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ p.snd)) (q : Marking p.fst.Y), (∀ (a : Gen), (QuotientGroup.mk' (mstageKernel chief K hR).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) → (∀ (a : Gen), p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) → ∀ (u v : Lifting.NAdd (mstageKernel chief K hR)), u ∈ radicalW chief K hR → v ∈ radicalW chief K hR → ∃ (n : Gen → Lifting.NAdd (mstageKernel chief K hR)), (Lifting.rowMap (mstageKernel chief K hR) q) n = (u, v)) : (∀ (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ p.snd)), Nonempty (TorsorProgram.liftHom p.fst (mstageKernel chief K hR).N ⋯ ⋯ boundaryPackage_GammaA p.snd g)) ∧ ∀ (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ p.snd)) (f₀ : TorsorProgram.liftHom p.fst (mstageKernel chief K hR).N ⋯ ⋯ boundaryPackage_GammaA p.snd g), Nat.card (TorsorProgram.Z1 p.fst (mstageKernel chief K hR).N ⋯ ⋯ boundaryPackage_GammaA p.snd g f₀) = 2 ^ (2 * sec7MStageDim K)

The GammaA half of the mstage cochain keep, from the radical hit.