Route145 Section 7 kernel/raw actual closers

This sidecar leaves Route144 untouched. It supplies a replacement kernel provider chain for the Route144 Section 7 kernel route:

• the broad concrete least packet is lowered to the least-over-chief choice packet;
• the broad concrete Frattini packet is lowered to the five literal Frattini-collapse fields;
• the Route143 raw literal object/action aggregates are lowered to the Route43 literal R, M, T, C objects and transported-action pieces;
• the Route143 raw simple-head aggregate is lowered to the Route43 maximal-submodule, orbit-span, action-witness, and lower-character atoms.

The exported route theorems are drop-in replacements for the current Route144 kernel provider chain, but no integrated file is edited here.

Least and Frattini replacements

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

Route145 replacement for Section7KernelRoute143FrattiniActualClosers.leastOverChiefData_from_route143FrattiniActual.

The closure uses the narrower least-over-chief choice packet, not the broad minimalBlock_kernelModuleConcreteLeastData residual.

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

Route145 replacement for Section7KernelRoute143FrattiniActualClosers.frattiniData_from_route143FrattiniActual.

The closure uses the field-level Frattini-collapse packets from MinimalBlockKernelModuleConcreteClosers2, not the broad minimalBlock_kernelModuleConcreteFrattiniData residual.

Raw quotient tower replacement

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

Route145 replacement for Section7KernelRoute143RawActualClosers.minimalBlock_kernelRawQuotientTowerData_from_section7KernelRoute143RawActualClosers.

This reassembles the consumed raw quotient tower from the Route43 literal object/action atoms:

• literal R = Phi(K), M = K/Phi(K), T, and C = Y/K;
• transported actions on R and M;
• transported stability of T;
• a head-action witness, which implies the nontrivial head required by the raw quotient tower.

Raw simple-head and invariant replacement

theorem Q2Presentation.Induction.Section7KernelRoute145ActualClosers.rawSimpleHeadSemanticData_from_section7KernelRoute145ActualClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D)

Route145 same-tower raw simple-head semantic packet from Route43 atoms.

This is the Route44/Route112 consumer shape, but it is assembled from the manuscript-shaped Route43 pieces instead of the Route143 rawSimpleHeadActualData aggregate.

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

Route145 replacement for Section7KernelRoute143RawActualClosers.minimalBlock_invariantActualProofs2Data_from_section7KernelRoute143RawActualClosers_lower.

The old actual invariant packet is rebuilt from the Route145 raw simple-head semantic packet, avoiding the Route143 rawSimpleHeadActualData aggregate.

Route144-compatible kernel provider

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

Route145 kernel provenance provider for the Route144 branch.

This has the same target as minimalBlock_kernelModuleConcreteProvenanceData_currentIntegrated144, but the least/Frattini/raw/invariant provider chain is routed through the Route145 lowered atoms above.

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

Lower group/module data through the Route145 kernel provider.

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

Group tower through the Route145 lowered kernel/raw provider chain.

Route145 audit branch over the Route144 Section 8/pushout route

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

Route144 nonterminal Fourier branch with only the Section 7 kernel provider swapped to the Route145 lowered provider.

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

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

Finite-surjection equality for the Route144 branch with Route145 kernel/raw lowering.