The child elementary kernels

def Q2Presentation.Induction.mChildKernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Lifting.ElementaryKernel (XRZero.xrChild chief K).fst

The elementary M-kernel at the child B = Y/Φ(K) (lem:simplehead carrier for lem:elementarystage): N = M' = K/Φ(K).

Equations

• Q2Presentation.Induction.mChildKernel chief K = { N := Q2Presentation.Induction.mChild chief K, normal := ⋯, le_LY := ⋯, theta_dies := ⋯, comm := ⋯, exp2 := ⋯ }

def Q2Presentation.Induction.tChildKernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Lifting.ElementaryKernel (XRZero.xrChild chief K).fst

The elementary T-kernel at the child (for the |Z¹(T)|-numerics and the twist calculus): N = T' = (K∩S)Φ(K)/Φ(K).

Equations

• Q2Presentation.Induction.tChildKernel chief K = { N := Q2Presentation.Induction.tChild chief K, normal := ⋯, le_LY := ⋯, theta_dies := ⋯, comm := ⋯, exp2 := ⋯ }

Generic strict measure decrease of a quotient framed pair

theorem Q2Presentation.Induction.quotientFramedPair_measure_lt (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) (F : BoundaryFrame Yt) (hN : N ≠ ⊥) : framedMeasure ⟨TorsorProgram.quotientFramedTarget Yt N hNLY hNθ, TorsorProgram.quotientFrame Yt N hNLY hNθ F⟩ < framedMeasure ⟨Yt, F⟩

Quotienting a framed pair by a nontrivial kernel strictly decreases the induction measure |L_Y| (the xrChild_measure_lt argument, made generic: the projection L_Y ↠ L_Y/N-image collapses a nontrivial element).

The C-child framed pair

