Route98 kernel closers for the minimal-block route

This sidecar is isolated from IntegratedCurrentRouteProofs98. It provides a drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute95Closers and keeps two audit routes available:

• minimalBlock_groupTowerData_from_kernelRoute98Closers is the compact route. It replaces the four Route98 Section 7 kernel packets by the two coherent lower/head packets used by Route46.
• minimalBlock_groupTowerData_from_kernelRoute98Closers_fieldSplit is the fully lowered audit route. It avoids the four Route98 packet names by using Route40's field-level least/Frattini/raw/head split.

The supervisor can choose which provider to integrate.

Compact two-packet provider

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

Route98 compact lower tower provider.

This is the coherent manuscript lower tower K, R = Phi(K), M = K/R, T, and C, with quotient actions and head nontriviality tied to one selected tower.

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

Route98 compact group tower.

Compared with Route95's provider, this closure has no occurrences of minimalBlock_kernelLeastOverChiefData, minimalBlock_kernelFrattiniCollapseFullData, minimalBlock_kernelRawQuotientTowerData, or minimalBlock_headInvariantSemanticRoute12Data.

Fully lowered field-split provider

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

Route98 field-split group tower.

This route removes the four Route98 semantic packet names by expanding them through the existing Route40 field-level least, Frattini, raw quotient/action, bridge/head, and invariant packets.

Public providers

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

Drop-in kernel provider replacing minimalBlock_groupTowerData_from_kernelRoute95Closers.

This is the smaller-count Route98 closer; see minimalBlock_groupTowerData_from_kernelRoute98Closers_fieldSplit for the field-level lowering of all four Route98 semantic packet names.

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

Audit provider lowering all four Route98 semantic packet names to existing field-level residuals.