Route15 kernel/head sidecar for Section 7

This file is route-neutral: it does not edit IntegratedCurrentRouteProofs14 or PresentationCorrect. It targets the minimal-block kernel/head residual cluster exposed by route14.

The improvement over route14 is small but genuine. Route14 gets head_nontrivial from the standalone residual minimalBlock_headNontrivialData. Here it is derived from the route12 same-raw-tower semantic packet: if the quotient head M/T were subsingleton, then every endomorphism of it would be pointwise trivial, contradicting the not_pointwise_trivial field.

The remaining kernel/module facts are still the concrete manuscript-shaped obligations for the fixed Section 7 tower: least K, the five Frattini-collapse conclusions for R = Phi(K), raw objects/actions, and the literal K/R ~= M bridge.

Head nontriviality from the same raw-tower semantic packet

theorem Q2Presentation.Induction.minimalBlock_headNontrivialData_from_kernelHeadRoute15 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockHeadNontrivialData D)

The route12 same-raw-tower head/invariant semantic packet implies that the quotient head is nontrivial.

This closes the standalone minimalBlock_headNontrivialData residual whenever the route is already using minimalBlock_headInvariantSemanticRoute12Data for the same raw tower.

Kernel/module assembly with delayed head input

theorem Q2Presentation.Induction.minimalBlock_kernelModuleActualProofs_from_kernelHeadRoute15 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleActualProofs chief)

Actual kernel/module packet rebuilt from route14's concrete Section 7 kernel data, but with head nontriviality derived from the head/invariant semantic packet instead of the standalone minimalBlock_headNontrivialData axiom.

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

Lower group/module data through the route15 kernel/head refinement.

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

Route15 replacement for the route14 group-tower provider.

Compared with minimalBlock_groupTowerData_from_currentIntegrated14, this provider no longer depends on minimalBlock_headNontrivialData. It still uses the route12 head/invariant semantic packet and the concrete kernel/Frattini/raw same-tower obligations listed in the acceptance output.