Actual lower group/invariant packet for Section 7 minimal blocks

This sidecar sharpens the current Section 7 lower group/module/invariant boundary without editing the routed files. The existing lower route consumes three residual packets independently:

• minimalBlock_lowerGroupModuleData;
• minimalBlock_rawHeadQuotientNoTrivialData;
• minimalBlock_rawLowerScalarQuotientData.

The manuscript uses one object: the chosen subgroup tower R = Phi(K) <= K <= L_Y, the quotient M = K/R, the lower target C = Y/K, the simple head M/T, and the scalar Frattini quotient. The packet below records that one-object boundary. It still leaves one finite group/representation theorem as a residual, but it prevents the final route from mixing unrelated lower towers, head-invariant data, and scalar quotients.

One lower group/invariant object

structure Q2Presentation.Induction.MinimalBlockGroupInvariantActualData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Coherent Section 7 lower group/invariant data for one non-scalar chief factor.

The lower field fixes the actual lower tower: least K, literal R = Phi(K), the raw modules R, M, T, the lower quotient C, the induced actions, the K/R ~= M bridge, and nontriviality of the head.

The head and scalar fields are attached to lower.rawTowerData, so they apply to that same tower rather than to an arbitrary separately chosen raw module layer.

• lower : MinimalBlockLowerGroupModuleData chief
• headNoTrivial : MinimalBlockRawHeadQuotientNoTrivialData self.lower.rawTowerData
• lowerScalarQuotient : MinimalBlockRawLowerScalarQuotientData self.lower.rawTowerData

@[reducible, inline]

abbrev Q2Presentation.Induction.MinimalBlockGroupInvariantActualData.rawTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockGroupInvariantActualData chief) : MinimalBlockRawTowerData p chief

The canonical raw tower selected by the actual lower packet.

Equations

• D.rawTowerData = D.lower.rawTowerData

def Q2Presentation.Induction.MinimalBlockGroupInvariantActualData.dualInvariantData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockGroupInvariantActualData chief) : MinimalBlockDualInvariantVanishesData D.rawTowerData

Dual-invariant vanishing on M, proved from the head quotient packet attached to the selected raw tower.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockGroupInvariantActualData.rawInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockGroupInvariantActualData chief) : MinimalBlockRawInvariantCharacterData D.rawTowerData

The raw invariant determinant character, proved from the lower scalar quotient attached to the selected raw tower.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockGroupInvariantActualData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockGroupInvariantActualData chief) : MinimalBlockGroupTowerData p chief

The realized group tower assembled from the one coherent lower/invariant object.

Equations

• D.groupTowerData = D.lower.groupTowerData ⋯ ⋯

def Q2Presentation.Induction.MinimalBlockGroupInvariantActualData.preheadTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockGroupInvariantActualData chief) : MinimalBlockPreheadTowerData p chief

The selected pre-head tower obtained from the same actual object.

Equations

• D.preheadTowerData = D.groupTowerData.preheadTowerData

def Q2Presentation.Induction.MinimalBlockGroupInvariantActualData.preheadInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockGroupInvariantActualData chief) : MinimalBlockPreheadInvariantCharacterData D.preheadTowerData

The selected pre-head invariant character obtained from the same actual object.

Equations

• ⋯ = ⋯

axiom Q2Presentation.Induction.minimalBlock_groupInvariantActualData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantActualData chief)

Remaining Section 7 finite group/representation theorem.

This is the sharpened boundary left by this sidecar: for the chosen first non-scalar chief factor, construct one subgroup tower R = Phi(K) <= K <= L_Y and prove, on that same tower, the head has no trivial dual invariant and the lower Frattini layer has a C-invariant scalar quotient.

Projections and theorem-level replacements

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

The old lower group/module packet is a projection of the actual packet.

theorem Q2Presentation.Induction.minimalBlock_canonicalLowerInvariantPackets_from_groupInvariantActual {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (D : MinimalBlockLowerGroupModuleData chief), Nonempty (MinimalBlockRawHeadQuotientNoTrivialData D.rawTowerData) ∧ Nonempty (MinimalBlockRawLowerScalarQuotientData D.rawTowerData)

The two lower invariant packets are available on the canonical raw tower selected by the same lower group/module object.

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

Route-ready replacement for minimalBlock_groupTowerData_from_lowerGroupModuleInvariantLowerProofs, with the three current lower group/module/invariant axioms replaced by one actual packet.

Count route through the sharper lower packet

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_groupInvariantActual (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

Nonterminal Fourier branch using the actual lower group/invariant packet and the existing lower marked-quotient Section 8 route.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_groupInvariantActual (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_groupInvariantActual (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_groupInvariantActual (p : FramedPair) : framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_groupInvariantActual (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Equal finite surjection counts with the three current lower group/module/invariant packets replaced by the one actual lower packet above.