Actual kernel-module closers for the current Section 7 route

This sidecar keeps the routed files untouched. It supplies route-ready wrappers for the current residual

minimalBlock_kernelModuleActualProofs : Nonempty (MinimalBlockKernelModuleActualProofs chief)

without using that aggregate axiom. The replacement route goes through the smaller manuscript-shaped packets already exposed by MinimalBlockKernelModuleConcreteClosers2:

• least K over the chosen chief factor;
• literal R = Phi(K) normal/nontrivial/central/fourth-power/exponent facts;
• raw R, M, T, C objects and induced actions;
• the literal K/R ~= M bridge;
• nontriviality of the head M/T.

The final theorem in this file mirrors the current integrated finite-surjection route, with the kernel-module aggregate residual replaced by those smaller packets.

Aggregate actual packet from smaller packets

structure Q2Presentation.Induction.MinimalBlockKernelModuleActualLeastData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type

Actual least-K packet for the kernel-module route.

This intentionally wraps the existing least-over-chief data type while exposing a current kernel-module packet name in theorem closures.

• least : MinimalBlockKernelLeastOverChiefData chief

structure Q2Presentation.Induction.MinimalBlockKernelModuleActualKmodRBridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Type

Actual K/Phi(K) ~= M bridge packet for the selected concrete tower.

• bridge : MinimalBlockKernelModuleConcreteBridgeData D

structure Q2Presentation.Induction.MinimalBlockKernelModuleActualHeadNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Prop

Actual nontrivial-head packet for the selected concrete tower.

• head : MinimalBlockKernelModuleConcreteHeadData D

axiom Q2Presentation.Induction.minimalBlock_kernelModuleActualLeastData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleActualLeastData chief)

Residual: choose the least K for the actual kernel-module route.

axiom Q2Presentation.Induction.minimalBlock_kernelModuleActualKmodRBridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Nonempty (MinimalBlockKernelModuleActualKmodRBridgeData D)

Residual: prove the actual bridge K/Phi(K) ~= M for the selected tower.

axiom Q2Presentation.Induction.minimalBlock_kernelModuleActualHeadNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Nonempty (MinimalBlockKernelModuleActualHeadNontrivialData D)

Residual: prove that the selected simple head M/T is nontrivial.

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

Assemble the aggregate actual packet from only current actual/concrete kernel-module packets.

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

Route-ready wrapper back to the current aggregate actual packet, but with axiom closure coming from the smaller Section 7 packets rather than from minimalBlock_kernelModuleActualProofs.

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

Concrete provenance for the same selected K/R tower, built from the smaller actual closers and avoiding the provenance wrapper that still calls minimalBlock_kernelModuleActualProofs.

Downstream provenance wrappers

theorem Q2Presentation.Induction.minimalBlock_provenanceConcreteFinalPieces_from_kernelModuleActualClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

Concrete-final provenance pieces using the smaller kernel-module actual closers and the current simple-head/scalar split.

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

Group-tower data through the smaller kernel-module actual closers and the current simple-head/scalar split.

Current integrated route with the kernel-module aggregate replaced

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

Nonterminal Fourier branch matching the current integrated route, except the Section 7 kernel-module provenance is supplied by the smaller actual closers above.

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

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

Current strongest finite-surjection equality route with the kernel-module aggregate actual residual replaced by the smaller Section 7 packets.