theorem Q2Presentation.Induction.card_dual_eq_of_finite' (W : Type) [AddCommGroup W] [Module (ZMod 2) W] [Finite W] : Nat.card (Module.Dual (ZMod 2) W) = Nat.card W

Finite 𝔽₂-duality preserves cardinality (local clone of the BlockR.card_dual_eq_of_finite computation, Induction/BlockRealizationAssembly.lean:117–126 — cloned rather than imported so as not to pull the packet file into this layer).

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

At a card-2 kernel the invariant-dual space has exactly two elements: 𝒳 = ⊤ (W2b) and |Dual N| = |N| = 2.

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

lem:commonscalars (l.3791–3815), local half, at ANY order-2 elementary kernel, as a THEOREM from the citable q2_localduality_general count clause (localObstruction_count): |Z¹| = |N|² · |𝒳| = 2² · 2 = 8. See the module docstring for the provenance note (Euler–Poincaré route, content-equal to the manuscript's labute_GQ2_maxPro2_marked route).

theorem Q2Presentation.Induction.liftHom_card_of_Z1_card {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : Lifting.ElementaryKernel Yt) (F : BoundaryFrame Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (h8 : ∀ (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g), Nat.card (TorsorProgram.Z1 Yt E.N ⋯ ⋯ B F g f₀) = 8) (hne : Nonempty (TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g)) : Nat.card (TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) = 8

Uniform lift count from the cocycle count (both sources; the glue supplying the W2a core's huni): if every base lift's twisted-cocycle set has size 8, so does the whole lift set of a liftable child.