def Q2Presentation.Induction.cChild {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : FramedPair

The C-child framed pair (the carrier of X_Γ(C); manuscript C = Y/K via B/M' ≅ C, mChildCollapse).

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Induction.mChild_ne_bot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : mChild chief K ≠ ⊥

M' ≠ 1 — the head is nontrivial unconditionally (head_nontrivial, i.e. towerT_ne_top), so the child M-layer contains the class of a kernel element outside Φ(K).

theorem Q2Presentation.Induction.cChild_measure_lt {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : framedMeasure (cChild chief K) < framedMeasure (XRZero.xrChild chief K)

Strict measure decrease of the C-child (hR-free: the head is nontrivial for every K).

The numerics: dim M, dim T, d = dim V, r = dim 𝒳_T, μ

def Q2Presentation.Induction.dimM {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ℕ

dim M (the 2^{2·dimM} of lem:elementarystage).

Equations

• Q2Presentation.Induction.dimM chief K = Module.finrank (ZMod 2) (Q2Presentation.Induction.towerM K)

def Q2Presentation.Induction.dimT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ℕ

dim T.

Equations

• Q2Presentation.Induction.dimT chief K = Module.finrank (ZMod 2) ↥(Q2Presentation.Induction.towerT K)

def Q2Presentation.Induction.dimV {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ℕ

d = dim V (the head V = M/T).

Equations

• Q2Presentation.Induction.dimV chief K = Module.finrank (ZMod 2) (Q2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.towerT K)

theorem Q2Presentation.Induction.dimM_eq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : dimM chief K = dimV chief K + dimT chief K

Rank–nullity: dim M = dim V + dim T.

def Q2Presentation.Induction.XT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Submodule (ZMod 2) (Module.Dual (ZMod 2) ↥(towerT K))

𝒳_T = (T^∨)^C: the C-invariant duals of the radical layer, against the proven restricted action sec7ActOnTHom.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Induction.mem_XT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (φ : Module.Dual (ZMod 2) ↥(towerT K)) : φ ∈ XT chief K ↔ ∀ (c : towerC K), φ ∘ₗ ↑((sec7ActOnTHom chief K) c) = φ

def Q2Presentation.Induction.rT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ℕ

r = dim 𝒳_T.

Equations

• Q2Presentation.Induction.rT chief K = Module.finrank (ZMod 2) ↥(Q2Presentation.Induction.XT chief K)

def Q2Presentation.Induction.muT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ℕ

The affine-lifting multiplicity VALUE μ = |B¹(V)|·|Z¹(T)| = 2^d · 2^{2·dimT + r} (eq:mumultiplicity; the per-source realization of this count is the §4.5–4.6 lane, not U2).

Equations

• Q2Presentation.Induction.muT chief K = 2 ^ Q2Presentation.Induction.dimV chief K * 2 ^ (2 * Q2Presentation.Induction.dimT chief K + Q2Presentation.Induction.rT chief K)

The M' ≅ K/Φ(K) bridge

def Q2Presentation.Induction.mChildProj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ↥K.Ksub →* ↥(mChild chief K)

The corestricted child projection K → M'.

Equations

• Q2Presentation.Induction.mChildProj chief K = { toFun := fun (k : ↥K.Ksub) => ⟨(QuotientGroup.mk' (Q2Presentation.Induction.XRZero.NR chief K)) ↑k, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem Q2Presentation.Induction.mChildProj_eq_one_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : ↥K.Ksub) : (mChildProj chief K) k = 1 ↔ k ∈ frattini ↥K.Ksub

The kernel of the corestricted projection is exactly Φ(K).

def Q2Presentation.Induction.mChildDescend {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : towerMgrp K →* ↥(mChild chief K)

The descended hom M = K/Φ(K) → M'.

Equations

• Q2Presentation.Induction.mChildDescend chief K = QuotientGroup.lift (frattini ↥K.Ksub) (Q2Presentation.Induction.mChildProj chief K) ⋯

@[simp]

theorem Q2Presentation.Induction.mChildDescend_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : ↥K.Ksub) : (mChildDescend chief K) ((QuotientGroup.mk' (frattini ↥K.Ksub)) k) = (mChildProj chief K) k

theorem Q2Presentation.Induction.mChildDescend_bijective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Function.Bijective ⇑(mChildDescend chief K)

noncomputable def Q2Presentation.Induction.mChildEquiv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : towerMgrp K ≃* ↥(mChild chief K)

The M'-bridge: K/Φ(K) ≃* M' (lem:simplehead's identification of the child M-layer with the tower module).

Equations

• Q2Presentation.Induction.mChildEquiv chief K = MulEquiv.ofBijective (Q2Presentation.Induction.mChildDescend chief K) ⋯

@[simp]

theorem Q2Presentation.Induction.mChildEquiv_mk_coe {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : ↥K.Ksub) : ↑((mChildEquiv chief K) ((QuotientGroup.mk' (frattini ↥K.Ksub)) k)) = (QuotientGroup.mk' (XRZero.NR chief K)) ↑k

def Q2Presentation.Induction.childMk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) : (XRZero.xrChild chief K).fst.Y

The B-image of an ambient element, at the child carrier (hygiene def: keeps child multiplication homogeneous in statements — the raw mk'-application elaborates at the literal quotient carrier, which is defeq but not reducibly equal to the child carrier, so HMul synthesis fails on mixed spellings).

Equations

• Q2Presentation.Induction.childMk chief K y = (QuotientGroup.mk' (Q2Presentation.Induction.XRZero.NR chief K)) y

@[simp]

theorem Q2Presentation.Induction.childMk_eq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) : childMk chief K y = (QuotientGroup.mk' (XRZero.NR chief K)) y

theorem Q2Presentation.Induction.mChildEquiv_conj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (k : ↥K.Ksub) : ↑((mChildEquiv chief K) ((QuotientGroup.mk' (frattini ↥K.Ksub)) ((kernelConjAut K y) k))) = childMk chief K y * ↑((mChildEquiv chief K) ((QuotientGroup.mk' (frattini ↥K.Ksub)) k)) * (childMk chief K y)⁻¹

Conjugation intertwining, generator form: the bridge conjugates kernelConjAut into ambient conjugation in B.

theorem Q2Presentation.Induction.mChildEquiv_conjOnMgrp {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (m : towerMgrp K) : ↑((mChildEquiv chief K) ((conjOnMgrp K y) m)) = childMk chief K y * ↑((mChildEquiv chief K) m) * (childMk chief K y)⁻¹

Conjugation intertwining, M-form: conjOnMgrp corresponds to conjugation in B across the bridge (the towerActM-side is conjOnMgrp by towerActM_mk).

theorem Q2Presentation.Induction.mChildEquiv_mem_tChild_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (m : towerMgrp K) : ↑((mChildEquiv chief K) m) ∈ tChild chief K ↔ m ∈ towerTgrp K

T-layer transport across the bridge: the bridge identifies the multiplicative radical layer towerTgrp with the child T'-layer.