theorem Q2Presentation.Induction.marking_x1_mem_LY {p : FramedPair} (F : BoundaryFrame p.fst) (q : Marking p.fst.Y) (hframe : ∀ (a : Gen), p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) : q Gen.x1 ∈ p.fst.LY

The marking's x₁-value is wild.

theorem Q2Presentation.Induction.headFamily_x1_eq_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (F : BoundaryFrame p.fst) (q : Marking p.fst.Y) (hframe : ∀ (a : Gen), p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) : (headFamily chief K hR).op (q Gen.x1) = 1

The head operator of the x₁-slot is trivial.

theorem Q2Presentation.Induction.card_Y_even {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : 2 ∣ Nat.card p.fst.Y

|Y| is even (the kernel is a nontrivial 2-group).

theorem Q2Presentation.Induction.head_rows_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))) (uv : HeadMod chief K hR × HeadMod chief K hR) : ∃ (nh : Gen → HeadMod chief K hR), (Lifting.foxShadowGen (headFamily chief K hR).op q nh Q2Word.tameRelator, Lifting.foxShadowGen (headFamily chief K hR).op q nh Q2Word.wildRelator) = uv

Unconditional head surjectivity — the five-lemma's head input.