theorem Q2Presentation.Induction.sec7_mstage_cochainData_proven {p : FramedPair} (h : ¬ScalarTerminal p) (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) : (∀ (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)) ∧ (∀ (g : boundaryFramedSurj boundaryPackage_GQ2 (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_GQ2 p.snd g)) ∧ ∀ (g : boundaryFramedSurj boundaryPackage_GQ2 (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_GQ2 p.snd g), Nat.card (TorsorProgram.Z1 p.fst (mstageKernel chief K hR).N ⋯ ⋯ boundaryPackage_GQ2 p.snd g f₀) = 2 ^ (2 * sec7MStageDim K)

The mstage cochain keep, PROVEN from the radical Bockstein step, the radical dual keep, and the canonical local-duality keep.