Route146 Section 7 least/Frattini closers

This sidecar leaves the Route145 integrated file untouched. It supplies drop-in replacements for the Route145 least/Frattini entry points while keeping the Route145 raw/head provider chain fixed.

The Route145 least/Frattini frontier

• minimalBlock_kernelLeastOverChiefData;
• minimalBlock_kernelModuleConcreteFrattiniNormalData;
• minimalBlock_kernelModuleConcreteFrattiniNontrivialData;
• minimalBlock_kernelModuleConcreteFrattiniCentralData;
• minimalBlock_kernelModuleConcreteFourthPowerData;
• minimalBlock_kernelModuleConcreteFrattiniExponentData;

is replaced by the stricter selected chief-series/Frattini atoms from the lower Route78 ladder. Normality of the literal embedded Phi(K) remains theorem-level.

Selected least-kernel replacement

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.leastKernelSelectedData_from_route146Frattini {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.LeastKernelSelectedData chief)

Route146 selected least-kernel packet.

This is the lower, dependent replacement for the Route145 leaf minimalBlock_kernelLeastOverChiefData: the chosen candidate and its universal leastness proof are attached to the same selected object.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.leastOverChiefData_from_route146Frattini {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route146 replacement for Section7KernelRoute145ActualClosers.leastOverChiefData_from_route145Actual.

Selected Frattini-collapse replacements

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.frattiniInternalSelectedData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniInternalSelectedData K)

Route146 selected internal nonidentity witness in the literal Frattini subgroup.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.frattiniInternalNonidentityData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniInternalNonidentityData K)

Route67-shaped internal nonidentity packet recovered from the selected Route146 witness.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.frattiniNontrivialData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniNontrivialData K)

Route146 nontriviality of the literal Frattini subgroup from the selected internal witness.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.frattiniCentralizerSelectedData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniCentralizerSelectedData K)

Route146 selected centralizer core plus Hall-image packet for the Frattini-centralizer collapse.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.frattiniCentralizerHallCommutatorData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniCentralizerHallCommutatorData K)

Route67-shaped centralizer Hall-commutator packet recovered from the selected Route146 data.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.frattiniCentralizerStepData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K)

Route146 centralizer proof-step packet, obtained by applying leastness to the selected centralizer candidate.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.frattiniCentralData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniCentralData K)

Route146 replacement for the Route145 Frattini-centrality leaf.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.fourthPowerKernelSelectedData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FourthPowerKernelSelectedData K)

Route146 selected fourth-power kernel plus Hall-image packet.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.fourthPowerKernelCommutatorData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FourthPowerKernelCommutatorData K)

Route67-shaped fourth-power kernel/commutator packet recovered from the selected Route146 data.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.fourthPowerMapVanishesData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K)

Route146 fourth-power proof-step packet, obtained by applying leastness to the selected kernel of the fourth-power map.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.fourthPowerData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFourthPowerData K)

Route146 replacement for the Route145 fourth-power leaf.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.frattiniSquareCommutatorLiteralExponentData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniSquareCommutatorLiteralExponentData K)

Route146 literal exponent-two packet for the embedded Phi(K) layer after the centralizer and fourth-power collapse steps.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.frattiniElementaryLayerData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FrattiniElementaryLayerData K)

Route146 elementary Frattini-layer proof-step packet.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.frattiniExponentData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniExponentData K)

Route146 replacement for the Route145 Frattini exponent-two leaf.

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.frattiniData_from_route146Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Route146 replacement for Section7KernelRoute145ActualClosers.frattiniData_from_route145Actual.

Normality of the literal embedded Phi(K) is theorem-level; the other four Frattini-collapse fields are supplied through selected Route146 atoms.

Route145-compatible kernel provider with Route146 least/Frattini

theorem Q2Presentation.Induction.Section7KernelRoute146FrattiniClosers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute146FrattiniClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete kernel provenance with the Route145 raw/head path left unchanged and the least/Frattini source swapped to Route146.

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

Lower group/module data through the Route146 least/Frattini provider.

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

Group tower through the Route146 least/Frattini provider and the Route145 raw/head/invariant chain.

Acceptance checks