theorem Q2Presentation.Induction.rowMap_M_surjective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (F : BoundaryFrame p.fst) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ F)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (mstageKernel chief K hR).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (hframe : ∀ (a : Gen), p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) (hrad : ∀ (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)) : Function.Surjective ⇑(Lifting.rowMap (mstageKernel chief K hR) q)

Row-map surjectivity at the consumer, modulo the radical hit.

theorem Q2Presentation.Induction.card_NAdd_mstage {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) : Nat.card (Lifting.NAdd (mstageKernel chief K hR)) = 2 ^ sec7MStageDim K

The kernel-module cardinality is 2^{dim M}.

theorem Q2Presentation.Induction.mstage_liftHom_nonempty {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (F : BoundaryFrame p.fst) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ F)) (hrad : ∀ (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 F.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)) : Nonempty (TorsorProgram.liftHom p.fst (mstageKernel chief K hR).N ⋯ ⋯ boundaryPackage_GammaA F g)

Existence of framed lifts, modulo the radical hit.

theorem Q2Presentation.Induction.mstage_liftHom_card {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (F : BoundaryFrame p.fst) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom p.fst (mstageKernel chief K hR).N ⋯ ⋯ boundaryPackage_GammaA F g) (hrad : ∀ (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) (Lifting.liftMarking (mstageKernel chief K hR) boundaryPackage_GammaA F g f₀)) n = (u, v)) : Nat.card (TorsorProgram.liftHom p.fst (mstageKernel chief K hR).N ⋯ ⋯ boundaryPackage_GammaA F g) = 2 ^ (2 * sec7MStageDim K)

The lift count, modulo the radical hit at the base marking.

theorem Q2Presentation.Induction.mstage_Z1_card {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (F : BoundaryFrame p.fst) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom p.fst (mstageKernel chief K hR).N ⋯ ⋯ boundaryPackage_GammaA F g) (hrad : ∀ (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) (Lifting.liftMarking (mstageKernel chief K hR) boundaryPackage_GammaA F g f₀)) n = (u, v)) : Nat.card (TorsorProgram.Z1 p.fst (mstageKernel chief K hR).N ⋯ ⋯ boundaryPackage_GammaA F g f₀) = 2 ^ (2 * sec7MStageDim K)

The engine cocycle count, modulo the radical hit at the base marking — the Z¹-clause of the mstage keep's GammaA half.