theorem Q2Presentation.Lifting.Z1_card_eq_ker_rowMap {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (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₀) = Nat.card ↥(rowMap E (baseMarking E F g)).ker

The uniform cocycle count: every base lift's twisted-cocycle set has the cardinality of the row-map kernel at the base marking.