Coherent route13 kernel/Frattini refinements for Section 7

This sidecar is route-neutral: it does not edit the integrated route files. It targets the three coarse route13 kernel/Frattini residuals

• minimalBlock_kernelLeastOverChiefData;
• minimalBlock_kernelFrattiniCollapseFullData;
• minimalBlock_kernelRawQuotientTowerData.

The bridge theorems below keep the same public target shapes, but prove them from finer manuscript-shaped obligations: the concrete least-kernel packet, the split Frattini-collapse conclusions, raw quotient objects/actions, and the same-tower quotient-bridge/head packets. The exported group-tower and finite surjection providers are compatible with IntegratedCurrentRouteProofs13, but their axiom closure no longer contains the three coarse route13 names above.

Coarse route13 residuals from finer Section 7 packets

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

Route13 least-kernel target, supplied by the concrete least-kernel packet rather than by the coarse minimalBlock_kernelLeastOverChiefData axiom.

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

Route13 Frattini-collapse target, assembled from the split Frattini-normal/nontrivial/central/fourth-power/exponent packets.

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

Concrete Frattini packet through the route13 coherent bridge.

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

Route13 raw quotient tower target, assembled from raw quotient objects/actions plus the same-tower quotient bridge and nonzero head.

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteRawData_from_coherentRoute13Proofs {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelModuleConcreteRawData K F)

Concrete raw-data packet through the route13 coherent raw quotient bridge.

Route-ready lower and group-tower providers

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

Actual kernel/module packet with the three route13 coarse residual names removed from the theorem closure and replaced by the finer Section 7 packets above.

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

Lower group/module data through the coherent route13 refinement.

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

Route13-compatible group tower provider using the coherent kernel/Frattini refinement and the existing route10 head/invariant sidecar.

Route13 branch and finite-surjection provider using the new tower

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

Route13 nonterminal branch with the kernel/Frattini provider replaced by minimalBlock_groupTowerData_from_coherentRoute13Proofs.

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

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

Route13 finite-surjection equality with the three coherent kernel/Frattini residuals removed/refined by this sidecar.