theorem Q2Presentation.Induction.sec7_polar_zero_on_T {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hinv : ∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) (t : towerM K) : t ∈ towerT K → ∀ (m : towerM K), ((sec7SquareFamily chief K lam).polar t) m = 0

Clause (i), unconditional (the chain is proven).

theorem Q2Presentation.Induction.sec7_form_add_on_T {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hinv : ∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) (t t' : towerM K) (ht : t ∈ towerT K) : (sec7SquareFamily chief K lam).form (t + t') = (sec7SquareFamily chief K lam).form t + (sec7SquareFamily chief K lam).form t'

q_λ is additive on T.

def Q2Presentation.Induction.shearW {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hinv : ∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) : Submodule (ZMod 2) (towerM K)

The shear kernel W = {t ∈ T | q_λ t = 0}.

Equations

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

theorem Q2Presentation.Induction.shearW_le_T {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hinv : ∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) : shearW chief K lam hinv ≤ towerT K

theorem Q2Presentation.Induction.mem_shearW_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hinv : ∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) (t : towerM K) : t ∈ shearW chief K lam hinv ↔ t ∈ towerT K ∧ (sec7SquareFamily chief K lam).form t = 0

theorem Q2Presentation.Induction.shearW_stable {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hinv : ∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) (c : towerC K) (t : towerM K) (ht : t ∈ shearW chief K lam hinv) : ((towerActM K) c) t ∈ shearW chief K lam hinv

The shear kernel is C-stable.

theorem Q2Presentation.Induction.exists_form_one_of_ne {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hinv : ∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) (hne : ∃ t ∈ towerT K, (sec7SquareFamily chief K lam).form t ≠ 0) : ∃ t₀ ∈ towerT K, (sec7SquareFamily chief K lam).form t₀ = 1 ∧ t₀ ∉ shearW chief K lam hinv

If q_λ|_T ≠ 0, some t₀ ∈ T has q_λ t₀ = 1 and W misses it.

Slice 2: the quotient extension M̄ = M/W

