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

The marking's x₀-value is wild.

theorem Q2Presentation.Induction.sec7_xr_bockstein_witness {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : 1 < Nat.card ↥(kernelFrattini K)) (hchar : ¬∃ (lam : Module.Dual (ZMod 2) (sec7RawTowerPacketCanonical chief K).rawModuleData.R), lam ≠ 0 ∧ ∀ (c : (sec7RawTowerPacketCanonical chief K).rawModuleData.C), lam ∘ₗ ↑((sec7RawTowerPacketCanonical chief K).rawActionData.actR c) = lam) (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))) (W : Submodule (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hWst : ∀ (y : p.fst.Y), ∀ m ∈ W, ((Lifting.conjFamily (xrKernel chief K)).op y) m ∈ W) (w : Lifting.NAdd (xrKernel chief K)) (hwfix : ∀ (y : p.fst.Y), ((Lifting.conjFamily (xrKernel chief K)).op y) w - w ∈ W) (hwW : w ∉ W) : ∃ (n : Gen → Lifting.NAdd (xrKernel chief K)), Lifting.foxShadowGen (Lifting.conjFamily (xrKernel chief K)).op q n Q2Word.tameRelator - w ∈ W ∧ Lifting.foxShadowGen (Lifting.conjFamily (xrKernel chief K)).op q n Q2Word.wildRelator ∈ W

The Bockstein witness, PROVEN (prop:defduality, the full dévissage: marked fullness, the (♦)-induction, and the mixed-Hessian faithfulness at the simple sections): in the 𝒳_R = 0 branch, every relatively fixed vector outside a stable floor admits an ambient tuple whose rows are (w, 0) modulo the floor — indeed on the nose.

theorem Q2Presentation.Induction.xr_rows_surjective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : 1 < Nat.card ↥(kernelFrattini K)) (hchar : ¬∃ (lam : Module.Dual (ZMod 2) (sec7RawTowerPacketCanonical chief K).rawModuleData.R), lam ≠ 0 ∧ ∀ (c : (sec7RawTowerPacketCanonical chief K).rawModuleData.C), lam ∘ₗ ↑((sec7RawTowerPacketCanonical chief K).rawActionData.actR c) = lam) (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))) : Function.Surjective ⇑(Lifting.rowMap (xrKernel chief K) q)

XR-layer row surjectivity at frame-compatible markings, from the Bockstein step and the proven nontrivial-section machinery.

theorem Q2Presentation.Induction.sec7_xr_layer_data_proven {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : 1 < Nat.card ↥(kernelFrattini K)) (hchar : ¬∃ (lam : Module.Dual (ZMod 2) (sec7RawTowerPacketCanonical chief K).rawModuleData.R), lam ≠ 0 ∧ ∀ (c : (sec7RawTowerPacketCanonical chief K).rawModuleData.C), lam ∘ₗ ↑((sec7RawTowerPacketCanonical chief K).rawActionData.actR c) = lam) : (∀ (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), (∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).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))) → Function.Surjective ⇑(Lifting.rowMap (xrKernel chief K) q)) ∧ ∀ (f : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))), (∀ (y : p.fst.Y) (m : Lifting.NAdd (xrKernel chief K)), f ((Lifting.conjEndN (xrKernel chief K) y) m) = f m) → f = 0

The XR-layer keep statement, PROVEN from the Bockstein step and the transport.