theorem Q2Presentation.Induction.conjOnR_eq_conjEndN_inv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (r : Lifting.NAdd (xrKernel chief K)) : (conjOnR chief K y) r = (Lifting.conjEndN (xrKernel chief K) y⁻¹) r

The raw conjugation matches the consumer conjugation at y⁻¹.

theorem Q2Presentation.Induction.xr_hinv_of_hchar {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (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) (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 GQ2-half transport: hchar gives invariant-dual vanishing in the consumer spelling.