Route110 kernel-core closers

This sidecar is isolated from the integrated route files. It provides a Route110-compatible kernel provider whose closure avoids the four broad kernel core atoms still visible in Route110:

• minimalBlock_kernelFrattiniCollapseFullData;
• minimalBlock_kernelLeastCandidateData;
• minimalBlock_kernelLeastUniversalData;
• minimalBlock_kernelRawQuotientTowerData.

The replacement keeps the same Section 7 tower shape from the manuscript: choose the least K, set R = Phi(K), form the raw K/R, T, and C tower, and then use the same-tower simple-head data.

Least-kernel surface

theorem Q2Presentation.Induction.MinimalBlockKernelRoute110CoreClosers.leastCandidateData_from_route110CoreClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

The candidate half of the least-kernel split is theorem-level: the upper chief-factor subgroup itself is always a candidate.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute110CoreClosers.selectedLeastUniversalData_from_route110CoreClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (K : MinimalBlockKernelCandidateData chief), Nonempty (MinimalBlockKernelLeastUniversalData K)

Selected universal leastness for the actual Route110 core kernel.

This is the route-ready replacement for the old arbitrary-candidate minimalBlock_kernelLeastUniversalData call: the universal property is attached to the selected least kernel used downstream.

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

Least-over-chief packet for the selected Route110 core tower.

Frattini-collapse surface

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

Replacement for minimalBlock_kernelFrattiniCollapseFullData, assembled from the lower Route90 proof-step packets for the same selected K.

Raw quotient tower surface

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

Replacement for minimalBlock_kernelRawQuotientTowerData, assembled from the Route90 literal object/action bridge and the same-tower simple-head packet.

Route-ready kernel provider

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

Concrete provenance through the Route110 core-lowered tower.

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

Lower group/module data through the Route110 core-lowered tower.

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

Route110-compatible kernel group-tower provider with the core cluster lowered.

Public aliases and Route110 audit variant

theorem Q2Presentation.Induction.minimalBlock_kernelLeastCandidateData_from_route110CoreClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

Public candidate-half closer for the Route110 core cluster.

theorem Q2Presentation.Induction.minimalBlock_kernelSelectedLeastUniversalData_from_route110CoreClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (K : MinimalBlockKernelCandidateData chief), Nonempty (MinimalBlockKernelLeastUniversalData K)

Public selected universal-leastness closer for the Route110 core cluster.

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

Public least-over-chief provider for downstream routes.

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

Public Frattini-collapse closer for the Route110 core cluster.

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

Public raw quotient tower closer for the Route110 core cluster.

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

Public concrete-provenance provider for the Route110 core-lowered tower.

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

Public lower-tower provider for the Route110 core-lowered tower.

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

Public Route110-compatible kernel provider.

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

Route110 boundary theorem with only the kernel provider swapped to the core-lowered provider in this sidecar.

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

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