Route110 raw-head closer sidecar

This sidecar keeps Route110's existing least/Frattini/raw-quotient kernel tower and changes only the same-tower simple-head assembly. The Route106 kernel provider obtained that assembly through Route63, whose closure exposes the four Route43 raw-head leaves. Here the same consumer packet is projected from the coherent same-raw-tower actual packet via Route83's rawSimpleHeadSemanticData_from_route83.

No integrated route file imports this module yet.

Route106 tower with Route83 same-tower head projection

theorem Q2Presentation.Induction.MinimalBlockKernelRoute110RawHeadClosers.lowerGroupModuleData_from_route110RawHeadClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Route110 raw-head closer keeps the Route106 least/Frattini/raw quotient tower unchanged.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute110RawHeadClosers.rawSimpleHeadSemanticData_from_route110RawHeadClosersLower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData lower.rawTowerData)

Same-tower simple-head semantic packet with the four Route43 raw-head leaves lowered to the coherent actual packet used by Route83.

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

Route-ready kernel group-tower provider matching minimalBlock_groupTowerData_from_kernelRoute106HeadClosers.

Compared with the Route106 provider, this avoids the four Route43 raw-head leaves by using Route83's same-raw-tower actual projection for the simple-head packet only.

Public route-ready aliases

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

Public lower-tower alias for the Route110 raw-head closer.

theorem Q2Presentation.Induction.minimalBlock_rawSimpleHeadSemanticData_from_kernelRoute110RawHeadClosers_lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData lower.rawTowerData)

Public selected-tower simple-head alias for the Route110 raw-head closer.

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

Public drop-in kernel provider matching the Route106 head-closer provider surface.

Route110 branch audit theorem

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_currentIntegrated110_rawHeadClosers (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

Route110 nonterminal branch with only the kernel provider swapped to the raw-head closer above. This theorem is for sidecar audit; integrated route files are unchanged.