Route103 kernel closers #

This sidecar leaves IntegratedCurrentRouteProofs103 untouched. It provides a drop-in kernel provider replacing minimalBlock_groupTowerData_from_kernelRoute98Closers.

The compact Route98 provider exposes two broad Section 7 residuals:

minimalBlock_lowerGroupModuleData;
MinimalBlockKernelConcreteRoute44.rawSimpleHeadSemanticData.

Route103 lowers that compact pair through the existing Route45 concrete route. The lower tower is rebuilt from the manuscript-shaped least-over-chief, Frattini-collapse, raw quotient/action, bridge, and head packets. The same-tower simple-head aggregate is rebuilt from quotient-head no-trivial-dual, quotient-head simplicity, and lower scalar quotient packets.

Lower tower split #

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute103Closers.lowerGroupModuleData_from_route103ManuscriptSplit {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockLowerGroupModuleData chief)

Route103 lower group/module data with the broad minimalBlock_lowerGroupModuleData residual removed.

The selected tower is the manuscript Section 7 tower K, R = Phi(K), M = K/R, T, and C, extracted from Route45's concrete provenance packet.

Same-tower simple-head split #

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute103Closers.rawSimpleHeadSemanticData_from_route103Lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) :

Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData lower.rawTowerData)

Route103 same-tower simple-head semantic packet with the Route44 rawSimpleHeadSemanticData aggregate removed.

This keeps the consumer shape used by Route98 while lowering the residual to the Route45 same-tower simple-head packets.

source

def Q2Presentation.Induction.MinimalBlockKernelRoute103Closers.dualInvariantVanishesData_of_rawSimpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D) :

MinimalBlockDualInvariantVanishesData D

Convert the lowered simple-head semantic packet into direct dual-invariant vanishing, without calling the Route44 aggregate axiom.

Equations

⋯ = ⋯

Instances For

source

def Q2Presentation.Induction.MinimalBlockKernelRoute103Closers.rawInvariantCharacterData_of_rawSimpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D) :

MinimalBlockRawInvariantCharacterData D

Convert the lowered simple-head semantic packet into the raw invariant character packet, without calling the Route44 aggregate axiom.

Equations

⋯ = ⋯

Instances For

Route103 drop-in kernel provider #

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute103Closers.groupTowerData_from_route103ManuscriptSplit {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupTowerData p chief)

Route103 kernel group-tower provider.

This is a drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute98Closers; its closure avoids the two compact Route98 kernel leaves and exposes the smaller manuscript Section 7 packets.