Proof of the route-ready Section 7 group/invariant packet

This sidecar closes the current route packet MinimalBlockGroupInvariantRouteData without using the residual axiom minimalBlock_groupInvariantRouteData.

The construction follows the manuscript tower of Section 7: first select one coherent lower subgroup/module tower, then attach dual-invariant vanishing and a raw invariant character to that same selected raw tower.

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

The route-ready Section 7 group/invariant packet follows from the coherent lower group/module tower plus the two lower invariant theorem-level closers, all attached to the same selected raw tower.

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

Route-ready replacement for minimalBlock_groupTowerData_from_groupInvariantRoute that uses the proved route packet above instead of the residual route axiom.

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

The selected pre-head tower is available from the proved route packet.

theorem Q2Presentation.Induction.minimalBlock_preheadInvariantCharacterData_from_groupInvariantRouteData_proven {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (D : MinimalBlockPreheadTowerData p chief), Nonempty (MinimalBlockPreheadInvariantCharacterData D)

The raw invariant character transported to the selected pre-head tower is available from the proved route packet.