Route138 Section 7 kernel closers

This sidecar leaves the public presentation route and the existing Route138 file untouched. It targets exactly the Route138 kernel/provenance frontier:

• minimalBlock_kernelLeastCandidateData;
• minimalBlock_kernelLeastUniversalData;
• minimalBlock_kernelFrattiniCollapseFullData;
• minimalBlock_kernelRawQuotientTowerData;
• the four Route43 raw simple-head packets.

The replacement keeps the manuscript Section 7 tower. The least kernel is the upper-chief candidate with selected universal leastness, the Frattini collapse is the Route81 split of R = Phi(K), and the raw quotient tower is assembled from literal Route43 R,M,T,C object/action packets through Route90. The head field is supplied from Route83's same-raw-tower actual invariant packet, so the new integrated theorem does not depend on the four Route43 raw-head leaves.

Kernel/provenance providers

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

The candidate half of the least-kernel step is theorem-level: use the upper chief-factor subgroup from the manuscript's first non-scalar layer.

theorem Q2Presentation.Induction.Section7KernelRoute138Closers.minimalBlock_kernelUpperSelectedLeastUniversalData_from_section7KernelRoute138Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute116Closers.UpperLeastKernelSelectedData chief)

Selected universal leastness for the upper-chief candidate.

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

Route-ready least-over-chief data for the selected K.

theorem Q2Presentation.Induction.Section7KernelRoute138Closers.minimalBlock_kernelFrattiniCollapseFullData_from_section7KernelRoute138Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelFrattiniCollapseFullData K)

Frattini-collapse packet for R = Phi(K), routed through the Route81 split of centralizer, fourth-power, and elementary-layer data.

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

Raw quotient tower for R, M = K/R, T, and C = Y/K.

The literal object/action/bridge data come from Route90. The required nontrivial head field is obtained from Route83's same-tower actual invariant packet, avoiding the four Route43 raw-head residuals in the Route138 closure.

theorem Q2Presentation.Induction.Section7KernelRoute138Closers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute138Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete provenance packet through the Route138 kernel-lowered tower.

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

Selected lower group/module tower through the Route138 kernel-lowered concrete provenance packet.

theorem Q2Presentation.Induction.Section7KernelRoute138Closers.minimalBlock_invariantActualProofs2Data_from_section7KernelRoute138Closers_lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockInvariantActualProofs2Data lower.rawTowerData)

Same-tower actual invariant packet that replaces the four Route43 raw-head leaves in the Route138 branch.

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

Route138 drop-in kernel group-tower provider with all listed Route138 kernel/provenance leaves removed from its closure.

Route139-style integrated theorem with the kernel provider swapped

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

Route138 nonterminal Fourier branch with only the Section 7 kernel provider swapped to the Route138 kernel-lowered sidecar above.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated139KernelLowered (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_currentIntegrated139KernelLowered (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_currentIntegrated139KernelLowered (p : FramedPair) : framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated139KernelLowered (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)))

Route139-style finite-surjection equality with the Route138 kernel leaves strictly lowered in this sidecar only.