theorem Q2Presentation.Lifting.conjEndN_eq_one_of_card_two {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (hcard : Nat.card (NAdd E) = 2) (y : Yt.Y) : conjEndN E y = 1

Every conjugation operator on a card-2 elementary kernel is the identity (transcription of conjEndN_relKernel_eq_one, ScalarPushout.lean:273–296: left-inverse bijectivity + the unique nonzero element of a card-2 module).

theorem Q2Presentation.Lifting.card_Y_even_of_kernel_card_two {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (hcard : Nat.card (NAdd E) = 2) : 2 ∣ Nat.card Yt.Y

Lagrange at the order-2 kernel: the ambient target has even order (no card_Y_even-style import; idiom card_scalarCoverTarget_even, ScalarPushout.lean:316–324).

theorem Q2Presentation.Lifting.hodd_of_kernel_card_two {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (hcard : Nat.card (NAdd E) = 2) : Odd (omega2Mod (Nat.card Yt.Y)).val

The oddness input for the rows diagonal (idiom: scalarCover_hodd, ScalarPushout.lean:329–333).

theorem Q2Presentation.Lifting.rowMap_card_two_apply {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (hcard : Nat.card (NAdd E) = 2) (q : Marking Yt.Y) (n : Gen → NAdd E) : (rowMap E q) n = (n Gen.tau, n Gen.tau)

Diagonal rows at any card-2 kernel (trivial Jacobian (b, b) of prop:defduality l.1935–1939), at EVERY marking: the card-2 kernel makes every functional conjugation-invariant, so both relator rows collapse to the τ-slot (transcription of rowMap_scalarRelKernel_apply, ScalarObstruction.lean:78–120).

theorem Q2Presentation.Lifting.conjInvDuals_eq_top_of_card_two {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (hcard : Nat.card (NAdd E) = 2) : conjInvDuals E = ⊤

At a card-2 kernel EVERY functional is conjugation-invariant: 𝒳 = (N^∨)^Y = ⊤ (the conjInvDuals = ⊤ collapse feeding the local count clause |N|²·|𝒳| = 8, W2c).

theorem Q2Presentation.Lifting.cover_Z1_card_gammaA {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (hcard : Nat.card (NAdd E) = 2) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g) : Nat.card (TorsorProgram.Z1 Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g f₀) = 8

lem:commonscalars (l.3791–3815), candidate half, at ANY order-2 elementary kernel (the generic form of scalarCover_Z1_card, needed at P4's stratum covers and P7's phase covers): the framed twisted-cocycle count of Γ_A through a card-2 kernel is |Hom(Γ_A, 𝔽₂)| = 2³ = 8 — the row-map kernel at the diagonal rows is the τ-vanishing tuple space N³.