Proof/refinement sidecar for the actual Section 7 group-invariant packet

This file does not edit the routed capstone. It records two theorem-level interfaces around the remaining final-closure packet minimalBlock_groupInvariantActualData.

First, the current aggregate packet is reassembled from the existing lower group/module, simple-head quotient, and lower scalar quotient APIs. This proves that the aggregate is not logically stronger than the already split same-tower interfaces.

Second, the route below uses a strictly smaller coherent packet. The current framed route only consumes:

• the chosen lower subgroup/module tower;
• dual-invariant vanishing on the raw module from that tower;
• a raw nonzero invariant determinant character on the same Frattini layer.

It does not consume the stronger quotient-head packet or the stronger lower scalar quotient packet directly. The smaller packet below keeps those consumed facts attached to one selected lower tower and routes the final framed-count argument without using minimalBlock_groupInvariantActualData.

Reassemble the current actual packet from existing APIs

theorem Q2Presentation.Induction.minimalBlock_groupInvariantActualData_proven {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantActualData chief)

The current actual group/invariant packet follows from the already split lower group/module, head quotient, and lower scalar quotient APIs, all tied to the same selected lower tower.

Smaller route-ready group/invariant packet

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

Route-ready Section 7 group/invariant data on one selected lower tower.

This is strictly weaker than MinimalBlockGroupInvariantActualData: it keeps the coherent lower subgroup/module tower, but it stores only the two facts actually needed to build MinimalBlockGroupTowerData, namely (M^vee)^C = 0 and a raw nonzero invariant character on R. It does not require the stronger head-quotient no-trivial packet or the stronger lower scalar quotient packet.

• lower : MinimalBlockLowerGroupModuleData chief
• dualInvariant : MinimalBlockDualInvariantVanishesData self.lower.rawTowerData
• rawInvariantCharacter : MinimalBlockRawInvariantCharacterData self.lower.rawTowerData

@[reducible, inline]

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

The raw tower selected by the route packet.

Equations

• D.rawTowerData = D.lower.rawTowerData

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

The group tower assembled from the smaller route packet.

Equations

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

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

The pre-head tower selected by the route packet.

Equations

• D.preheadTowerData = D.groupTowerData.preheadTowerData

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

The pre-head invariant character selected by the route packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockGroupInvariantRouteData.ofActual {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockGroupInvariantActualData chief) : MinimalBlockGroupInvariantRouteData chief

Forget the stronger current actual packet to the smaller route packet.

Equations

• Q2Presentation.Induction.MinimalBlockGroupInvariantRouteData.ofActual D = { lower := D.lower, dualInvariant := ⋯, rawInvariantCharacter := ⋯ }

axiom Q2Presentation.Induction.minimalBlock_groupInvariantRouteData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Smaller residual replacing minimalBlock_groupInvariantActualData for routes that only need the realized lower tower, dual-invariant vanishing, and raw invariant character.

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

The smaller route packet is a projection of the current actual packet.

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

Route-ready replacement for minimalBlock_groupTowerData_from_groupInvariantActual, using the smaller group/invariant route packet.

Count route through the smaller group/invariant packet

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

Nonterminal Fourier branch using the smaller actual group/invariant route, the current coherent lower pushout packet, and the framed marked-quotient route.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_groupInvariantRouteProofs (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)

Recursive branch using the smaller actual group/invariant route.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_groupInvariantRouteProofs (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)

Recursion step using the smaller actual group/invariant route.

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

Boundary-framed count equality through the smaller actual group/invariant route.

theorem Q2Presentation.Induction.finite_surjection_counts_equal_groupInvariantRouteProofs (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 minimalBlock_groupInvariantActualData replaced by the smaller route packet minimalBlock_groupInvariantRouteData.