Kernel-module semantic closers, third pass

This sidecar is route-neutral. It targets the current route3 Section 7 minimal-block/kernel-module residuals without editing PresentationCorrect.

The kernel-module part uses the already finer concrete route from MinimalBlockKernelModuleConcreteClosers2; this removes the theorem-level ActualLeast, ActualKmodRBridge, and ActualHeadNontrivial wrapper packets from the route closure. The invariant/simple-head part uses MinimalBlockInvariantActualProofs3, replacing the monolithic minimalBlock_invariantActualProofs2Data packet by the lower same-raw-tower simple-head and scalar-character facts.

Lower tower through the concrete kernel-module split

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

Lower group/module data for the Section 7 minimal block, routed through the finer concrete kernel-module split rather than the three route3 actual wrapper packets.

Same-tower invariant/simple-head split

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

Group-tower data through the concrete kernel-module split and the third-pass same-raw-tower invariant split.

The axiom closure of this theorem avoids minimalBlock_invariantActualProofs2Data, minimalBlock_kernelModuleActualLeastData, minimalBlock_kernelModuleActualKmodRBridgeData, and minimalBlock_kernelModuleActualHeadNontrivialData.

Current route3 branch with the kernel/invariant step swapped

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

Nonterminal Fourier branch matching route3, but with the Section 7 kernel-module and invariant pieces supplied by this sidecar.

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

theorem Q2Presentation.Induction.finite_surjection_counts_equal_kernelModuleSemanticClosers3 (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 with route3 candidate/target and extraspecial inputs unchanged, but with the Section 7 kernel/invariant closure refined by this file.