Route76 raw closers for the minimal-block kernel

This sidecar is a drop-in group-tower provider refining the Route75 minimal-block kernel frontier. It keeps the Route55 consumer shape, but makes two strict frontier changes:

• the least/Frattini side is routed through the finer Route72 split packets instead of the selected Route67/Route63 atoms visible in Route75;
• the raw-head side avoids two selected Route43 atoms by using the weaker same-tower head-action and lower-character formulations consumed downstream: not-pointwise-trivial action, and existential invariant character.

The literal R, M, T, C object and transport-action leaves remain the Route43 manuscript packets.

Smaller raw-head leaves

axiom Q2Presentation.Induction.MinimalBlockKernelRoute76RawClosers.rawHeadActionNotPointwiseTrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadActionNotPointwiseTrivialData D)

Route76 head-action packet for one raw tower.

This is weaker than the Route43 selected witness rawHeadActionNontrivialData: it records only that the head action is not pointwise trivial. The witness form is recovered theorem-level when needed.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute76RawClosers.rawLowerInvariantCharacterExistsData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerInvariantCharacterExistsData D)

Route76 lower-character packet for one raw tower.

This is weaker than the Route43 selected-character packet rawLowerNonzeroInvariantCharacterData: it records only the existential nonzero invariant character consumed by the Route44 semantic interface.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute76RawClosers.rawHeadActionNontrivialData_from_route76 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadActionNontrivialData D)

Recover the selected witness-form head-action packet from the Route76 not-pointwise-trivial formulation.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute76RawClosers.rawLowerNonzeroInvariantCharacterData_from_route76 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerNonzeroInvariantCharacterData D)

Recover the selected lower-character packet from the Route76 existential form.

Route60-compatible raw/head transport with Route76 head action

theorem Q2Presentation.Induction.MinimalBlockKernelRoute76RawClosers.rawHeadTransportPieces_from_route76RawClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces K F)

Route60 raw/head transport data with the head-action field supplied by the Route76 not-pointwise-trivial packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute76RawClosers.rawQuotientTowerData_from_route76RawClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Raw quotient tower obtained from the Route76 raw/head transport pieces.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute76RawClosers.rawSimpleHeadSemanticData_from_route76RawClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D)

Route44 same-tower simple-head semantic packet with the Route76 head-action and lower-character leaves.

Route55-shaped provider

theorem Q2Presentation.Induction.MinimalBlockKernelRoute76RawClosers.kernelRoute55Data_from_route76 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute55.KernelRoute55Data chief)

Route55-shaped packet using Route72 Frattini split data and Route76 raw head/lower-character refinements.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute76RawClosers.kernelRoute54Data_from_route76 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute54.KernelRoute54Data chief)

Route54 coherent data supplied through Route76.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute76RawClosers.consumedData_from_route76 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute53.ConsumedData chief)

Route53 consumed data supplied through Route76.

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

Route53 group/invariant route data supplied through Route76.

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

Group-tower provider using Route72 Frattini split data and Route76 raw head/lower-character refinements.

Public provider

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

Drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute74FrattiniClosers, with the Route75 selected Frattini atoms split through Route72 and two Route43 selected raw-head atoms replaced by weaker Route76 raw packets.