Route41 minimal-block kernel/head refinement #

This sidecar is standalone: no routed or root file imports it yet.

Route41 keeps Route40's concrete Section 7 kernel tower exactly as selected: least K, literal R = Phi(K), raw R,M,T,C, transported actions, quotient bridge, and nonzero head. It only refines the final head/invariant projection layer after the concrete tower is fixed.

Compared with minimalBlock_groupTowerData_from_kernelConcreteRoute40, the public Route41 provider removes these Route40 residual names from its axiom closure:

minimalBlock_rawHeadQuotientNoTrivialData;
minimalBlock_rawHeadSimplicityActualData;
minimalBlock_rawLowerScalarQuotientData.

They are replaced by existing finer, same-raw-tower packets:

direct dual-invariant vanishing, split as the two head-dual closers;
the nonzero-stable-submodule criterion for the quotient head;
the raw nonzero invariant determinant character on (R^vee)^C.

Manuscript anchors: reference/q2_manuscript.tex, Section 7, pp. 40--42: Lemma 7.1 "Simple head" for (M^vee)^C = 0 and quotient-head simplicity, and the beginning of the determinant-pushout paragraph for X_R = (R^vee)^B = (R^vee)^C.

No new axioms are declared in this file.

Route40 concrete tower, Route41 head/invariant split #

source

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute41.kernelModuleConcreteProvenanceData_from_route41 {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Route41 keeps the concrete kernel/module provenance from Route40.

This checkpoint isolates the unchanged kernel part: its closure is the Route40 kernel/module frontier, before the final head/invariant residuals are attached.

source

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute41.provenanceConcreteFinalPieces_from_route41 {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

Concrete-final provenance through Route40's fixed kernel tower and the finer Route41 head/invariant packets.

The selected lower tower is minimalBlock_lowerFromConcreteProvenance concrete, so the dual-invariant, head-simplicity, and raw-character inputs are all tied to the same K/R tower selected by Route40.

source