The invariant-dual vanishing at the child (lem:simplehead, transported) #
The additive identification towerM K ≃+ NAdd (mChildKernel) (the U2
bridge mChildEquiv, additively — the mstageMAddEquiv idiom).
Equations
Instances For
Pull a child-kernel functional back to the tower module.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Invariant duals on the child M-kernel vanish (lem:simplehead
part 2, transported along the U2 bridge): a conjugation-invariant
functional pulls back along mChildEquiv to a towerActM-invariant
functional on M (conjugation on M' corresponds to conjOnMgrp across
the bridge, mChildEquiv_conjOnMgrp), which the proven
towerDualInv_zero kills.
The child kernel-module numerics #
The child kernel-module cardinality is 2^{dim M} (card_NAdd_mstage
at the child, through the U2 bridge).
The child M-layer is nontrivial (head_nontrivial through
mChild_ne_bot) — hR-free.
The child M-layer never has exactly two elements: operators would be
trivial and a nonzero functional invariant, contradicting mChild_hinv
(the mstage_card_ne_two argument at the child).
4 divides |B|, unconditionally: the child M-layer is a
2-group of order > 2 (nontrivial by head_nontrivial, never exactly
two by the invariant-dual vanishing), so its order — and hence |B| —
is divisible by 4 (the mstage_card_Y_four argument, hR-free).
2 divides |B| (from the 4-divisibility).
Frame facts at frame-compatible markings over the C-child #
The marking's x₀-value is wild (local clone of the generic
marking_x0_mem_LY shape at the child pair).
The marking covers B modulo the child M-kernel (the
mstage_marking_covers argument at the child: the generators
topologically generate Γ_A and the boundary surjection fills the finite
quotient).
The cover in operator form.
Relator operators are trivial at compatible markings.
The tame relation at the tame quotient of the child (the
xr_tame_relation argument at the child M-kernel: the tame relator
defect lies in M' ≤ L_B, hence dies under π).
The marked window is full at the child M-kernel (marked fullness from the cover upgrade + the transported invariant-dual vanishing).
Family-row surjectivity at the child M-kernel, from the full
(♦)-dévissage — no interim keep: the faithfulness input is discharged
generically (hfaithNT_of_frame) from the frame facts above.
Row-map surjectivity at the child M-kernel (lem:elementarystage
H² = 0 content, candidate source; design §4.6's first target
statement).
The lem:elementarystage clauses, candidate source #
Existence of framed M-lifts at the child, candidate source
(design §4.6 mChild_liftHom_nonempty_gammaA).
The framed M-lift count at the child, candidate source:
2^{2·dim M} (eq:elementarystage-numerics; uniform over g).
The twisted-cocycle count at the child, candidate source
(design §4.6 mChild_Z1_card_gammaA): |Z¹| = 2^{2·dim M}.