theorem Q2Presentation.Induction.marking_x0_mem_LY_rad {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_radical_bockstein_witness {p : FramedPair} (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)) (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 p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) (W : Submodule (ZMod 2) (Lifting.NAdd (mstageKernel chief K hR))) (hWst : ∀ (y : p.fst.Y), ∀ m ∈ W, ((Lifting.conjFamily (mstageKernel chief K hR)).op y) m ∈ W) (w : Lifting.NAdd (mstageKernel chief K hR)) (hwfix : ∀ (y : p.fst.Y), ((Lifting.conjFamily (mstageKernel chief K hR)).op y) w - w ∈ W) (hwW : w ∉ W) : ∃ (n : Gen → Lifting.NAdd (mstageKernel chief K hR)), Lifting.foxShadowGen (Lifting.conjFamily (mstageKernel chief K hR)).op q n Q2Word.tameRelator - w ∈ W ∧ Lifting.foxShadowGen (Lifting.conjFamily (mstageKernel chief K hR)).op q n Q2Word.wildRelator ∈ W

The radical Bockstein witness, PROVEN (T-layer content of lem:simplehead part 2 / prop:defduality via the full dévissage): 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.radical_reach {p : FramedPair} (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)) (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 p.snd.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)

Radical-window reach: frame-compatible markings hit every pair of radical targets through the full row map.