Route10 kernel/Frattini refinements for Section 7

This sidecar is route-neutral: it does not edit the integrated route files. It targets the route10 P3 kernel/Frattini/raw residual cluster by replacing the independent concrete packet names with the coherent manuscript tower from Section 7:

• the least normal K <= P over the selected non-scalar chief factor;
• the Frattini-centralizer collapse for the literal R = Phi(K);
• the raw quotient tower R, M = K/R, T, C, transported actions, the K/R ~= M bridge, and the nonzero head.

The theorem-level candidate packet is proved directly from chief.upper. The leastness, collapse, and raw quotient tower remain explicit finite group/module inputs; this file keeps them coherent instead of using route10's arbitrary independent choices for each downstream field.

Direct route10 packet replacements

theorem Q2Presentation.Induction.minimalBlock_kernelLeastCandidateData_from_route10KernelFrattiniProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

The non-minimal candidate part of the route10 least-kernel split is theorem-level: the chief-factor upper subgroup itself is a valid candidate.

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

Route10 replacement for the split least-kernel construction. The coherent least-over-chief packet keeps the candidate and its universal property attached to the same selected K.

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteFrattiniNonidentityData.ofNontrivial {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : MinimalBlockKernelModuleConcreteFrattiniNontrivialData K) : MinimalBlockKernelModuleConcreteFrattiniNonidentityData K

Convert cardinal nontriviality of the literal Frattini subgroup into the route10 nonidentity-witness shape.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteFrattiniNonidentityData_from_route10KernelFrattiniProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniNonidentityData K)

Route10 replacement for Frattini nonidentity, projected from the coherent Frattini-collapse package.

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

Route10 replacement for Frattini centrality, projected from the coherent Frattini-collapse package.

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

Route10 replacement for K^4 = 1, projected from the coherent Frattini-collapse package.

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

Route10 replacement for exponent two on Phi(K), projected from the coherent Frattini-collapse package.

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

Route10 replacement for the full concrete Frattini packet. Its closure uses the single coherent collapse package rather than the independent route10 central/fourth/exponent/nonidentity residuals.

theorem Q2Presentation.Induction.minimalBlock_kernelRawQuotientTowerData_from_route10KernelFrattiniProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Route10 replacement for the raw quotient tower. This keeps the raw objects, subquotients, transported actions, K/R ~= M bridge, and head nonzero proof attached to the same selected tower.

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteRawData_from_route10KernelFrattiniProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelModuleConcreteRawData K F)

Route10 replacement for the concrete raw-data packet through the coherent raw quotient tower.

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteKmodRQuotientEquivData_from_route10KernelFrattiniProofs {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Nonempty (MinimalBlockKernelModuleConcreteBridgeData D)

Route10 replacement for the K/Phi(K) ~= M quotient equivalence. This uses the lower same-tower K/R bridge instead of the route10 concrete bridge axiom.

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteHeadNonzeroData.ofHeadData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {D : MinimalBlockKernelModuleConcreteRawData K F} (H : MinimalBlockKernelModuleConcreteHeadData D) : MinimalBlockKernelModuleConcreteHeadNonzeroData D

Convert the existing nontrivial-head packet into route10's explicit nonzero-coset witness.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteHeadNonzeroData_from_route10KernelFrattiniProofs {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Nonempty (MinimalBlockKernelModuleConcreteHeadNonzeroData D)

Route10 replacement for the head-nonzero witness, projected from the same-tower nontrivial-head packet.

Route-level assembly with the P3 cluster swapped out

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

Actual kernel/module packet with route10's independent P3 concrete residuals replaced by the coherent least/collapse/raw tower packets.

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

Lower group/module data through the route10 P3 replacement.

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

Group tower through the route10 P3 replacement. This is the drop-in sidecar for future route integration.

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

Route10 nonterminal branch with the P3 kernel/Frattini cluster supplied by this sidecar.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated10_route10KernelFrattiniProofs (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_currentIntegrated10_route10KernelFrattiniProofs (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_currentIntegrated10_route10KernelFrattiniProofs (p : FramedPair) : framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated10_route10KernelFrattiniProofs (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Route-ready finite-surjection equality for route10 with the P3 kernel/Frattini concrete cluster removed from this theorem's axiom closure.