Route53 minimal-block kernel/module refinement

This sidecar keeps Route52 and the presentation files untouched. It replaces the two Route52 Section 7 kernel leaves

• minimalBlock_kernelModuleActualProofs;
• minimalBlock_invariantActualProofs2Data;

by the smaller manuscript-shaped packets already exposed in the theorem-level closers:

• the least K, Frattini-collapse, raw R,M,T,C objects/actions, K/R ≃ M bridge, and nonzero head packets from MinimalBlockKernelModuleConcreteClosers2;
• the third-pass invariant split into quotient-head no-triviality, quotient-head simplicity, and lower scalar character packets from MinimalBlockInvariantActualProofs3.

The exported minimalBlock_groupTowerData_from_kernelRoute53 has the same target as the Route52 provider, so it can be used as a drop-in kernel sidecar in a later integrated route.

Narrowed replacements for the two Route52 kernel leaves

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

Route53 replacement for minimalBlock_kernelModuleActualProofs.

The aggregate actual-kernel packet is assembled from the smaller concrete Section 7 packets: least K, literal R = Phi(K), raw R,M,T,C objects/actions, the quotient bridge, and nonzero head.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute53.invariantActualProofs2Data_from_route53 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockInvariantActualProofs2Data D.rawTowerData)

Route53 replacement for minimalBlock_invariantActualProofs2Data on a selected lower tower.

This uses the third-pass invariant split, so the monolithic same-tower invariant packet is narrowed to quotient-head no-triviality, quotient-head simplicity, and the lower scalar character on the same raw tower.

Same-tower full actual packet

structure Q2Presentation.Induction.MinimalBlockKernelRoute53.ActualInvariantData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Coherent Route53 kernel/invariant packet.

The invariant packet is attached to the raw tower selected by the same actual kernel-module construction, preventing any mix of unrelated K/R towers.

• kernel : MinimalBlockKernelModuleActualProofs chief
• invariant : MinimalBlockInvariantActualProofs2Data self.kernel.lowerGroupModuleData.rawTowerData

def Q2Presentation.Induction.MinimalBlockKernelRoute53.ActualInvariantData.lower {p : FramedPair} {chief : NonScalarChiefFactor p} (D : ActualInvariantData chief) : MinimalBlockLowerGroupModuleData chief

The coherent lower tower selected by the Route53 packet.

Equations

• D.lower = D.kernel.lowerGroupModuleData

def Q2Presentation.Induction.MinimalBlockKernelRoute53.ActualInvariantData.groupInvariantRouteData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : ActualInvariantData chief) : MinimalBlockGroupInvariantRouteData chief

Forget Route53's consumed packet to the route packet shape used downstream.

Equations

• D.groupInvariantRouteData = { lower := D.lower, dualInvariant := ⋯, rawInvariantCharacter := ⋯ }

def Q2Presentation.Induction.MinimalBlockKernelRoute53.ActualInvariantData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : ActualInvariantData chief) : MinimalBlockGroupTowerData p chief

The group tower assembled from the Route53 consumed packet.

Equations

• D.groupTowerData = D.groupInvariantRouteData.groupTowerData

theorem Q2Presentation.Induction.MinimalBlockKernelRoute53.actualInvariantData_from_route53 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (ActualInvariantData chief)

Route53's consumed same-tower packet assembled from the narrowed kernel and invariant closers.

Same-tower consumed packet for the Route53 provider

structure Q2Presentation.Induction.MinimalBlockKernelRoute53.ConsumedData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

The narrower data actually consumed by the group-tower route.

The full MinimalBlockInvariantActualProofs2Data theorem above is retained as a closure comparison for the Route52 leaf. The provider itself only needs dual-invariant vanishing and a raw invariant character on the same selected raw tower, so it uses those theorem-level closers directly.

• kernel : MinimalBlockKernelModuleActualProofs chief
• dualInvariant : MinimalBlockDualInvariantVanishesData self.kernel.lowerGroupModuleData.rawTowerData
• rawInvariantCharacter : MinimalBlockRawInvariantCharacterData self.kernel.lowerGroupModuleData.rawTowerData

def Q2Presentation.Induction.MinimalBlockKernelRoute53.ConsumedData.lower {p : FramedPair} {chief : NonScalarChiefFactor p} (D : ConsumedData chief) : MinimalBlockLowerGroupModuleData chief

The coherent lower tower selected by the Route53 provider.

Equations

• D.lower = D.kernel.lowerGroupModuleData

def Q2Presentation.Induction.MinimalBlockKernelRoute53.ConsumedData.groupInvariantRouteData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : ConsumedData chief) : MinimalBlockGroupInvariantRouteData chief

Forget the consumed Route53 packet to the route packet shape used downstream.

Equations

• D.groupInvariantRouteData = { lower := D.lower, dualInvariant := ⋯, rawInvariantCharacter := ⋯ }

def Q2Presentation.Induction.MinimalBlockKernelRoute53.ConsumedData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : ConsumedData chief) : MinimalBlockGroupTowerData p chief

The group tower assembled from the consumed Route53 packet.

Equations

• D.groupTowerData = D.groupInvariantRouteData.groupTowerData

theorem Q2Presentation.Induction.MinimalBlockKernelRoute53.consumedData_from_route53 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (ConsumedData chief)

Route53's consumed same-tower packet, with the invariant side narrowed to the two facts needed by MinimalBlockGroupTowerData.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute53.groupInvariantRouteData_from_route53 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant packet with both Route52 kernel leaves replaced by smaller manuscript-shaped residuals.

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

Route53 group-tower provider replacing minimalBlock_groupTowerData_from_kernelRoute52.

Public Route53 kernel provider

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

Drop-in kernel provider for a Route53 integration.

It has the same target as minimalBlock_groupTowerData_from_kernelRoute52, but its axiom closure no longer contains minimalBlock_kernelModuleActualProofs or minimalBlock_invariantActualProofs2Data.

Route52 skeleton with the Route53 kernel provider

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

Route52's nonterminal branch with only the Section 7 kernel provider swapped to Route53.

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

Recursive branch using the Route53 kernel provider.

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

Recursion step using the Route53 kernel provider.

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_kernelRoute53 (p : FramedPair) : framedCountA p = framedCountQ p

Boundary-framed count equality using the Route53 kernel provider.

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

Equal finite surjection counts with Route52 unchanged except for the Route53 Section 7 kernel/module provider.