Route27 minimal-block kernel/head refinement

Route26 keeps the lower K, Phi(K), R, M, T, C construction split into the current concrete Section 7 leaves, but it still obtains the route12 head/invariant packet from the four route21 raw-head leaves.

This sidecar keeps the same route26 packet shape and lower tower. It replaces those four route21 head leaves by the existing same-raw-tower actual invariant packet minimalBlock_invariantActualProofs2Data, then projects that packet to the route12 semantic head data. The selected raw tower is unchanged.

Head/invariant data from the same-tower actual packet

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute27.headInvariantOfActual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockInvariantActualProofs2Data D) : MinimalBlockHeadInvariantSemanticRoute12Data D

Route27 projects the coherent actual simple-head/lower-character packet to the route12 semantic head/invariant interface used by route26.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute27.headActionNotPointwiseTrivialOfActual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockInvariantActualProofs2Data D) : MinimalBlockRawHeadActionNotPointwiseTrivialData D

Not-pointwise-trivial head action projected from the same actual packet.

This supplies the head-nonzero field needed by the route25 raw quotient helper without calling the route21 not-pointwise residual.

Equations

• ⋯ = ⋯

Route27 packet and projections

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

Route27 coherent Section 7 kernel/head packet.

The fields intentionally match route26: the lower concrete tower is unchanged, and the head/invariant component is stored in the same route12 semantic form.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattiniFull : MinimalBlockKernelFrattiniCollapseFullData self.least
• rawQuotient : MinimalBlockKernelRawQuotientTowerData self.least ⋯
• headInvariant : MinimalBlockHeadInvariantSemanticRoute12Data self.rawQuotient.rawData.rawTowerData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute27Data.frattiniData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute27Data chief) : MinimalBlockKernelModuleConcreteFrattiniData P.least

The concrete Frattini packet carried by Route27.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute27Data.rawData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute27Data chief) : MinimalBlockKernelModuleConcreteRawData P.least ⋯

The coherent raw data carried by Route27.

Equations

• P.rawData = P.rawQuotient.rawData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute27Data.actualProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute27Data chief) : MinimalBlockKernelModuleActualProofs chief

The actual lower kernel/module packet selected by Route27.

Equations

• P.actualProofs = Q2Presentation.Induction.MinimalBlockKernelConcreteRoute24.actualProofsOfRawQuotient P.least ⋯ P.rawQuotient

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute27Data.lowerGroupModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute27Data chief) : MinimalBlockLowerGroupModuleData chief

Lower group/module data selected by Route27.

Equations

• P.lowerGroupModuleData = P.actualProofs.lowerGroupModuleData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute27Data.route20Data {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute27Data chief) : MinimalBlockKernelConcreteRoute20Data chief

Route20-compatible same-tower packet recovered from Route27.

Equations

• P.route20Data = { lower := P.lowerGroupModuleData, headInvariant := ⋯ }

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute27Data.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelConcreteRoute27Data chief) : MinimalBlockGroupTowerData p chief

Route27 group-tower data.

Equations

• P.groupTowerData = P.route20Data.groupTowerData

Route27 assembly theorems

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute27Data_from_actualHeadPacket {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute27Data chief)

Route27 packet from the route26 lower tower and a coherent actual simple-head/lower-character packet on the same raw tower.

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

Route27 replacement for the current minimal-block group-tower provider.