The local lem:elementarystage at the child M-kernel (THEOREM) #
The child M-kernel has no invariant duals (lem:simplehead's
(M^∨)^C = 0, in the consumer spelling): the obstruction space of the
citable local keep degenerates at mChildKernel.
Local lem:elementarystage, existence clause (THEOREM from the
citable q2_localduality_general + the proven invariant-dual vanishing):
every G_{ℚ₂}-framed surjection onto the C-child admits framed
M-lifts.
Local lem:elementarystage, count clause (THEOREM): the framed
twisted-cocycle count at the child M-kernel is 2^{2·dim M}.
The framed M-lift count at the child, local source:
2^{2·dim M} (uniform over g; the GQ2 mirror of
mChild_liftHom_card_gammaA).
The C-child count e_Γ(C') #
The C-child count (the e_Γ(C') of R4a/R4b): boundary-framed
surjections onto the C-child pair (P3-U2's cChild).
Equations
- Q2Presentation.Induction.eC chief K B = Nat.card (Q2Presentation.boundaryFramedSurj B (Q2Presentation.Induction.cChild chief K).fst (Q2Presentation.Induction.cChild chief K).snd)
Instances For
Z_{Γ,λ}(B/C) and the top-stratum keep bridge #
λ-liftability of a weak M-lift (lem:properimagesubtraction
l.4269–4271): a point of the W2a total space at the child M-kernel is
λ-liftable when some framed hom into B_λ projects to it along
p_λ = scalarCoverProj — surjectivity onto B_λ NOT imposed (weak
solvability; images are stratified by eq:recursionR2/R3).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unrestricted top count Z_{Γ,λ}(B/C): framed maps to B
whose composite to C is onto ("without imposing generation in B",
l.4270) and which weakly lift through p_λ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A surjective framed map, embedded into the W2a total space (its composite to the C-child is onto since the map itself is).
Equations
- Q2Presentation.Induction.coverSurjEmbed chief K B g = ⟨(↑g).hom, ⋯⟩
Instances For
The top-stratum keep bridge (design §4.5; R2's J = B term, for
P4): a surjective framed f is coverLiftableWeak iff its
boundaryFramedSurj packaging admits a cover lift in the KEEP's exact
scalarCoverLiftHom spelling — both sides are the same raw-hom
existential through scalarCoverLiftHom_iff_exists (P1).