theorem Q2Presentation.Induction.xr_marking_defect_mem {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (w : GExpr) (hw1 : (w.eval fun (a : Gen) => (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) = 1) : w.eval q ∈ (xrKernel chief K).N

The relator defect of a marking over the XR-child lies in Φ(K).

theorem Q2Presentation.Induction.xr_tame_relation {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) : rconj (p.fst.piY (q Gen.tau)) (p.fst.piY (q Gen.sigma)) = p.fst.piY (q Gen.tau) ^ 2

The tame relation at the tame quotient, from the XR-child.

theorem Q2Presentation.Induction.xr_rows_surjective_of_no_trivial_sections {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (hframe : ∀ (a : Gen), p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) (hnotriv : ∀ (W' W : Submodule (ZMod 2) (Lifting.NAdd (xrKernel chief K))), W' < W → ∀ (hW' : ∀ (y : p.fst.Y), ∀ m ∈ W', ((Lifting.conjFamily (xrKernel chief K)).op y) m ∈ W') (hW : ∀ (y : p.fst.Y), ∀ m ∈ W, ((Lifting.conjFamily (xrKernel chief K)).op y) m ∈ W), ¬∀ (y : p.fst.Y), (Lifting.sectionFamily (Lifting.conjFamily (xrKernel chief K)) W' W hW hW').op y = 1) : Function.Surjective ⇑(Lifting.rowMap (xrKernel chief K) q)

XR-layer row surjectivity, modulo trivial sections: if no stable section of Φ(K) is acted on trivially, the full row map at a frame-compatible marking is surjective.