Lower invariant proofs for Section 7 minimal blocks

This sidecar targets the two remaining representation-invariant Section 7 residuals:

• minimalBlock_dualInvariantVanishesData;
• minimalBlock_rawInvariantCharacterData.

The manuscript input is lem:simplehead on pages 40-42: invariant functionals on M vanish because they factor through the unique nontrivial simple head, and the lower scalar/Frattini layers provide the invariant determinant characters in (R^vee)^C.

The theorem-level replacements below keep that split explicit:

• dual-invariant vanishing follows from a radical-killing statement plus no-trivial-dual-invariant statement on the quotient head M/T;
• raw invariant character data follows from a fixed scalar quotient of the lower Frattini layer R.

The induced action on the raw simple head

def Q2Presentation.Induction.minimalBlock_rawHeadAction {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (c : D.C) : D.M ⧸ D.T →ₗ[ZMod 2] D.M ⧸ D.T

The C-action on the quotient head M/T induced from the raw tower action on M.

Equations

• Q2Presentation.Induction.minimalBlock_rawHeadAction D c = D.T.mapQ D.T ↑(D.actM c) ⋯

@[simp]

theorem Q2Presentation.Induction.minimalBlock_rawHeadAction_mk {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (c : D.C) (m : D.M) : (minimalBlock_rawHeadAction D c) (Submodule.Quotient.mk m) = Submodule.Quotient.mk ((D.actM c) m)

def Q2Presentation.Induction.minimalBlock_descendFunctionalToHead {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (phi : Module.Dual (ZMod 2) D.M) (hkill : ∀ t ∈ D.T, phi t = 0) : Module.Dual (ZMod 2) (D.M ⧸ D.T)

Descend a linear functional on M to M/T once it kills T.

Equations

• Q2Presentation.Induction.minimalBlock_descendFunctionalToHead D phi hkill = D.T.liftQ phi ⋯

@[simp]

theorem Q2Presentation.Induction.minimalBlock_descendFunctionalToHead_mk {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (phi : Module.Dual (ZMod 2) D.M) (hkill : ∀ t ∈ D.T, phi t = 0) (m : D.M) : (minimalBlock_descendFunctionalToHead D phi hkill) (Submodule.Quotient.mk m) = phi m

theorem Q2Presentation.Induction.minimalBlock_descendFunctionalToHead_invariant {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (phi : Module.Dual (ZMod 2) D.M) (hkill : ∀ t ∈ D.T, phi t = 0) (hphi : ∀ (c : D.C), phi ∘ₗ ↑(D.actM c) = phi) (c : D.C) : minimalBlock_descendFunctionalToHead D phi hkill ∘ₗ minimalBlock_rawHeadAction D c = minimalBlock_descendFunctionalToHead D phi hkill

Invariant functionals on M descend to invariant functionals on the head M/T, provided they kill T.

Dual-invariant vanishing from simple-head representation packets

structure Q2Presentation.Induction.MinimalBlockRawHeadQuotientNoTrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Prop

A narrower representation-theory packet for the manuscript's (M^vee)^C = 0 conclusion.

The first field says invariant functionals kill the radical/prehead layer T. The second field says the quotient head M/T has no trivial dual invariant.

• invariant_functionals_kill_T (phi : Module.Dual (ZMod 2) D.M) : (∀ (c : D.C), phi ∘ₗ ↑(D.actM c) = phi) → ∀ t ∈ D.T, phi t = 0
• head_dualInv_zero (psi : Module.Dual (ZMod 2) (D.M ⧸ D.T)) : (∀ (c : D.C), psi ∘ₗ minimalBlock_rawHeadAction D c = psi) → psi = 0

def Q2Presentation.Induction.MinimalBlockDualInvariantVanishesData.ofRawHeadQuotientNoTrivial {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (H : MinimalBlockRawHeadQuotientNoTrivialData D) : MinimalBlockDualInvariantVanishesData D

Convert the quotient-head no-trivial-invariant packet into the current raw dual-invariant-vanishing data.

Equations

• ⋯ = ⋯

axiom Q2Presentation.Induction.minimalBlock_rawHeadQuotientNoTrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadQuotientNoTrivialData D)

Residual lower representation-theory packet replacing the direct (M^vee)^C = 0 assertion.

theorem Q2Presentation.Induction.minimalBlock_dualInvariantVanishesData_from_headQuotientNoTrivial {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockDualInvariantVanishesData D)

Theorem-level replacement for minimalBlock_dualInvariantVanishesData, reduced to radical-killing plus no trivial dual invariant on the simple head.

Raw invariant characters from lower scalar quotient data

structure Q2Presentation.Induction.MinimalBlockRawLowerScalarQuotientData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Type

Lower scalar quotient data for the Frattini layer R.

This is the raw-tower form of the manuscript statement that the lower scalar layers produce a C-invariant character of R; over F_2, surjectivity forces the character to be nonzero.

• quotient : Module.Dual (ZMod 2) D.R
• quotient_surjective : Function.Surjective ⇑self.quotient
• quotient_invariant (c : D.C) : self.quotient ∘ₗ ↑(D.actR c) = self.quotient

def Q2Presentation.Induction.MinimalBlockRawInvariantCharacterData.ofLowerScalarQuotient {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (Q : MinimalBlockRawLowerScalarQuotientData D) : MinimalBlockRawInvariantCharacterData D

A lower scalar quotient gives the raw nonzero invariant determinant character packet.

Equations

• ⋯ = ⋯

axiom Q2Presentation.Induction.minimalBlock_rawLowerScalarQuotientData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerScalarQuotientData D)

Residual lower-scalar packet replacing the direct nonzero invariant-character assertion.

theorem Q2Presentation.Induction.minimalBlock_rawInvariantCharacterData_from_lowerScalarQuotient {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantCharacterData D)

Theorem-level replacement for minimalBlock_rawInvariantCharacterData, reduced to a scalar quotient of the lower Frattini layer.

Reassembly hooks for existing Section 7 routes

theorem Q2Presentation.Induction.minimalBlock_preheadTowerData_from_invariantLowerProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockPreheadTowerData p chief)

The pre-head tower assembled using the lower-invariant replacement for dual-invariant vanishing.

theorem Q2Presentation.Induction.minimalBlock_preheadInvariantCharacterData_from_lowerScalarQuotient {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (V : MinimalBlockDualInvariantVanishesData D) : Nonempty (MinimalBlockPreheadInvariantCharacterData (MinimalBlockPreheadTowerData.ofRaw D V))

The pre-head invariant-character packet assembled from a raw lower scalar quotient, after the pre-head tower has been built from the same raw tower.

theorem Q2Presentation.Induction.minimalBlock_simpleHeadSemanticData_from_invariantLowerProofs {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelChoiceSemanticData p chief} {R : MinimalBlockFrattiniKernelSemanticData K} (E : MinimalBlockModuleExtractionSemanticData K R) : Nonempty (MinimalBlockSimpleHeadSemanticData E)

Reassemble the simple-head semantic packet while replacing the two current invariant residuals by the lower representation/scalar quotient packets.

theorem Q2Presentation.Induction.minimalBlock_groupTowerData_from_lowerGroupModuleInvariantLowerProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Reassemble MinimalBlockGroupTowerData from the coherent lower group/module packet while also replacing the two invariant residuals by their lower representation-theoretic packets.