The head action, bundled; the faithful quotient

def Q2Presentation.Induction.headActEquiv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c : towerC K) : (towerM K ⧸ towerT K) ≃ₗ[ZMod 2] towerM K ⧸ towerT K

The head action as a linear automorphism (from the headActE laws).

Equations

• Q2Presentation.Induction.headActEquiv chief K c = LinearEquiv.ofLinear (Q2Presentation.Induction.headActE chief K c) (Q2Presentation.Induction.headActE chief K c⁻¹) ⋯ ⋯

@[simp]

theorem Q2Presentation.Induction.headActEquiv_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c : towerC K) (v : towerM K ⧸ towerT K) : (headActEquiv chief K c) v = (headActE chief K c) v

def Q2Presentation.Induction.headActHom {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : towerC K →* (towerM K ⧸ towerT K) ≃ₗ[ZMod 2] towerM K ⧸ towerT K

The head action as a homomorphism into the automorphism group.

Equations

• Q2Presentation.Induction.headActHom chief K = { toFun := Q2Presentation.Induction.headActEquiv chief K, map_one' := ⋯, map_mul' := ⋯ }

@[reducible, inline]

abbrev Q2Presentation.Induction.HeadIm {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Type

The faithful head-action image (the carrier of the averaging; the manuscript's H_V-quotient of lem:basedetclass).

Equations

• Q2Presentation.Induction.HeadIm chief K = (Q2Presentation.Induction.towerC K ⧸ (Q2Presentation.Induction.headActHom chief K).ker)

instance Q2Presentation.Induction.instFiniteHeadIm {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Finite (HeadIm chief K)

noncomputable instance Q2Presentation.Induction.instFintypeHeadIm {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Fintype (HeadIm chief K)

Equations

• Q2Presentation.Induction.instFintypeHeadIm chief K = Fintype.ofFinite (Q2Presentation.Induction.HeadIm chief K)

def Q2Presentation.Induction.actQ {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : HeadIm chief K →* (towerM K ⧸ towerT K) ≃ₗ[ZMod 2] towerM K ⧸ towerT K

The descended (faithful) action on the head.

Equations

• Q2Presentation.Induction.actQ chief K = QuotientGroup.kerLift (Q2Presentation.Induction.headActHom chief K)

@[simp]

theorem Q2Presentation.Induction.actQ_mk' {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c : towerC K) (v : towerM K ⧸ towerT K) : ((actQ chief K) ((QuotientGroup.mk' (headActHom chief K).ker) c)) v = (headActE chief K c) v

theorem Q2Presentation.Induction.actQ_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (g h : HeadIm chief K) (v : towerM K ⧸ towerT K) : ((actQ chief K) (g * h)) v = ((actQ chief K) g) (((actQ chief K) h) v)

theorem Q2Presentation.Induction.actQ_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (v : towerM K ⧸ towerT K) : ((actQ chief K) 1) v = v

theorem Q2Presentation.Induction.actQ_form_inv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (cb : HeadIm chief K) (v : towerM K ⧸ towerT K) : (edgeHeadForm chief K lam hinv hne).form (((actQ chief K) cb) v) = (edgeHeadForm chief K lam hinv hne).form v

theorem Q2Presentation.Induction.actQ_polar_inv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (cb : HeadIm chief K) (v w : towerM K ⧸ towerT K) : ((edgeHeadForm chief K lam hinv hne).polar (((actQ chief K) cb) v)) (((actQ chief K) cb) w) = ((edgeHeadForm chief K lam hinv hne).polar v) w

The correction cochain r and the per-class refinements

def Q2Presentation.Induction.rQ {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (cb : HeadIm chief K) (v w : towerM K ⧸ towerT K) : ZMod 2

The equivariance-correction bilinear cochain r_g = f∘(g×g) + f.

Equations

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

theorem Q2Presentation.Induction.rQ_cocycle {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (g h : HeadIm chief K) (v w : towerM K ⧸ towerT K) : rQ chief K lam hinv hne (g * h) v w = rQ chief K lam hinv hne g (((actQ chief K) h) v) (((actQ chief K) h) w) + rQ chief K lam hinv hne h v w

r is a (right-twisted) 1-cocycle in the action slot.

def Q2Presentation.Induction.rPkg {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (cb : HeadIm chief K) : QRefPkg chief K

The per-class QRefPkg of r_g (symmetric zero-diagonal normalized 2-cocycle — form/polar invariance under the faithful action).

Equations

• Q2Presentation.Induction.rPkg chief K lam hinv hne cb = { h := Q2Presentation.Induction.rQ chief K lam hinv hne cb, hsym := ⋯, hdiag := ⋯, hzero := ⋯, hcoc := ⋯ }

def Q2Presentation.Induction.kSel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (cb : HeadIm chief K) : towerM K ⧸ towerT K → ZMod 2

The per-class quadratic refinement (choice, frozen Core machinery).

Equations

• Q2Presentation.Induction.kSel chief K lam hinv hne cb = ⋯.choose

theorem Q2Presentation.Induction.kSel_zero {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (cb : HeadIm chief K) : kSel chief K lam hinv hne cb 0 = 0

theorem Q2Presentation.Induction.kSel_spec {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (cb : HeadIm chief K) (v w : towerM K ⧸ towerT K) : rQ chief K lam hinv hne cb v w = kSel chief K lam hinv hne cb (v + w) + kSel chief K lam hinv hne cb v + kSel chief K lam hinv hne cb w

The coherence defect and its laws

def Q2Presentation.Induction.dQ {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (g h : HeadIm chief K) (v : towerM K ⧸ towerT K) : ZMod 2

The coherence defect d(g,h) = k_g∘h + k_h + k_{gh}.

Equations

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

theorem Q2Presentation.Induction.dQ_zero {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (g h : HeadIm chief K) : dQ chief K lam hinv hne g h 0 = 0

theorem Q2Presentation.Induction.dQ_additive {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (g h : HeadIm chief K) (v w : towerM K ⧸ towerT K) : dQ chief K lam hinv hne g h (v + w) + dQ chief K lam hinv hne g h v + dQ chief K lam hinv hne g h w = 0

The defect is additive (linear-valued): its quadratic part cancels against the r-cocycle law.

theorem Q2Presentation.Induction.dQ_cocycle {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (g h k' : HeadIm chief K) (v : towerM K ⧸ towerT K) : dQ chief K lam hinv hne g h (((actQ chief K) k') v) + dQ chief K lam hinv hne (g * h) k' v = dQ chief K lam hinv hne h k' v + dQ chief K lam hinv hne g (h * k') v

The 2-cocycle law of the defect.

The first-slot average and the coboundary identity

def Q2Presentation.Induction.e2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (h : HeadIm chief K) (v : towerM K ⧸ towerT K) : ZMod 2

The first-slot average e₂(h) = Σ_g d(g,h).

Equations

• Q2Presentation.Induction.e2 chief K lam hinv hne h v = ∑ g : Q2Presentation.Induction.HeadIm chief K, Q2Presentation.Induction.dQ chief K lam hinv hne g h v

theorem Q2Presentation.Induction.e2_zero {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (h : HeadIm chief K) : e2 chief K lam hinv hne h 0 = 0

theorem Q2Presentation.Induction.e2_additive {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (h : HeadIm chief K) (v w : towerM K ⧸ towerT K) : e2 chief K lam hinv hne h (v + w) + e2 chief K lam hinv hne h v + e2 chief K lam hinv hne h w = 0

theorem Q2Presentation.Induction.dQ_eq_coboundary {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (hodd : Odd (Nat.card (HeadIm chief K))) (h k' : HeadIm chief K) (v : towerM K ⧸ towerT K) : dQ chief K lam hinv hne h k' v = e2 chief K lam hinv hne h (((actQ chief K) k') v) + e2 chief K lam hinv hne k' v + e2 chief K lam hinv hne (h * k') v

The averaging identity: over an odd faithful image the defect is exactly the twisted coboundary of e₂ (corestriction, constructive).

The coherent model on the faithful image

def Q2Presentation.Induction.mQ {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (h : HeadIm chief K) (v : towerM K ⧸ towerT K) : ZMod 2

The corrected model m = kSel + e₂.

Equations

• Q2Presentation.Induction.mQ chief K lam hinv hne h v = Q2Presentation.Induction.kSel chief K lam hinv hne h v + Q2Presentation.Induction.e2 chief K lam hinv hne h v

theorem Q2Presentation.Induction.mQ_quadratic {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (h : HeadIm chief K) (v w : towerM K ⧸ towerT K) : mQ chief K lam hinv hne h (v + w) + mQ chief K lam hinv hne h v + mQ chief K lam hinv hne h w = rQ chief K lam hinv hne h v w

theorem Q2Presentation.Induction.mQ_coherent {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (hodd : Odd (Nat.card (HeadIm chief K))) (h k' : HeadIm chief K) (v : towerM K ⧸ towerT K) : mQ chief K lam hinv hne (h * k') v = mQ chief K lam hinv hne h (((actQ chief K) k') v) + mQ chief K lam hinv hne k' v

theorem Q2Presentation.Induction.mQ_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (hodd : Odd (Nat.card (HeadIm chief K))) (v : towerM K ⧸ towerT K) : mQ chief K lam hinv hne 1 v = 0

The exits: model, splitting, bundle (odd faithful image)

theorem Q2Presentation.Induction.baseModelExists_of_oddHeadAction {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (hodd : Odd (Nat.card (HeadIm chief K))) : BaseModelExists chief K lam hinv hne

BaseModelExists holds when the faithful head-action image is odd — the manuscript's unramified clause of lem:basedetclass (l.2342–2345: the cyclic unramified image has trivial 2-primary action, so the faithful image is odd and the averaging applies). No ZeroEdge needed: the model is cover-free. On the ramified branch (even faithful image) the input remains P6-owned (lem:faithfulprojective + the orbit factor sets); the §15 baseModelExists_iff_splits pins that residual.

theorem Q2Presentation.Induction.splitsBtChild_of_zeroEdge_of_oddHeadAction {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (hZ : ZeroEdge chief K lam hinv) (hodd : Odd (Nat.card (HeadIm chief K))) : SplitsBtChild chief K

SplitsBtChild on the zero-edge branch with odd faithful head action — lem:basedetclass's unramified clause discharged through the frozen §15 chain; the R4b transgression tower is input-free here.

theorem Q2Presentation.Induction.zeroEdgeDescentData_nonempty_of_zeroEdge_of_oddHeadAction {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (hne : lam ≠ 0) (hZ : ZeroEdge chief K lam hinv) (hodd : Odd (Nat.card (HeadIm chief K))) : Nonempty (ZeroEdgeDescentData chief K lam hinv)

The U8 bundle on the branch with odd faithful head action.