The radical-layer bridge T ≅ NAdd T' (the U2 bridge, corestricted) #
The underlying function of the T-layer bridge: the U2 bridge value
of a radical-layer element, landed in the KERNEL-projection carrier
(banked mixed-defeq-carrier fix-class: the NAdd-headed instances fire
reducibly only at the E.N-spelling).
Equations
- Q2Presentation.Induction.tChildBridgeFun chief K t = Additive.ofMul ⟨↑((Q2Presentation.Induction.mChildEquiv chief K) (Additive.toMul ↑t)), ⋯⟩
Instances For
The T-layer bridge as an 𝔽₂-linear map.
Equations
Instances For
The radical-layer bridge T ≃ NAdd T' (linear).
Equations
Instances For
Child conjugation covers the proven C-action on T across the
bridge (childMk-generator form; mChildEquiv_conjOnMgrp corestricted
to the radical layer — the "B acts on T' through C" intertwining).
(T'^∨)^B ≃ 𝒳_T and the 2^r / 2^{dimT} cards #
A conjugation-invariant T'-dual pulls back to a 𝒳_T-element
(only childMk-conjugations are consumed).
A 𝒳_T-element pushes forward to a conjugation-invariant T'-dual:
an ARBITRARY y : B acts on T' through its C-class — the Noether-III
decomposition y = childMk y₀ · d with d ∈ M' acting trivially
(conjEndN_tChild_eq_one_of_mChild).
The invariant-dual transport (T'^∨)^B ≃ 𝒳_T (design §4-N5's
"one new transport").
Equations
- One or more equations did not get rendered due to their size.
Instances For
|X_{T'}| = |𝒳_T| = 2^r (the card_XT_eq value across the
transport; the finrank computation is replicated locally to keep the
keeps file out of this unit's import cone).
|NAdd T'| = |T| = 2^{dimT} (across the bridge).
The local T'-counts at every weak M-lift (clause (d) closed) #
The |Z¹(T')|-numeric at every weak M-lift (the local
T-stage factor of eq:mumultiplicity, lem:affinelifting): clause
(d) at the child T'-kernel, the S8.2 intrinsic bridge, and the
𝒳_T-transport give |Z¹_{F,f}(T')| = 2^{2·dimT + r} at EVERY
total-space point — weak lifts included, not only framed surjections.
The same count in the S8.2 twist-datum idiom (twistCocycle_card
closed against the numerics).
The V-layer of B/T' as an elementary kernel #
The V-layer elementary kernel at the descended child B/T'
(design §4-N5's "ElementaryKernel btChild packaging";
N = vLayer ≅ V = M/T).
Equations
- Q2Presentation.Induction.vLayerKernel chief K = { N := Q2Presentation.Induction.vLayer chief K, normal := ⋯, le_LY := ⋯, theta_dies := ⋯, comm := ⋯, exp2 := ⋯ }
Instances For
The fibre of the descended stage covers B/T' modulo the V-layer
(the fibre_covers_mod_mChild mirror at btChild: a total-space point
of the V-stage is exactly a framed weak V⋊C-lift, and its
composite-to-C surjectivity is this covering — and nothing more).
The fibre inclusion at the kernel carrier and the dual vanishing #
The linear fibre inclusion V → NAdd vLayer, re-typed at the
kernel-projection carrier (banked mixed-defeq-carrier fix-class; every
downstream statement consumes THIS spelling, and the two instance paths
meet only inside vInN_add).
Equations
- Q2Presentation.Induction.vInN chief K v = (Q2Presentation.Induction.vIn chief K) v
Instances For
Conjugation covers the head action at the kernel carrier
(vInG_conj, NAdd-level).
Invariant duals on the V-layer kernel vanish — (V^∨)^C = 0
from head-simplicity, NOT from 𝒳_T (the design's carrier guard: this
concerns V, never T): pull an invariant functional back along
vInN, transport invariance through vInG_conj/btProj_surjective,
push to M along mkQ, and kill by the proven towerDualInv_zero.
X_V = ⊥: the conjugation-invariant duals of the V-layer kernel
vanish (the mChild_conjInvDuals_eq_bot pattern one layer down).
The V-layer counts at every V⋊C-lift #
|NAdd vLayer| = |V| = 2^{dimV} (across the fibre inclusion).
The intrinsic collapse at V⋊C-lifts (audit-§G1 discipline —
PROVEN at these bases from the fibre covering, never assumed at weak
bases): the g-intrinsic invariant duals at a V-stage total-space
point are the target-level ones.
At a V⋊C-lift the intrinsic duals VANISH — mapInvDuals = ⊥
(design §4-N5's spelling of the simple-head dual-invariant vanishing).
The |Z¹(V)|-numeric at every V⋊C-lift: clause (d) at the
V-layer kernel plus the proven intrinsic collapse give
|Z¹_{F,f}(V)| = 2^{2·dimV} — the V-stage factor of
eq:mumultiplicity.
The h⁰-side: V^C = 0 (the chief dichotomy at the fixed space) #
The C-fixed subspace V^C of the head.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The multiplicative preimage of V^C inside the Frattini quotient
(the dualKerGrp device at the fixed space).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ambient preimage J ≤ Y of V^C: kernel elements whose head
class is C-fixed (the dualKerAmbient pattern one level up).
Equations
- Q2Presentation.Induction.headFixAmbient chief K = Subgroup.map K.Ksub.subtype (Subgroup.comap (QuotientGroup.mk' (frattini ↥K.Ksub)) (Q2Presentation.Induction.headFixGrp chief K))
Instances For
J is normal in Y: the conjugated class is the headActE-image
of the class, which the fixedness collapses back.
V^C = 0 (lem:simplehead's h⁰-side): a C-fixed head
vector vanishes. Chief dichotomy on J ⊔ S: in the S-branch the
fixed vector's kernel representative lies in K ∩ S, i.e. the vector
lies in T; in the P-branch ⊆-minimality gives J = K, ALL of V
is fixed, and any nonzero functional on V ≠ 0 pulls back along mkQ
to a nonzero C-invariant functional on M — killed by the proven
towerDualInv_zero.
V^C = ⊥, submodule form (the freeness input of the B¹(V)-orbit
stage).