Route143 Section 7 Frattini actual closers

This sidecar leaves the current Route143 file untouched. It supplies a drop-in kernel provider for the Route143 integrated proof that bypasses the fifteen selected least/Frattini Route141 atoms and uses the concrete Section 7 packets instead:

• minimalBlock_kernelModuleConcreteLeastData, the selected least K <= P with K S = P;
• minimalBlock_kernelModuleConcreteFrattiniData, the actual R = Phi(K) collapse packet containing nontriviality, centrality in K, K^4 = 1, and exponent two on R.

The raw R,M,T,C tower remains routed through the Route141 raw sidecar, so the delta here is isolated to the least/Frattini portion of the kernel provider.

Least and Frattini providers

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

Route143 actual replacement for Section7KernelRoute141FrattiniClosers.leastOverChiefData_from_route141Frattini.

The selected least kernel is supplied by the concrete Section 7 packet, rather than by the Route141 selected least atom.

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

Route143 actual replacement for Section7KernelRoute141FrattiniClosers.frattiniData_from_route141Frattini.

This uses the concrete Frattini-collapse packet for the selected K directly, so the centralizer, fourth-power, and elementary Frattini proof-step atoms are not needed by this provider.

Route143 kernel provider with the actual Frattini source

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

Route143 kernel provenance with only the least/Frattini source swapped.

This is the local provider theorem that can replace the pair leastOverChiefData_from_route141Frattini / frattiniData_from_route141Frattini in an integrated route.

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

Lower group/module data through the Route143 actual Frattini provider.

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

Group-tower data through the Route143 actual Frattini provider and the existing Route141 raw/invariant sidecar.

Integrated Route143 variant with the Frattini actual provider

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

Route143 nonterminal Fourier branch with the selected least/Frattini source replaced by the concrete Section 7 actual packets.

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

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

Integrated finite-surjection equality variant exposing the exact axiom delta for replacing the Route141 selected least/Frattini atoms.