Lower group/invariant proof reductions for Section 7

This sidecar closes or narrows the three current lower group/invariant packets used by the final Section 7 route:

• minimalBlock_lowerGroupModuleData;
• minimalBlock_rawHeadQuotientNoTrivialData;
• minimalBlock_rawLowerScalarQuotientData.

It does not edit routed files. The replacements follow the manuscript tower in Section 7, pages 40--42: choose the least K, set R = Phi(K), extract M = K/R, T, and C, use the simple-head vanishing (M^vee)^C = 0, and replace a surjective lower scalar quotient by the weaker raw nonzero invariant character over F_2.

Lower group/module packet from existing manuscript-shaped pieces

theorem Q2Presentation.Induction.minimalBlock_lowerGroupModuleData_from_lowerGroupProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

The coherent lower group/module packet follows from the six smaller manuscript-shaped lower pieces already split out in the semantic sidecars: least K, Frattini collapse, raw module/action data, the K/R ~= M bridge, and nontriviality of the simple head.

Head-quotient no-trivial packet from direct dual-invariant vanishing

def Q2Presentation.Induction.minimalBlock_liftHeadFunctionalToRaw {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (psi : Module.Dual (ZMod 2) (D.M ⧸ D.T)) : Module.Dual (ZMod 2) D.M

Compose a quotient-head functional with M -> M/T.

Equations

• Q2Presentation.Induction.minimalBlock_liftHeadFunctionalToRaw D psi = psi ∘ₗ D.T.mkQ

@[simp]

theorem Q2Presentation.Induction.minimalBlock_liftHeadFunctionalToRaw_apply {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (psi : Module.Dual (ZMod 2) (D.M ⧸ D.T)) (m : D.M) : (minimalBlock_liftHeadFunctionalToRaw D psi) m = psi (Submodule.Quotient.mk m)

theorem Q2Presentation.Induction.minimalBlock_liftHeadFunctionalToRaw_invariant {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (psi : Module.Dual (ZMod 2) (D.M ⧸ D.T)) (hpsi : ∀ (c : D.C), psi ∘ₗ minimalBlock_rawHeadAction D c = psi) (c : D.C) : minimalBlock_liftHeadFunctionalToRaw D psi ∘ₗ ↑(D.actM c) = minimalBlock_liftHeadFunctionalToRaw D psi

Invariance of a functional on M/T gives invariance of its pullback to M.

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

Direct vanishing of (M^vee)^C implies the quotient-head no-trivial packet.

The first field is immediate because every invariant functional on M is zero. For the second field, pull an invariant functional on M/T back to M; the pullback is invariant and hence zero, so the original quotient functional is zero by quotient extensionality.

Equations

• ⋯ = ⋯

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

Theorem-level replacement for minimalBlock_rawHeadQuotientNoTrivialData, reduced to the smaller direct dual-invariant vanishing packet.

Lower scalar quotient from the weaker raw invariant character packet

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

A raw nonzero invariant character on R supplies the lower scalar quotient. The quotient-surjectivity field is automatic over F_2.

Equations

• Q2Presentation.Induction.MinimalBlockRawLowerScalarQuotientData.ofRawInvariantCharacter X = { quotient := Classical.choose ⋯, quotient_surjective := ⋯, quotient_invariant := ⋯ }

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

Theorem-level replacement for minimalBlock_rawLowerScalarQuotientData, reduced to the smaller raw nonzero invariant-character packet.

Route packet with the three broad lower packets removed from closure

theorem Q2Presentation.Induction.minimalBlock_groupInvariantRouteData_from_lowerGroupProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route-ready Section 7 group/invariant packet with the three current lower group/invariant packets removed from the axiom closure.

The lower tower is assembled from the six smaller group/module pieces, while the two invariant fields are supplied by the direct dual-invariant and raw invariant-character packets.

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

Group-tower reassembly through the lower-proof route packet.