theorem Induction2Shear.polar_comm {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (x y : Q2Presentation.Induction.towerM K) : ((Q2Presentation.Induction.sec7SquareFamily chief K lam).polar x) y = ((Q2Presentation.Induction.sec7SquareFamily chief K lam).polar y) x

The polar of a quadratic form is symmetric (char-2 polarization identity).

theorem Induction2Shear.form_descends {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (m w : Q2Presentation.Induction.towerM K) (hw : w ∈ Q2Presentation.Induction.shearW chief K lam hinv) : (Q2Presentation.Induction.sec7SquareFamily chief K lam).form (m + w) = (Q2Presentation.Induction.sec7SquareFamily chief K lam).form m

q_λ is constant on W-cosets.

@[reducible, inline]

abbrev Induction2Shear.Mbar {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Type

The quotient module M̄ = M/W.

Equations

• Induction2Shear.Mbar chief K lam hinv = (Q2Presentation.Induction.towerM K ⧸ Q2Presentation.Induction.shearW chief K lam hinv)

theorem Induction2Shear.neg_eq_self_M {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (x : Q2Presentation.Induction.towerM K) : -x = x

Char-2 negation is the identity.

def Induction2Shear.qbar {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Mbar chief K lam hinv → ZMod 2

The descended quadratic function q̄ : M̄ → F₂.

Equations

• Induction2Shear.qbar chief K lam hinv x = Quotient.liftOn' x (Q2Presentation.Induction.sec7SquareFamily chief K lam).form ⋯

@[simp]

theorem Induction2Shear.qbar_mk {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (m : Q2Presentation.Induction.towerM K) : qbar chief K lam hinv (Submodule.Quotient.mk m) = (Q2Presentation.Induction.sec7SquareFamily chief K lam).form m

def Induction2Shear.Tbar {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Submodule (ZMod 2) (Mbar chief K lam hinv)

The image of T in M̄.

Equations

• Induction2Shear.Tbar chief K lam hinv = Submodule.map (Q2Presentation.Induction.shearW chief K lam hinv).mkQ (Q2Presentation.Induction.towerT K)

theorem Induction2Shear.Tbar_eq_pair {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (t₀ : Q2Presentation.Induction.towerM K) (ht₀T : t₀ ∈ Q2Presentation.Induction.towerT K) (ht₀ : (Q2Presentation.Induction.sec7SquareFamily chief K lam).form t₀ = 1) (x : Mbar chief K lam hinv) : x ∈ Tbar chief K lam hinv → x = 0 ∨ x = Submodule.Quotient.mk t₀

The distinguished line generator.

theorem Induction2Shear.mk_t0_ne_zero {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (t₀ : Q2Presentation.Induction.towerM K) (ht₀ : (Q2Presentation.Induction.sec7SquareFamily chief K lam).form t₀ = 1) : Submodule.Quotient.mk t₀ ≠ 0

t̄₀ ≠ 0 in M̄.

Slice 3A: the C-action on M̄

theorem Induction3Shear.shearW_map_eq {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) : Submodule.map (↑((Q2Presentation.Induction.towerActM K) c)) (Q2Presentation.Induction.shearW chief K lam hinv) = Q2Presentation.Induction.shearW chief K lam hinv

W is carried onto itself by each c.

def Induction3Shear.actMbar {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) : Induction2Shear.Mbar chief K lam hinv ≃ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv

The descended action on M̄.

Equations

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

@[simp]

theorem Induction3Shear.actMbar_mk {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (m : Q2Presentation.Induction.towerM K) : (actMbar chief K lam hinv c) (Submodule.Quotient.mk m) = Submodule.Quotient.mk (((Q2Presentation.Induction.towerActM K) c) m)

theorem Induction3Shear.qbar_invariant {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (x : Induction2Shear.Mbar chief K lam hinv) : Induction2Shear.qbar chief K lam hinv ((actMbar chief K lam hinv c) x) = Induction2Shear.qbar chief K lam hinv x

q̄ is C-invariant.

theorem Induction3Shear.Tbar_stable {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (x : Induction2Shear.Mbar chief K lam hinv) (hx : x ∈ Induction2Shear.Tbar chief K lam hinv) : (actMbar chief K lam hinv c) x ∈ Induction2Shear.Tbar chief K lam hinv

T̄ is stable.

theorem Induction3Shear.actMbar_fixes_t0 {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (t₀ : Q2Presentation.Induction.towerM K) (ht₀T : t₀ ∈ Q2Presentation.Induction.towerT K) (ht₀ : (Q2Presentation.Induction.sec7SquareFamily chief K lam).form t₀ = 1) (c : Q2Presentation.Induction.towerC K) : (actMbar chief K lam hinv c) (Submodule.Quotient.mk t₀) = Submodule.Quotient.mk t₀

The action is trivial on the line T̄.

Slice 3B: the averaged splitting and the contradiction

theorem Induction3BShear.odd_nsmul_eq_self {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] {n : ℕ} (hn : Odd n) (x : V) : n • x = x

Odd-multiple identity in characteristic 2.

theorem Induction3BShear.Tbar_map_eq {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) : Submodule.map (↑(Induction3Shear.actMbar chief K lam hinv c)) (Induction2Shear.Tbar chief K lam hinv) = Induction2Shear.Tbar chief K lam hinv

T̄ maps onto itself under each c.

@[reducible, inline]

abbrev Induction3BShear.Vq {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Type

The head V̄ = M̄/T̄.

Equations

• Induction3BShear.Vq chief K lam hinv = (Induction2Shear.Mbar chief K lam hinv ⧸ Induction2Shear.Tbar chief K lam hinv)

def Induction3BShear.actVq {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) : Vq chief K lam hinv ≃ₗ[ZMod 2] Vq chief K lam hinv

The head action.

Equations

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

@[simp]

theorem Induction3BShear.actVq_mk {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (x : Induction2Shear.Mbar chief K lam hinv) : (actVq chief K lam hinv c) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((Induction3Shear.actMbar chief K lam hinv c) x)

theorem Induction3BShear.actMbar_mul_apply {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (a b : Q2Presentation.Induction.towerC K) (x : Induction2Shear.Mbar chief K lam hinv) : (Induction3Shear.actMbar chief K lam hinv (a * b)) x = (Induction3Shear.actMbar chief K lam hinv a) ((Induction3Shear.actMbar chief K lam hinv b) x)

Pointwise multiplicativity of the M̄-action.

theorem Induction3BShear.actVq_mul_apply {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (a b : Q2Presentation.Induction.towerC K) (v : Vq chief K lam hinv) : (actVq chief K lam hinv (a * b)) v = (actVq chief K lam hinv a) ((actVq chief K lam hinv b) v)

Pointwise multiplicativity of the head action.

theorem Induction3BShear.mkQ_equivariant {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (x : Induction2Shear.Mbar chief K lam hinv) : (Induction2Shear.Tbar chief K lam hinv).mkQ ((Induction3Shear.actMbar chief K lam hinv c) x) = (actVq chief K lam hinv c) ((Induction2Shear.Tbar chief K lam hinv).mkQ x)

The projection is equivariant.

theorem Induction3BShear.qbar_add_on_Tbar {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (x y : Induction2Shear.Mbar chief K lam hinv) (hx : x ∈ Induction2Shear.Tbar chief K lam hinv) (hy : y ∈ Induction2Shear.Tbar chief K lam hinv) : Induction2Shear.qbar chief K lam hinv (x + y) = Induction2Shear.qbar chief K lam hinv x + Induction2Shear.qbar chief K lam hinv y

q̄ is additive on T̄.

theorem Induction3BShear.eq_zero_of_mem_Tbar_qbar_zero {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (t₀ : Q2Presentation.Induction.towerM K) (ht₀T : t₀ ∈ Q2Presentation.Induction.towerT K) (ht₀ : (Q2Presentation.Induction.sec7SquareFamily chief K lam).form t₀ = 1) (x : Induction2Shear.Mbar chief K lam hinv) (hx : x ∈ Induction2Shear.Tbar chief K lam hinv) (hq : Induction2Shear.qbar chief K lam hinv x = 0) : x = 0

Elements of T̄ with q̄ = 0 vanish.

theorem Induction3CShear.actMbar_one_apply {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (x : Induction2Shear.Mbar chief K lam hinv) : (Induction3Shear.actMbar chief K lam hinv 1) x = x

theorem Induction3CShear.actVq_one_apply {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (v : Induction3BShear.Vq chief K lam hinv) : (Induction3BShear.actVq chief K lam hinv 1) v = v

def Induction3CShear.conjSec {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (L : Induction3BShear.Vq chief K lam hinv →ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv) : Induction3BShear.Vq chief K lam hinv →ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv

The conjugated section.

Equations

• Induction3CShear.conjSec chief K lam hinv c L = ↑(Induction3Shear.actMbar chief K lam hinv c) ∘ₗ L ∘ₗ ↑(Induction3BShear.actVq chief K lam hinv c⁻¹)

@[simp]

theorem Induction3CShear.conjSec_apply {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (L : Induction3BShear.Vq chief K lam hinv →ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv) (v : Induction3BShear.Vq chief K lam hinv) : (conjSec chief K lam hinv c L) v = (Induction3Shear.actMbar chief K lam hinv c) (L ((Induction3BShear.actVq chief K lam hinv c⁻¹) v))

theorem Induction3CShear.finite_towerC {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Finite (Q2Presentation.Induction.towerC K)

Finiteness of C (from the finite framed target).

noncomputable def Induction3CShear.avgSec {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (I : Subgroup (Q2Presentation.Induction.towerC K)) [Fintype ↥I] (σ₀ : Induction3BShear.Vq chief K lam hinv →ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv) : Induction3BShear.Vq chief K lam hinv →ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv

The averaged section: sum of the I-conjugates.

Equations

• Induction3CShear.avgSec chief K lam hinv I σ₀ = ∑ i : ↥I, Induction3CShear.conjSec chief K lam hinv (↑i) σ₀

theorem Induction3CShear.conjSec_mul_apply {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (a b : Q2Presentation.Induction.towerC K) (L : Induction3BShear.Vq chief K lam hinv →ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv) (v : Induction3BShear.Vq chief K lam hinv) : (conjSec chief K lam hinv a (conjSec chief K lam hinv b L)) v = (conjSec chief K lam hinv (a * b) L) v

theorem Induction3CShear.avgSec_section {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (I : Subgroup (Q2Presentation.Induction.towerC K)) [Fintype ↥I] (hodd : Odd (Nat.card ↥I)) (σ₀ : Induction3BShear.Vq chief K lam hinv →ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv) (hσ₀ : ∀ (w : Induction3BShear.Vq chief K lam hinv), (Induction2Shear.Tbar chief K lam hinv).mkQ (σ₀ w) = w) (v : Induction3BShear.Vq chief K lam hinv) : (Induction2Shear.Tbar chief K lam hinv).mkQ ((avgSec chief K lam hinv I σ₀) v) = v

The average of a section is a section (odd order).

theorem Induction3CShear.avgSec_equivariant {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (I : Subgroup (Q2Presentation.Induction.towerC K)) [Fintype ↥I] (σ₀ : Induction3BShear.Vq chief K lam hinv →ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv) (j : Q2Presentation.Induction.towerC K) (hj : j ∈ I) (v : Induction3BShear.Vq chief K lam hinv) : (Induction3Shear.actMbar chief K lam hinv j) ((avgSec chief K lam hinv I σ₀) v) = (avgSec chief K lam hinv I σ₀) ((Induction3BShear.actVq chief K lam hinv j) v)

The average is I-equivariant.

theorem Induction3DShear.sections_unique {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (I : Subgroup (Q2Presentation.Induction.towerC K)) (t₀ : Q2Presentation.Induction.towerM K) (hIvan : ∀ (f : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerM K)), (∀ t ∈ Q2Presentation.Induction.towerT K, f t = 0) → (∀ i ∈ I, ∀ (m : Q2Presentation.Induction.towerM K), f (((Q2Presentation.Induction.towerActM K) i) m) = f m) → f = 0) (ht₀T : t₀ ∈ Q2Presentation.Induction.towerT K) (ht₀ : (Q2Presentation.Induction.sec7SquareFamily chief K lam).form t₀ = 1) (σ σ' : Induction3BShear.Vq chief K lam hinv →ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv) (hσ : ∀ (v : Induction3BShear.Vq chief K lam hinv), (Induction2Shear.Tbar chief K lam hinv).mkQ (σ v) = v) (hσ' : ∀ (v : Induction3BShear.Vq chief K lam hinv), (Induction2Shear.Tbar chief K lam hinv).mkQ (σ' v) = v) (hσI : ∀ j ∈ I, ∀ (v : Induction3BShear.Vq chief K lam hinv), (Induction3Shear.actMbar chief K lam hinv j) (σ v) = σ ((Induction3BShear.actVq chief K lam hinv j) v)) (hσ'I : ∀ j ∈ I, ∀ (v : Induction3BShear.Vq chief K lam hinv), (Induction3Shear.actMbar chief K lam hinv j) (σ' v) = σ' ((Induction3BShear.actVq chief K lam hinv j) v)) : σ = σ'

Uniqueness of I-equivariant sections over the odd-inertia vanishing.

Slice 3E-pre: existence of the equivariant section

The manuscript provenance (l.3749–3760), formalized: the shears vanish by quadratic invariance (W was already quotiented out, so the defect of any V-trivial operator dies in M̄), hence the C-action on M̄ factors through the faithful image H_V = C/ker(actVq). H_V is a quotient of the tame H (its wild image is a normal 2-subgroup, trivial by head simplicity), so it is generated by σ̂, τ̂ with the tame relation and τ̂ of odd order. Ramified case: ⟨τ̂⟩ is odd normal with no nonzero fixed vectors on the simple head; unramified: H_V is odd cyclic. Either way the generic odd-averaging machinery (Lifting/OddSplitting) produces the C-equivariant section. Head simplicity is lem:simplehead: stable submodules pull back along M ↠ V̄ to Y-normal subgroups between S and P, and the chief property plus ⊆-minimality of K leave only ⊥ and ⊤.

The bundled action homs

def Induction3EShearBuild.actVqHom {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Q2Presentation.Induction.towerC K →* Induction3BShear.Vq chief K lam hinv ≃ₗ[ZMod 2] Induction3BShear.Vq chief K lam hinv

The head action as a monoid hom.

Equations

• Induction3EShearBuild.actVqHom chief K lam hinv = { toFun := Induction3BShear.actVq chief K lam hinv, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Induction3EShearBuild.actVqHom_apply {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (v : Induction3BShear.Vq chief K lam hinv) : ((actVqHom chief K lam hinv) c) v = (Induction3BShear.actVq chief K lam hinv c) v

def Induction3EShearBuild.actMbarHom {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Q2Presentation.Induction.towerC K →* Induction2Shear.Mbar chief K lam hinv ≃ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv

The M̄-action as a monoid hom.

Equations

• Induction3EShearBuild.actMbarHom chief K lam hinv = { toFun := Induction3Shear.actMbar chief K lam hinv, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Induction3EShearBuild.actMbarHom_apply {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (x : Induction2Shear.Mbar chief K lam hinv) : ((actMbarHom chief K lam hinv) c) x = (Induction3Shear.actMbar chief K lam hinv c) x

Shear rigidity: V-trivial operators are trivial on M̄

theorem Induction3EShearBuild.actMbar_eq_id_of_actVq_eq_id {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (hc : ∀ (v : Induction3BShear.Vq chief K lam hinv), (Induction3BShear.actVq chief K lam hinv c) v = v) (x : Induction2Shear.Mbar chief K lam hinv) : (Induction3Shear.actMbar chief K lam hinv c) x = x

If c acts trivially on the head V̄, it acts trivially on M̄: the defect against any vector lies in T̄ and has vanishing q̄ (quadratic invariance plus T ⊥ M), so it lies in the already-killed shear kernel.

The faithful acting quotient H_V

def Induction3EShearBuild.CVker {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Subgroup (Q2Presentation.Induction.towerC K)

The kernel of the head action.

Equations

• Induction3EShearBuild.CVker chief K lam hinv = (Induction3EShearBuild.actVqHom chief K lam hinv).ker

instance Induction3EShearBuild.instNormalTowerCCVker {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : (CVker chief K lam hinv).Normal

@[reducible, inline]

abbrev Induction3EShearBuild.HV {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Type

The faithful acting quotient H_V = C / ker(actVq).

Equations

• Induction3EShearBuild.HV chief K lam hinv = (Q2Presentation.Induction.towerC K ⧸ Induction3EShearBuild.CVker chief K lam hinv)

def Induction3EShearBuild.rhoV {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : HV chief K lam hinv →* Induction3BShear.Vq chief K lam hinv ≃ₗ[ZMod 2] Induction3BShear.Vq chief K lam hinv

The faithful head action of H_V.

Equations

• Induction3EShearBuild.rhoV chief K lam hinv = QuotientGroup.kerLift (Induction3EShearBuild.actVqHom chief K lam hinv)

theorem Induction3EShearBuild.rhoV_injective {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Function.Injective ⇑(rhoV chief K lam hinv)

@[simp]

theorem Induction3EShearBuild.rhoV_mk {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (v : Induction3BShear.Vq chief K lam hinv) : ((rhoV chief K lam hinv) ↑c) v = (Induction3BShear.actVq chief K lam hinv c) v

theorem Induction3EShearBuild.CVker_acts_trivially_Mbar {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (hc : c ∈ CVker chief K lam hinv) : (actMbarHom chief K lam hinv) c = 1

def Induction3EShearBuild.rhoM {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : HV chief K lam hinv →* Induction2Shear.Mbar chief K lam hinv ≃ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv

The descended M̄-action of H_V (well-defined by shear rigidity).

Equations

• Induction3EShearBuild.rhoM chief K lam hinv = QuotientGroup.lift (Induction3EShearBuild.CVker chief K lam hinv) (Induction3EShearBuild.actMbarHom chief K lam hinv) ⋯

@[simp]

theorem Induction3EShearBuild.rhoM_mk {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (x : Induction2Shear.Mbar chief K lam hinv) : ((rhoM chief K lam hinv) ↑c) x = (Induction3Shear.actMbar chief K lam hinv c) x

theorem Induction3EShearBuild.rho_comm {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (h : HV chief K lam hinv) (x : Induction2Shear.Mbar chief K lam hinv) : (Induction2Shear.Tbar chief K lam hinv).mkQ (((rhoM chief K lam hinv) h) x) = ((rhoV chief K lam hinv) h) ((Induction2Shear.Tbar chief K lam hinv).mkQ x)

theorem Induction3EShearBuild.rho_ker_fixed {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (t₀ : Q2Presentation.Induction.towerM K) (ht₀T : t₀ ∈ Q2Presentation.Induction.towerT K) (ht₀ : (Q2Presentation.Induction.sec7SquareFamily chief K lam).form t₀ = 1) (h : HV chief K lam hinv) (x : Induction2Shear.Mbar chief K lam hinv) (hx : (Induction2Shear.Tbar chief K lam hinv).mkQ x = 0) : ((rhoM chief K lam hinv) h) x = x

The full projection M → V̄ and head simplicity

def Induction3EShearBuild.bigProj {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Q2Presentation.Induction.towerM K →ₗ[ZMod 2] Induction3BShear.Vq chief K lam hinv

The composite projection M ↠ M̄ ↠ V̄.

Equations

• Induction3EShearBuild.bigProj chief K lam hinv = (Induction2Shear.Tbar chief K lam hinv).mkQ ∘ₗ (Q2Presentation.Induction.shearW chief K lam hinv).mkQ

theorem Induction3EShearBuild.bigProj_surjective {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Function.Surjective ⇑(bigProj chief K lam hinv)

theorem Induction3EShearBuild.bigProj_equivariant {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (c : Q2Presentation.Induction.towerC K) (m : Q2Presentation.Induction.towerM K) : (bigProj chief K lam hinv) (((Q2Presentation.Induction.towerActM K) c) m) = (Induction3BShear.actVq chief K lam hinv c) ((bigProj chief K lam hinv) m)

theorem Induction3EShearBuild.bigProj_zero_of_mem_towerT {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (m : Q2Presentation.Induction.towerM K) (hm : m ∈ Q2Presentation.Induction.towerT K) : (bigProj chief K lam hinv) m = 0

theorem Induction3EShearBuild.neg_eq_self_Vq {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (w : Induction3BShear.Vq chief K lam hinv) : -w = w

Char-2 negation is the identity on V̄.

def Induction3EShearBuild.thetaMap {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (k : ↥K.Ksub) : Induction3BShear.Vq chief K lam hinv

The projection value of a kernel element.

Equations

• Induction3EShearBuild.thetaMap chief K lam hinv k = (Induction3EShearBuild.bigProj chief K lam hinv) (Additive.ofMul ((QuotientGroup.mk' (frattini ↥K.Ksub)) k))

theorem Induction3EShearBuild.thetaMap_mul {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (k₁ k₂ : ↥K.Ksub) : thetaMap chief K lam hinv (k₁ * k₂) = thetaMap chief K lam hinv k₁ + thetaMap chief K lam hinv k₂

theorem Induction3EShearBuild.thetaMap_inv {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (k : ↥K.Ksub) : thetaMap chief K lam hinv k⁻¹ = thetaMap chief K lam hinv k

theorem Induction3EShearBuild.thetaMap_one {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : thetaMap chief K lam hinv 1 = 0

theorem Induction3EShearBuild.thetaMap_conj {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (g : p.fst.Y) (k : ↥K.Ksub) : thetaMap chief K lam hinv ((Q2Presentation.Induction.kernelConjAut K g) k) = (Induction3BShear.actVq chief K lam hinv ↑g) (thetaMap chief K lam hinv k)

theorem Induction3EShearBuild.Vq_stable_bot_or_top {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (U : Submodule (ZMod 2) (Induction3BShear.Vq chief K lam hinv)) (hstab : ∀ (c : Q2Presentation.Induction.towerC K), ∀ v ∈ U, (Induction3BShear.actVq chief K lam hinv c) v ∈ U) : U = ⊥ ∨ U = ⊤

Head simplicity (lem:simplehead core): a C-stable submodule of V̄ is ⊥ or ⊤ — pull back along bigProj and lift to a Y-normal subgroup between S and P; the chief dichotomy plus ⊆-minimality of K decide it.

theorem Induction3EShearBuild.Vq_nontrivial {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Nontrivial (Induction3BShear.Vq chief K lam hinv)

Normal 2-subgroups of H_V are trivial

def Induction3EShearBuild.fixedSubmodule {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (A : Subgroup (HV chief K lam hinv)) : Submodule (ZMod 2) (Induction3BShear.Vq chief K lam hinv)

The fixed submodule of a subgroup of H_V.

Equations

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

theorem Induction3EShearBuild.mem_fixedSubmodule {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (A : Subgroup (HV chief K lam hinv)) (v : Induction3BShear.Vq chief K lam hinv) : v ∈ fixedSubmodule chief K lam hinv A ↔ ∀ a ∈ A, ((rhoV chief K lam hinv) a) v = v

theorem Induction3EShearBuild.fixedSubmodule_stable {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (A : Subgroup (HV chief K lam hinv)) (hA : A.Normal) (c : Q2Presentation.Induction.towerC K) (v : Induction3BShear.Vq chief K lam hinv) (hv : v ∈ fixedSubmodule chief K lam hinv A) : (Induction3BShear.actVq chief K lam hinv c) v ∈ fixedSubmodule chief K lam hinv A

theorem Induction3EShearBuild.two_dvd_card_Vq {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : 2 ∣ Nat.card (Induction3BShear.Vq chief K lam hinv)

Char-2 involution kernel: 2 ∣ card of a nontrivial finite ZMod 2 module.

theorem Induction3EShearBuild.normal_two_subgroup_eq_bot {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (N : Subgroup (HV chief K lam hinv)) (hN : N.Normal) (h2 : IsPGroup 2 ↥N) : N = ⊥

Normal 2-subgroups of H_V act with a nonzero fixed space, which is stable, hence everything by head simplicity; faithfulness kills them.

The tame structure of H_V

def Induction3EShearBuild.sigmaH {p : Q2Presentation.Induction.FramedPair} : p.fst.H

The frame's tame generators, pushed into H.

Equations

• Induction3EShearBuild.sigmaH = (ProfiniteGrp.Hom.hom p.snd.alpha) Q2Presentation.tameSigma

def Induction3EShearBuild.tauH {p : Q2Presentation.Induction.FramedPair} : p.fst.H

The frame's tame inertia generator, pushed into H.

Equations

• Induction3EShearBuild.tauH = (ProfiniteGrp.Hom.hom p.snd.alpha) Q2Presentation.tameTau

theorem Induction3EShearBuild.tame_rel_H {p : Q2Presentation.Induction.FramedPair} : sigmaH⁻¹ * tauH * sigmaH = tauH ^ 2

The tame relation holds in H.

theorem Induction3EShearBuild.mem_closure_frame_gens {p : Q2Presentation.Induction.FramedPair} (h : p.fst.H) : h ∈ Subgroup.closure {sigmaH, tauH}

H is generated by the frame's tame generators: the topological generation of Ttame pushes through the continuous surjection α onto the finite discrete H. The argument runs in the topological carrier of ofFiniteGrp H; the resulting membership transfers to p.1.H by defeq.

def Induction3EShearBuild.psiYH {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : p.fst.Y →* HV chief K lam hinv

The composite Y → C → H_V.

Equations

• Induction3EShearBuild.psiYH chief K lam hinv = (QuotientGroup.mk' (Induction3EShearBuild.CVker chief K lam hinv)).comp (QuotientGroup.mk' K.Ksub)

theorem Induction3EShearBuild.psiYH_surjective {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Function.Surjective ⇑(psiYH chief K lam hinv)

theorem Induction3EShearBuild.psiYH_LY_dies {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (y : p.fst.Y) (hy : y ∈ p.fst.LY) : (psiYH chief K lam hinv) y = 1

The wild part dies in H_V: its image is a normal 2-subgroup.

theorem Induction3EShearBuild.psiYH_ker_piY {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (y : p.fst.Y) (hy : y ∈ p.fst.piY.ker) : (psiYH chief K lam hinv) y = 1

noncomputable def Induction3EShearBuild.phiH {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : p.fst.H →* HV chief K lam hinv

The factored map H → H_V (the wild part dies, so the composite factors through π_Y).

Equations

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

theorem Induction3EShearBuild.phiH_piY {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (y : p.fst.Y) : (phiH chief K lam hinv) (p.fst.piY y) = (psiYH chief K lam hinv) y

theorem Induction3EShearBuild.phiH_surjective {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Function.Surjective ⇑(phiH chief K lam hinv)

noncomputable def Induction3EShearBuild.sHV {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : HV chief K lam hinv

The tame generators of H_V.

Equations

• Induction3EShearBuild.sHV chief K lam hinv = (Induction3EShearBuild.phiH chief K lam hinv) Induction3EShearBuild.sigmaH

noncomputable def Induction3EShearBuild.tHV {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : HV chief K lam hinv

The tame inertia generator of H_V.

Equations

• Induction3EShearBuild.tHV chief K lam hinv = (Induction3EShearBuild.phiH chief K lam hinv) Induction3EShearBuild.tauH

theorem Induction3EShearBuild.tame_rel_HV {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : (sHV chief K lam hinv)⁻¹ * tHV chief K lam hinv * sHV chief K lam hinv = tHV chief K lam hinv ^ 2

theorem Induction3EShearBuild.HV_gen {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Subgroup.closure {sHV chief K lam hinv, tHV chief K lam hinv} = ⊤

theorem Induction3EShearBuild.tHV_odd {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) : Odd (orderOf (tHV chief K lam hinv))

The main existence theorem

theorem Induction3EShearBuild.shearEquivariantSection_exists {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (t₀ : Q2Presentation.Induction.towerM K) (ht₀T : t₀ ∈ Q2Presentation.Induction.towerT K) (ht₀ : (Q2Presentation.Induction.sec7SquareFamily chief K lam).form t₀ = 1) : ∃ (σA : Induction3BShear.Vq chief K lam hinv →ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv), (∀ (v : Induction3BShear.Vq chief K lam hinv), (Induction2Shear.Tbar chief K lam hinv).mkQ (σA v) = v) ∧ ∀ (c : Q2Presentation.Induction.towerC K) (v : Induction3BShear.Vq chief K lam hinv), (Induction3Shear.actMbar chief K lam hinv c) (σA v) = σA ((Induction3BShear.actVq chief K lam hinv c) v)

Existence of the C-equivariant section (prop:simpleheaddet clause (ii) core, manuscript l.3749–3760), fully proven: shear rigidity factors the action through the faithful tame quotient H_V; the ramified case averages over the odd normal ⟨τ̂⟩ (no nonzero fixed vectors on the simple head) and the unramified case over the odd cyclic H_V itself.

theorem Q2Presentation.Induction.sec7_shearEquivariantSection {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (towerR chief K)) (hinv : ∀ (c : towerC K), lam ∘ₗ ↑((towerActR chief K) c) = lam) (t₀ : towerM K) (ht₀T : t₀ ∈ towerT K) (ht₀ : (sec7SquareFamily chief K lam).form t₀ = 1) : ∃ (σA : Induction3BShear.Vq chief K lam hinv →ₗ[ZMod 2] Induction2Shear.Mbar chief K lam hinv), (∀ (v : Induction3BShear.Vq chief K lam hinv), (Induction2Shear.Tbar chief K lam hinv).mkQ (σA v) = v) ∧ ∀ (c : towerC K) (v : Induction3BShear.Vq chief K lam hinv), (Induction3Shear.actMbar chief K lam hinv c) (σA v) = σA ((Induction3BShear.actVq chief K lam hinv c) v)

The shear-splitting residual, PROVEN (prop:simpleheaddet clause (ii) core; manuscript l.3749-3760): given a T-vector of form value 1, the shear extension 0 → T̄ → M̄ → V → 0 splits C-equivariantly. The shears vanish by quadratic invariance, so the action factors through the faithful tame quotient H_V; the ramified case averages over the odd normal ⟨τ̂⟩ (no nonzero fixed vectors on the simple head, norm-trick rigidity), the unramified case over the odd cyclic H_V itself (Induction3EShearBuild.shearEquivariantSection_exists).

theorem Induction3EShear.sec7_form_zero_on_T_final {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Q2Presentation.Induction.towerR chief K)) (hinv : ∀ (c : Q2Presentation.Induction.towerC K), lam ∘ₗ ↑((Q2Presentation.Induction.towerActR chief K) c) = lam) (t : Q2Presentation.Induction.towerM K) : t ∈ Q2Presentation.Induction.towerT K → (Q2Presentation.Induction.sec7SquareFamily chief K lam).form t = 0

Clause (ii) (prop:simpleheaddet): the invariant square family vanishes on T — the shear/odd-averaging contradiction against (M^∨)^C = 0.

theorem Induction3EShear.sec7_simpleHeadCruxData3_proven {p : Q2Presentation.Induction.FramedPair} (chief : Q2Presentation.Induction.FirstNonScalarChiefFactor p) (K : Q2Presentation.Induction.KernelMinimal chief.toNonScalarChiefFactor) : Nonempty (Q2Presentation.Induction.Sec7SimpleHeadCruxData3 chief K)

Leaf #1, clause (ii) PROVED: the crux packet exists.