theorem Q2Presentation.Induction.xrObstructionDual_scalar_eq_zero_iff {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)) (lam : ↥(Lifting.conjInvDuals (xrKernel chief K))) (hne : ↑lam ≠ 0) : (xrObstructionDual chief K g) lam = 0 ↔ Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) ↑lam ⋯ boundaryPackage_GammaA p.snd g)

P1-A at the Frattini layer: the canonical candidate obstruction's λ-component vanishes iff g lifts through B_λ (lem:obstructionseparation l.4219–4223). No hR.