Char-2 helpers on a quotient of M (the edgeV_add_self pattern,

S-generic)

theorem Q2Presentation.Induction.delV_add_self {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (v : towerM K ⧸ S) : v + v = 0

Every vector of M/S is 2-torsion.

theorem Q2Presentation.Induction.delV_eq_of_add_eq_zero {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) {v w : towerM K ⧸ S} (h : v + w = 0) : v = w

Char-2 cancellation on M/S.

theorem Q2Presentation.Induction.delV_mk_eq_of_add_mem {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) {a b : towerM K} (h : a + b ∈ S) : Submodule.Quotient.mk a = Submodule.Quotient.mk b

mk-equality from a char-2 membership: a + b ∈ S → mk a = mk b.

The descended C-action on M/S (the headActE construction,

S-generic over the stability witness)

def Q2Presentation.Induction.delQuotMap {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (c : towerC K) : towerM K ⧸ S →ₗ[ZMod 2] towerM K ⧸ S

The C-action descended to M/S (towerActM mod the stable S, via Submodule.mapQ — the headActE template).

Equations

• Q2Presentation.Induction.delQuotMap chief K S hS c = S.mapQ S ↑((Q2Presentation.Induction.towerActM K) c) ⋯

@[simp]

theorem Q2Presentation.Induction.delQuotMap_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (c : towerC K) (m : towerM K) : (delQuotMap chief K S hS c) (Submodule.Quotient.mk m) = Submodule.Quotient.mk (((towerActM K) c) m)

theorem Q2Presentation.Induction.delQuotMap_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (v : towerM K ⧸ S) : (delQuotMap chief K S hS 1) v = v

theorem Q2Presentation.Induction.delQuotMap_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (c d : towerC K) (v : towerM K ⧸ S) : (delQuotMap chief K S hS (c * d)) v = (delQuotMap chief K S hS c) ((delQuotMap chief K S hS d) v)

theorem Q2Presentation.Induction.delQuotMap_cancel_left {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (c : towerC K) (v : towerM K ⧸ S) : (delQuotMap chief K S hS c⁻¹) ((delQuotMap chief K S hS c) v) = v

Left inverse-cancellation of the descended action.

theorem Q2Presentation.Induction.delQuotMap_cancel_right {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (c : towerC K) (v : towerM K ⧸ S) : (delQuotMap chief K S hS c) ((delQuotMap chief K S hS c⁻¹) v) = v

Right inverse-cancellation of the descended action.

def Q2Presentation.Induction.delQuotEquiv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (c : towerC K) : (towerM K ⧸ S) ≃ₗ[ZMod 2] towerM K ⧸ S

The descended action as a linear equivalence.

Equations

• Q2Presentation.Induction.delQuotEquiv chief K S hS c = LinearEquiv.ofLinear (Q2Presentation.Induction.delQuotMap chief K S hS c) (Q2Presentation.Induction.delQuotMap chief K S hS c⁻¹) ⋯ ⋯

theorem Q2Presentation.Induction.delQuotEquiv_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (c : towerC K) (v : towerM K ⧸ S) : (delQuotEquiv chief K S hS c) v = (delQuotMap chief K S hS c) v

The split tower W ⋊ C-child: the multiplicative automorphism

action, the semidirect carrier, and its cardinality

def Q2Presentation.Induction.delMulAut {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : towerC K →* MulAut (Multiplicative (towerM K ⧸ S))

The descended action, read as multiplicative automorphisms of the Multiplicative-wrapped module (the ⋊-twist datum, towerC-level).

Equations

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

theorem Q2Presentation.Induction.delMulAut_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (c : towerC K) (x : Multiplicative (towerM K ⧸ S)) : ((delMulAut chief K S hS) c) x = Multiplicative.ofAdd ((delQuotMap chief K S hS c) (Multiplicative.toAdd x))

def Q2Presentation.Induction.delPhi {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : (cChild chief K).fst.Y →* MulAut (Multiplicative (towerM K ⧸ S))

The ⋊-twist through the C-child carrier (the collapse B/M' ≃* C first, then the descended action).

Equations

• Q2Presentation.Induction.delPhi chief K S hS = (Q2Presentation.Induction.delMulAut chief K S hS).comp (Q2Presentation.Induction.cChildCollapse chief K).toMonoidHom

theorem Q2Presentation.Induction.delPhi_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (x : (cChild chief K).fst.Y) (w : Multiplicative (towerM K ⧸ S)) : ((delPhi chief K S hS) x) w = Multiplicative.ofAdd ((delQuotMap chief K S hS ((cChildCollapse chief K) x)) (Multiplicative.toAdd w))

@[reducible, inline]

abbrev Q2Presentation.Induction.delY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : Type

The split tower carrier W ⋊ C-child at W = M/S.

Equations

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

instance Q2Presentation.Induction.instFiniteDelQuot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) : Finite (towerM K ⧸ S)

instance Q2Presentation.Induction.instFiniteCChildY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Finite (cChild chief K).fst.Y

def Q2Presentation.Induction.delProdEquiv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : delY chief K S hS ≃ Multiplicative (towerM K ⧸ S) × (cChild chief K).fst.Y

The underlying product decomposition (structure eta).

Equations

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

instance Q2Presentation.Induction.instFiniteDelY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : Finite (delY chief K S hS)

theorem Q2Presentation.Induction.card_delY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : Nat.card (delY chief K S hS) = Nat.card (towerM K ⧸ S) * Nat.card (cChild chief K).fst.Y

theorem Q2Presentation.Induction.card_delQuot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) : Nat.card (towerM K ⧸ S) = 2 ^ Module.finrank (ZMod 2) (towerM K ⧸ S)

|M/S| = 2^{dim (M/S)}.

The boundary-framed structure of the split tower (H/E

preserved on the nose from the C-child — the exactImageTarget inheritance pattern, so the C-child frame transports verbatim)

def Q2Presentation.Induction.delLY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : Subgroup (delY chief K S hS)

The wild subgroup of the split tower: everything over L_C.

Equations

• Q2Presentation.Induction.delLY chief K S hS = Subgroup.comap SemidirectProduct.rightHom (Q2Presentation.Induction.cChild chief K).fst.LY

def Q2Presentation.Induction.delLYEquiv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : ↥(delLY chief K S hS) ≃ Multiplicative (towerM K ⧸ S) × ↥(cChild chief K).fst.LY

The wild subgroup decomposes as W × L_C (membership only constrains the right coordinate).

Equations

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

theorem Q2Presentation.Induction.card_delLY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : Nat.card ↥(delLY chief K S hS) = Nat.card (towerM K ⧸ S) * Nat.card ↥(cChild chief K).fst.LY

theorem Q2Presentation.Induction.delLY_isTwoGroup {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : IsPGroup 2 ↥(delLY chief K S hS)

The wild subgroup of the split tower is a 2-group (card route: 2-power kernel times the 2-group L_C).

def Q2Presentation.Induction.delTarget {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : BoundaryFramedTarget

The split-tower framed target: Y := W ⋊ C-child, tame data and decoration pulled through rightHom; H and E are the C-child's on the nose.

Equations

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

def Q2Presentation.Induction.delFrame {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : BoundaryFrame (delTarget chief K S hS)

The transported frame (H/E preserved definitionally, so the C-child frame fields typecheck verbatim — exactImageFrame pattern).

Equations

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

def Q2Presentation.Induction.delKernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : Lifting.ElementaryKernel (delTarget chief K S hS)

The kernel-part elementary kernel: N := ker rightHom (the inl-copy of W = M/S).

Equations

• Q2Presentation.Induction.delKernel chief K S hS = { N := SemidirectProduct.rightHom.ker, normal := ⋯, le_LY := ⋯, theta_dies := ⋯, comm := ⋯, exp2 := ⋯ }

theorem Q2Presentation.Induction.mem_delKernelN {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (x : delY chief K S hS) : x ∈ (delKernel chief K S hS).N ↔ x.right = 1

theorem Q2Presentation.Induction.delKernel_eq_inl {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {x : delY chief K S hS} (hx : x ∈ (delKernel chief K S hS).N) : SemidirectProduct.inl x.left = x

A kernel-part element is its own inl-readout.

The kernel-carrier bridge M/S ≃ NAdd (delKernel) (the vInN

fix-class: one raw-typed hygiene def, all downstream statements at THIS spelling)

def Q2Presentation.Induction.delInN {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (v : towerM K ⧸ S) : Lifting.NAdd (delKernel chief K S hS)

The linear fibre inclusion M/S → NAdd (ker rightHom).

Equations

• Q2Presentation.Induction.delInN chief K S hS v = Additive.ofMul ⟨SemidirectProduct.inl (Multiplicative.ofAdd v), ⋯⟩

theorem Q2Presentation.Induction.delInN_add {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (v w : towerM K ⧸ S) : delInN chief K S hS (v + w) = delInN chief K S hS v + delInN chief K S hS w

theorem Q2Presentation.Induction.delInN_bijective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : Function.Bijective (delInN chief K S hS)

theorem Q2Presentation.Induction.card_NAdd_delKernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : Nat.card (Lifting.NAdd (delKernel chief K S hS)) = Nat.card (towerM K ⧸ S)

Conjugation on the kernel part factors through the C-collapse

theorem Q2Presentation.Induction.delConj_inr {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (x : (cChild chief K).fst.Y) (v : towerM K ⧸ S) : (SemidirectProduct.inr x)⁻¹ * SemidirectProduct.inl (Multiplicative.ofAdd v) * SemidirectProduct.inr x = SemidirectProduct.inl (Multiplicative.ofAdd ((delQuotMap chief K S hS ((cChildCollapse chief K) x)⁻¹) v))

Group-level conjugation of an inl-value by an inr-value: the inverse descended action (inl_aut_inv + the delPhi-readout).

theorem Q2Presentation.Induction.conjEndN_delKernel_inr {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (x : (cChild chief K).fst.Y) (v : towerM K ⧸ S) : (Lifting.conjEndN (delKernel chief K S hS) (SemidirectProduct.inr x)) (delInN chief K S hS v) = delInN chief K S hS ((delQuotMap chief K S hS ((cChildCollapse chief K) x)⁻¹) v)

Kernel-module conjugation by an inr-point is the inverse descended action across the carrier bridge.

theorem Q2Presentation.Induction.conjEndN_delKernel_right {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (y : delY chief K S hS) : Lifting.conjEndN (delKernel chief K S hS) y = Lifting.conjEndN (delKernel chief K S hS) (SemidirectProduct.inr y.right)

Kernel-module conjugation only sees the right coordinate (the inl-part is abelian, hence acts trivially on its own module).

The invariant-dual vanishing core (the vLayer_hinv route:

pull to M/S, then to M along mkQ, kill by towerDualInv_zero)

theorem Q2Presentation.Induction.delDualInv_core {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (f : Module.Dual (ZMod 2) (Lifting.NAdd (delKernel chief K S hS))) (hf : ∀ (c : towerC K) (v : towerM K ⧸ S), f (delInN chief K S hS ((delQuotMap chief K S hS c) v)) = f (delInN chief K S hS v)) : f = 0

The vanishing core: a functional on the kernel module invariant under the full descended C-action is zero.

theorem Q2Presentation.Induction.conjInvDuals_delKernel_eq_bot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) : Lifting.conjInvDuals (delKernel chief K S hS) = ⊥

Target-level invariant duals vanish at the kernel-part (candidate-engine input): full conjugation invariance restricts to the inr-copy of C, which covers towerC through the collapse.

The canonical base over ρ: inr ∘ ρ (exists for EVERY lower

map — the split tower's raison d'être)

def Q2Presentation.Induction.delBase {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Γ ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (delTarget chief K S hS).Y)

The split-tower base: γ ↦ inr (ρ γ) (a continuous hom for every ρ — no obstruction, unlike the arithmetic Y'/T'_χ-tower).

Equations

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

theorem Q2Presentation.Induction.delBase_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (γ : ↑Γ.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (delBase chief K S hS B ρ)) γ = SemidirectProduct.inr ((ProfiniteGrp.Hom.hom (↑ρ).hom) γ)

def Q2Presentation.Induction.delBaseVal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (γ : ↑Γ.toProfinite.toTop) : delY chief K S hS

Raw-typed readout of the base (the btLiftVal hygiene fix-class: every PRODUCT statement below is spelled at THIS raw carrier — the wrapped arrow-readout delBase … γ only ever appears applied, never as a HMul-operand).

Equations

• Q2Presentation.Induction.delBaseVal chief K S hS B ρ γ = SemidirectProduct.inr ((ProfiniteGrp.Hom.hom (↑ρ).hom) γ)

theorem Q2Presentation.Induction.delBaseVal_def {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (γ : ↑Γ.toProfinite.toTop) : delBaseVal chief K S hS B ρ γ = SemidirectProduct.inr ((ProfiniteGrp.Hom.hom (↑ρ).hom) γ)

theorem Q2Presentation.Induction.delBase_qYMap {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (γ : ↑Γ.toProfinite.toTop) : (delTarget chief K S hS).qYMap ((ProfiniteGrp.Hom.hom (delBase chief K S hS B ρ)) γ) = (ProfiniteGrp.Hom.hom (delFrame chief K S hS).beta) ((ProfiniteGrp.Hom.hom B.toBoundary) γ)

The base is framed: q_Y ∘ (inr ∘ ρ) = β ∘ b_Γ (the split tower's q_Y reads through rightHom, so this is ρ's own frame clause).

theorem Q2Presentation.Induction.mapInvDuals_delKernel_eq_bot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : mapInvDuals (delKernel chief K S hS) (delBase chief K S hS B ρ) = ⊥

The intrinsic collapse at the split-tower base (audit-§G1 discipline, proven — never assumed): the g-intrinsic invariant duals vanish, because the base's conjugation realizes the FULL towerC-action (ρ̄ is onto C).

The additive twisted-cocycle carrier Z¹_ρ(M/S) (the edgeZ1

template at the descended action — N1's orientation pin verbatim)

def Q2Presentation.Induction.delZ1Add {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : AddSubgroup (↑Γ.toProfinite.toTop → towerM K ⧸ S)

The additive-subgroup carrier of Z¹_ρ(M/S).

Equations

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

def Q2Presentation.Induction.delZ1 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Submodule (ZMod 2) (↑Γ.toProfinite.toTop → towerM K ⧸ S)

Z¹_ρ(M/S) — locally constant ρ̄-twisted 1-cocycles valued in the intermediate module (the mid-carrier of the dévissage).

Equations

• Q2Presentation.Induction.delZ1 chief K S hS B ρ = (AddSubgroup.toZModSubmodule 2) (Q2Presentation.Induction.delZ1Add chief K S hS B ρ)

theorem Q2Presentation.Induction.mem_delZ1 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↑Γ.toProfinite.toTop → towerM K ⧸ S) : z ∈ delZ1 chief K S hS B ρ ↔ IsLocallyConstant z ∧ ∀ (γ γ' : ↑Γ.toProfinite.toTop), z (γ * γ') = z γ + (delQuotMap chief K S hS (lowerBar chief K B ρ γ)) (z γ')

theorem Q2Presentation.Induction.delZ1_val_lc {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(delZ1 chief K S hS B ρ)) : IsLocallyConstant ↑z

theorem Q2Presentation.Induction.delZ1_val_law {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(delZ1 chief K S hS B ρ)) (γ γ' : ↑Γ.toProfinite.toTop) : ↑z (γ * γ') = ↑z γ + (delQuotMap chief K S hS (lowerBar chief K B ρ γ)) (↑z γ')

theorem Q2Presentation.Induction.delBase_conj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (γ' : ↑Γ.toProfinite.toTop) (v : towerM K ⧸ S) : (delBaseVal chief K S hS B ρ γ')⁻¹ * SemidirectProduct.inl (Multiplicative.ofAdd v) * delBaseVal chief K S hS B ρ γ' = SemidirectProduct.inl (Multiplicative.ofAdd ((delQuotMap chief K S hS (lowerBar chief K B ρ γ')⁻¹) v))

The base's conjugation on inl-values, read at the lowerBar spelling (one-spelling bridge over delConj_inr; RAW carrier throughout).

theorem Q2Presentation.Induction.delZ1_inv_twist_law {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(delZ1 chief K S hS B ρ)) (γ γ' : ↑Γ.toProfinite.toTop) : (delQuotMap chief K S hS (lowerBar chief K B ρ (γ * γ'))⁻¹) (↑z (γ * γ')) = (delQuotMap chief K S hS (lowerBar chief K B ρ γ')⁻¹) ((delQuotMap chief K S hS (lowerBar chief K B ρ γ)⁻¹) (↑z γ)) + (delQuotMap chief K S hS (lowerBar chief K B ρ γ')⁻¹) (↑z γ')

The inverse-twisted reading of the cocycle law (the dictionary's target law).

The dictionary Z¹_ρ(M/S) ≃ weakZ1 (delKernel) (inr ∘ ρ) (the

inverse-act twist w γ = ρ̄(γ)⁻¹ · z γ, inl-wrapped)

def Q2Presentation.Induction.delDictFun {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(delZ1 chief K S hS B ρ)) (γ : ↑Γ.toProfinite.toTop) : ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (delTarget chief K S hS).Y)).toProfinite.toTop

The forward dictionary value (WRAPPED codomain — the carrier that carries the topology and the weakZ1-slot instances; the body is the raw inl-term, def-value defeq).

Equations

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

theorem Q2Presentation.Induction.delDictFun_mem {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↥(delZ1 chief K S hS B ρ)) : (∀ (γ : ↑Γ.toProfinite.toTop), delDictFun chief K S hS B ρ z γ ∈ (delKernel chief K S hS).N) ∧ Continuous (delDictFun chief K S hS B ρ z) ∧ ∀ (γ γ' : ↑Γ.toProfinite.toTop), delDictFun chief K S hS B ρ z (γ * γ') = ((ProfiniteGrp.Hom.hom (delBase chief K S hS B ρ)) γ')⁻¹ * delDictFun chief K S hS B ρ z γ * (ProfiniteGrp.Hom.hom (delBase chief K S hS B ρ)) γ' * delDictFun chief K S hS B ρ z γ'

The forward dictionary lands in weakZ1 (all three clauses stated at the slot's own spellings — wrapped carrier, delBase-applications).

def Q2Presentation.Induction.weakVal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (E : Lifting.ElementaryKernel (delTarget chief K S hS)) (W : weakZ1 E (delBase chief K S hS B ρ)) (γ : ↑Γ.toProfinite.toTop) : delY chief K S hS

Raw-typed readout of a weak twisted cocycle at ANY elementary kernel of the split tower (the btLiftVal hygiene fix-class: every product/projection statement below is spelled at THIS raw carrier — the wrapped W.val γ never appears as a HMul-operand or under a field projection).

Equations

• Q2Presentation.Induction.weakVal chief K S hS B ρ E W γ = ↑W γ

def Q2Presentation.Induction.delDictInvFun {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (W : weakZ1 (delKernel chief K S hS) (delBase chief K S hS B ρ)) (γ : ↑Γ.toProfinite.toTop) : towerM K ⧸ S

The inverse dictionary value (z γ = ρ̄(γ) · toAdd (W γ).left).

Equations

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

theorem Q2Presentation.Induction.delDictInvFun_mem {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (W : weakZ1 (delKernel chief K S hS) (delBase chief K S hS B ρ)) : delDictInvFun chief K S hS B ρ W ∈ delZ1 chief K S hS B ρ

The inverse dictionary lands in Z¹_ρ(M/S).

def Q2Presentation.Induction.delDict {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : ↥(delZ1 chief K S hS B ρ) ≃ weakZ1 (delKernel chief K S hS) (delBase chief K S hS B ρ)

The dictionary: the additive mid-carrier and the split-tower twisted-cocycle set have the same cardinality data.

Equations

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

theorem Q2Presentation.Induction.card_delZ1_eq_weakZ1 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Nat.card ↥(delZ1 chief K S hS B ρ) = Nat.card (weakZ1 (delKernel chief K S hS) (delBase chief K S hS B ρ))

The LOCAL engine fire: clause (d) at the split-tower kernel

(q2_localduality_weakZ1_card, the citable keep — no side conditions)

theorem Q2Presentation.Induction.delZ1_card_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (B : BoundaryPackage GQ2Profinite) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Nat.card ↥(delZ1 chief K S hS B ρ) = Nat.card (towerM K ⧸ S) ^ 2

|Z¹_ρ(M/S)| = |M/S|² at G_ℚ₂ — clause (d) + the proven mapInvDuals-collapse.

The CANDIDATE engine fire: N6's ledger + corank engine at the

split tower (kernel-generic — reused at the χ-bit kernel)

theorem Q2Presentation.Induction.delBase_covers_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (ρ : boundaryFramedSurj boundaryPackage_GammaA (cChild chief K).fst (cChild chief K).snd) : Function.Surjective fun (γ : ↑GammaA.toProfinite.toTop) => (QuotientGroup.mk' (delKernel chief K S hS).N) ((ProfiniteGrp.Hom.hom (delBase chief K S hS boundaryPackage_GammaA ρ)) γ)

The split-tower base covers the target modulo the kernel part (ρ-surjectivity through rightHom).

theorem Q2Presentation.Induction.delWeakZ1_card_gammaA_of {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (ρ : boundaryFramedSurj boundaryPackage_GammaA (cChild chief K).fst (cChild chief K).snd) (h4 : 4 ∣ Nat.card (towerM K ⧸ S)) (E : Lifting.ElementaryKernel (delTarget chief K S hS)) (hcover : ∀ (y : (delTarget chief K S hS).Y), ∃ c ∈ Subgroup.closure (Set.range (weakMarking (delBase chief K S hS boundaryPackage_GammaA ρ))), (Lifting.conjFamily E).op (y * c⁻¹) = 1) : Nat.card (weakZ1 E (delBase chief K S hS boundaryPackage_GammaA ρ)) = Nat.card (Lifting.NAdd E) ^ 2 * Nat.card ↥(Lifting.conjInvDuals E)

The generic candidate count at the split tower: N6's ledger dictionary + corank engine, for ANY elementary kernel over delTarget with a marking-covering (|Z¹| = |N|²·|𝒳|, the prop:defduality instance shape).

theorem Q2Presentation.Induction.delZ1_card_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (S : Submodule (ZMod 2) (towerM K)) (hS : ∀ (c : towerC K), ∀ m ∈ S, ((towerActM K) c) m ∈ S) (ρ : boundaryFramedSurj boundaryPackage_GammaA (cChild chief K).fst (cChild chief K).snd) (h4 : 4 ∣ Nat.card (towerM K ⧸ S)) : Nat.card ↥(delZ1 chief K S hS boundaryPackage_GammaA ρ) = Nat.card (towerM K ⧸ S) ^ 2

|Z¹_ρ(M/S)| = |M/S|² at Γ_A — the corank engine at the kernel part (𝒳 = ⊥ by the vanishing core).

The ker χ̃-kernel data: T_χ = ker (χ|_T) and the 𝔽₂-line

T/T_χ (T ∩ ker χ̃ = ker (χ|_T) since χ̃|_T = χ — the design's "clause-(d) instances at ker χ̃-kernels")

def Q2Presentation.Induction.chiKerT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) : Submodule (ZMod 2) (towerM K)

T_χ ≤ M: the kernel of χ on the radical layer, ambient spelling.

Equations

• Q2Presentation.Induction.chiKerT chief K chi = Submodule.map (Q2Presentation.Induction.towerT K).subtype (LinearMap.ker ↑chi)

theorem Q2Presentation.Induction.chiKerT_le {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) : chiKerT chief K chi ≤ towerT K

theorem Q2Presentation.Induction.mem_chiKerT_of {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {m : towerM K} (hm : m ∈ towerT K) (h0 : ↑chi ⟨m, hm⟩ = 0) : m ∈ chiKerT chief K chi

theorem Q2Presentation.Induction.chiVal_eq_zero_of_mem_chiKerT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {m : towerM K} (hmem : m ∈ chiKerT chief K chi) (hm : m ∈ towerT K) : ↑chi ⟨m, hm⟩ = 0

theorem Q2Presentation.Induction.chiTilde_of_mem_towerT {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {m : towerM K} (hm : m ∈ towerT K) : (chiTilde chief K chi) m = ↑chi ⟨m, hm⟩

χ̃ restricted to T is χ (the retraction is the identity on T).

theorem Q2Presentation.Induction.chiKerT_stable {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (c : towerC K) (m : towerM K) : m ∈ chiKerT chief K chi → ((towerActM K) c) m ∈ chiKerT chief K chi

T_χ is C-stable (χ-invariance: mem_XT through the restricted action's coe law).

def Q2Presentation.Induction.chiLine {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) : Submodule (ZMod 2) (towerM K ⧸ chiKerT chief K chi)

The 𝔽₂-line T/T_χ inside the intermediate module M/T_χ.

Equations

• Q2Presentation.Induction.chiLine chief K chi = Submodule.map (Q2Presentation.Induction.chiKerT chief K chi).mkQ (Q2Presentation.Induction.towerT K)

theorem Q2Presentation.Induction.mk_mem_chiLine_of {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {m : towerM K} (hm : m ∈ towerT K) : Submodule.Quotient.mk m ∈ chiLine chief K chi

theorem Q2Presentation.Induction.delQuotMap_of_mem_chiLine {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (c : towerC K) {v : towerM K ⧸ chiKerT chief K chi} (hv : v ∈ chiLine chief K chi) : (delQuotMap chief K (chiKerT chief K chi) ⋯ c) v = v

The descended action is TRIVIAL on the line (χ-invariance measures the defect).

theorem Q2Presentation.Induction.card_chiLine {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) : Nat.card ↥(chiLine chief K chi) = 2

The line has exactly two elements (χ ≠ 0 gives a χ-unit t₀; everything in the line is 0 or mk t₀).

The χ-bit kernel: the 𝔽₂-line as a CENTRAL elementary kernel of

the χ-split tower (its |Z¹| = 2²·2 = 8 is the |Hom(Γ, ℤ/2)|-count of the dévissage fibre)

def Q2Presentation.Induction.chiBitN {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) : Subgroup (delY chief K (chiKerT chief K chi) ⋯)

The line's subgroup inside the χ-split tower.

Equations

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

theorem Q2Presentation.Induction.chiBit_conj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (g : delY chief K (chiKerT chief K chi) ⋯) {x : delY chief K (chiKerT chief K chi) ⋯} (hx : x ∈ chiBitN chief K chi) : g * x * g⁻¹ = x

Centrality of the bit: conjugation fixes the line pointwise (the inl-part is abelian; the inr-part acts trivially on the line).

def Q2Presentation.Induction.chiBitKernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) : Lifting.ElementaryKernel (delTarget chief K (chiKerT chief K chi) ⋯)

The χ-bit elementary kernel.

Equations

• Q2Presentation.Induction.chiBitKernel chief K chi = { N := Q2Presentation.Induction.chiBitN chief K chi, normal := ⋯, le_LY := ⋯, theta_dies := ⋯, comm := ⋯, exp2 := ⋯ }

theorem Q2Presentation.Induction.conjEndN_chiBit {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (y : (delTarget chief K (chiKerT chief K chi) ⋯).Y) : Lifting.conjEndN (chiBitKernel chief K chi) y = 1

Conjugation operators are TRIVIAL at the bit (centrality).

theorem Q2Presentation.Induction.card_NAdd_chiBit {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) : Nat.card (Lifting.NAdd (chiBitKernel chief K chi)) = 2

The bit carrier has exactly two elements.

theorem Q2Presentation.Induction.conjInvDuals_chiBit_eq_top {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) : Lifting.conjInvDuals (chiBitKernel chief K chi) = ⊤

Every dual of the bit is conjugation-invariant (centrality).

theorem Q2Presentation.Induction.mapInvDuals_chiBit_eq_top {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : mapInvDuals (chiBitKernel chief K chi) (delBase chief K (chiKerT chief K chi) ⋯ B ρ) = ⊤

Every dual of the bit is intrinsically invariant at any base.

theorem Q2Presentation.Induction.card_dual_chiBit {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) : Nat.card (Module.Dual (ZMod 2) (Lifting.NAdd (chiBitKernel chief K chi))) = 2

|(bit)^∨| = 2 (finite 𝔽₂-duality preserves cardinality).

theorem Q2Presentation.Induction.card_top_dual_chiBit {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) : Nat.card ↥⊤ = 2

The card of the ⊤-submodule of bit duals is 2.

theorem Q2Presentation.Induction.chiBit_weakZ1_card_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) (B : BoundaryPackage GQ2Profinite) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Nat.card (weakZ1 (chiBitKernel chief K chi) (delBase chief K (chiKerT chief K chi) ⋯ B ρ)) = 8

The local bit count: |Z¹_{G_ℚ₂}(𝔽₂-line)| = 2²·2 = 8 (clause (d); this is |Hom_cont(G_ℚ₂, ℤ/2)| in engine form).

theorem Q2Presentation.Induction.chiBit_weakZ1_card_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) (h4 : 4 ∣ Nat.card (towerM K ⧸ chiKerT chief K chi)) (ρ : boundaryFramedSurj boundaryPackage_GammaA (cChild chief K).fst (cChild chief K).snd) : Nat.card (weakZ1 (chiBitKernel chief K chi) (delBase chief K (chiKerT chief K chi) ⋯ boundaryPackage_GammaA ρ)) = 8

The candidate bit count: |Z¹_{Γ_A}(𝔽₂-line)| = 2²·2 = 8 (the ledger corank engine; the covering is trivial by centrality).

The towerT-instance: the generic carrier at S = T IS edgeZ1

(the two laws differ only in the mapQ-packaging of the same action)

theorem Q2Presentation.Induction.towerT_stable' {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (c : towerC K) (m : towerM K) : m ∈ towerT K → ((towerActM K) c) m ∈ towerT K

Stability of T in the generic hypothesis shape.

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

theorem Q2Presentation.Induction.delZ1_towerT_eq_edgeZ1 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : delZ1 chief K (towerT K) ⋯ B ρ = edgeZ1 chief K B ρ

Carrier identification: Z¹_ρ(M/T)-generic = edgeZ1 (N7's engine carrier), as submodules.

theorem Q2Presentation.Induction.card_edgeZ1_eq_delZ1 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Nat.card ↥(edgeZ1 chief K B ρ) = Nat.card ↥(delZ1 chief K (towerT K) ⋯ B ρ)

The V-numerics: |V| ∉ {1, 2}, hence 4 ∣ |V|

theorem Q2Presentation.Induction.card_edgeV_pos {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : 0 < Nat.card (towerM K ⧸ towerT K)

theorem Q2Presentation.Induction.card_edgeV_ne_two {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Nat.card (towerM K ⧸ towerT K) ≠ 2

|V| ≠ 2: on a two-element module every linear automorphism is the identity, so a nonzero head vector would be C-fixed — killed by N5's headInv_eq_zero.

theorem Q2Presentation.Induction.four_dvd_card_edgeV {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : 4 ∣ Nat.card (towerM K ⧸ towerT K)

4 ∣ |V| (the head is a 2-power of order > 2).

The χ-quotient cardinality: |M/T_χ| = 2·|V| (division-free)

theorem Q2Presentation.Induction.card_chiKerT_pos {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) : 0 < Nat.card ↥(chiKerT chief K chi)

theorem Q2Presentation.Induction.card_towerT_sub_quot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) : Nat.card (↥(towerT K) ⧸ LinearMap.ker ↑chi) = 2

|T/ker χ| = 2 (χ ≠ 0 through the χ-unit t₀).

theorem Q2Presentation.Induction.card_towerT_eq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) : Nat.card ↥(towerT K) = Nat.card ↥(chiKerT chief K chi) * 2

|T| = |T_χ|·2.

theorem Q2Presentation.Induction.card_chiQuot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) : Nat.card (towerM K ⧸ chiKerT chief K chi) = 2 * Nat.card (towerM K ⧸ towerT K)

|M/T_χ| = 2·|V| (tower cardinality bookkeeping, division-free via left-cancellation at |T_χ| > 0).

theorem Q2Presentation.Induction.four_dvd_card_chiQuot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) : 4 ∣ Nat.card (towerM K ⧸ chiKerT chief K chi)

4 ∣ |M/T_χ| (the candidate engine's target-size input).

The mid-to-edge projection π_* : Z¹_ρ(M/T_χ) →ₗ Z¹_ρ(V)

def Q2Presentation.Induction.chiMkV {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) : towerM K ⧸ chiKerT chief K chi →ₗ[ZMod 2] towerM K ⧸ towerT K

The module collapse M/T_χ → V.

Equations

• Q2Presentation.Induction.chiMkV chief K chi = (Q2Presentation.Induction.chiKerT chief K chi).mapQ (Q2Presentation.Induction.towerT K) LinearMap.id ⋯

@[simp]

theorem Q2Presentation.Induction.chiMkV_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (m : towerM K) : (chiMkV chief K chi) (Submodule.Quotient.mk m) = Submodule.Quotient.mk m

theorem Q2Presentation.Induction.chiMkV_eq_zero_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (v : towerM K ⧸ chiKerT chief K chi) : (chiMkV chief K chi) v = 0 ↔ v ∈ chiLine chief K chi

theorem Q2Presentation.Induction.chiMkV_delQuotMap {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (c : towerC K) (v : towerM K ⧸ chiKerT chief K chi) : (chiMkV chief K chi) ((delQuotMap chief K (chiKerT chief K chi) ⋯ c) v) = (headActE chief K c) ((chiMkV chief K chi) v)

The collapse intertwines the descended actions.

def Q2Presentation.Induction.chiMidProjFun {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (w : ↥(delZ1 chief K (chiKerT chief K chi) ⋯ B ρ)) : ↥(edgeZ1 chief K B ρ)

The underlying projection value.

Equations

• Q2Presentation.Induction.chiMidProjFun chief K chi B ρ w = ⟨fun (γ : ↑Γ.toProfinite.toTop) => (Q2Presentation.Induction.chiMkV chief K chi) (↑w γ), ⋯⟩

theorem Q2Presentation.Induction.chiMidProjFun_val {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (w : ↥(delZ1 chief K (chiKerT chief K chi) ⋯ B ρ)) (γ : ↑Γ.toProfinite.toTop) : ↑(chiMidProjFun chief K chi B ρ w) γ = (chiMkV chief K chi) (↑w γ)

def Q2Presentation.Induction.chiMidProjHom {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : ↥(delZ1 chief K (chiKerT chief K chi) ⋯ B ρ) →ₗ[ZMod 2] ↥(edgeZ1 chief K B ρ)

π_*, linearly packaged.

Equations

• Q2Presentation.Induction.chiMidProjHom chief K chi B ρ = AddMonoidHom.toZModLinearMap 2 (AddMonoidHom.mk' (Q2Presentation.Induction.chiMidProjFun chief K chi B ρ) ⋯)

theorem Q2Presentation.Induction.chiMidProjHom_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (w : ↥(delZ1 chief K (chiKerT chief K chi) ⋯ B ρ)) : (chiMidProjHom chief K chi B ρ) w = chiMidProjFun chief K chi B ρ w

Claim A: a solvable χ̃-pushout defect lifts the cocycle to the

intermediate carrier (the hard direction of the dévissage; the solving cochain corrects the section lift along the χ-unit)

theorem Q2Presentation.Induction.exists_mid_lift {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) (z : ↥(edgeZ1 chief K B ρ)) (hz : edgeLRead chief K B ρ z chi = 0) : ∃ (w : ↥(delZ1 chief K (chiKerT chief K chi) ⋯ B ρ)), (chiMidProjHom chief K chi B ρ) w = z

Claim A: edgeLRead z χ = 0 produces a π_*-preimage of z in Z¹_ρ(M/T_χ).

theorem Q2Presentation.Induction.chiMidProjHom_range_eq_top {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) (H : ∀ (z : ↥(edgeZ1 chief K B ρ)), edgeLRead chief K B ρ z chi = 0) : (chiMidProjHom chief K chi B ρ).range = ⊤

Under the contradiction hypothesis L(·)(χ) ≡ 0, π_* is onto.

The fibre identification: ker π_* ≃ weakZ1 (χ-bit) (the

|Hom_cont(Γ, ℤ/2)|-fibre of the dévissage, engine-countable)

theorem Q2Presentation.Induction.mem_ker_chiMidProjHom {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (w : ↥(delZ1 chief K (chiKerT chief K chi) ⋯ B ρ)) : w ∈ (chiMidProjHom chief K chi B ρ).ker ↔ ∀ (γ : ↑Γ.toProfinite.toTop), ↑w γ ∈ chiLine chief K chi

def Q2Presentation.Induction.chiKerEquivBit {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : ↥(chiMidProjHom chief K chi B ρ).ker ≃ weakZ1 (chiBitKernel chief K chi) (delBase chief K (chiKerT chief K chi) ⋯ B ρ)

The fibre equivalence (inl-wrapping; the twist is trivial on the line, so no act-correction appears).

Equations

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

theorem Q2Presentation.Induction.card_ker_chiMidProjHom {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Nat.card ↥(chiMidProjHom chief K chi B ρ).ker = Nat.card (weakZ1 (chiBitKernel chief K chi) (delBase chief K (chiKerT chief K chi) ⋯ B ρ))

The contradiction core and the per-source exits

theorem Q2Presentation.Induction.delSurj_core {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : ↑chi ⟨t₀, ht₀T⟩ = 1) (hMid : Nat.card ↥(delZ1 chief K (chiKerT chief K chi) ⋯ B ρ) = Nat.card (towerM K ⧸ chiKerT chief K chi) ^ 2) (hV : Nat.card ↥(edgeZ1 chief K B ρ) = Nat.card (towerM K ⧸ towerT K) ^ 2) (hKer : Nat.card ↥(chiMidProjHom chief K chi B ρ).ker = 8) (H : ∀ (z : ↥(edgeZ1 chief K B ρ)), edgeLRead chief K B ρ z chi = 0) : False

The counting contradiction core (source-generic): the three engine counts against rank–nullity at π_* force 8 = 4.

theorem Q2Presentation.Induction.exists_chi_unit {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (chi : ↥(XT chief K)) (hchi : chi ≠ 0) : ∃ (t : ↥(towerT K)), ↑chi t = 1

A nonzero 𝒳_T-class has a χ-unit.

theorem Q2Presentation.Induction.edgeDelSurj_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (B : BoundaryPackage GQ2Profinite) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : EdgeDelSurj chief K B ρ

edgeDelSurj_gq2 — the LOCAL ∂-floor discharge (design §5 F-∂, local row): no 0 ≠ χ ∈ 𝒳_T kills every constraint defect at G_ℚ₂. Clause (d) of the citable keep at the ker χ̃-kernels (split-tower packaging), the χ-bit count |Hom_cont(G_ℚ₂, ℤ/2)|-slot = 8, and the V-count against rank–nullity at π_*.

theorem Q2Presentation.Induction.edgeDelSurj_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (ρ : boundaryFramedSurj boundaryPackage_GammaA (cChild chief K).fst (cChild chief K).snd) : EdgeDelSurj chief K boundaryPackage_GammaA ρ

edgeDelSurj_gammaA — the CANDIDATE ∂-floor discharge (design §5 F-∂, candidate row): the same dévissage with all three counts through N6's ledger corank engine (prop:defduality instances at the ker χ̃-kernels).