Route50 minimal-block kernel/module invariant provenance

This sidecar is route-neutral: it does not edit the routed capstone or any existing integrated route file.

Route49 still gets its Section 7 kernel provider from Route48, whose active kernel leaf is the broad packet

• minimalBlock_groupInvariantRouteData.

The current nonterminal branch only consumes the resulting MinimalBlockGroupTowerData. For that purpose, the needed Section 7 kernel data are:

• one concrete provenance tower for R = Phi(K) <= K, M = K/R, T, C, actions, bridge, and nonzero head;
• direct dual-invariant vanishing (M^vee)^C = 0 on that tower;
• one raw nonzero invariant character on the same Frattini layer.

The packet below deliberately does not store quotient-head simplicity or the stronger lower scalar quotient packet; those are not consumed by the Route49 kernel branch.

Consumed same-tower kernel/invariant data

structure Q2Presentation.Induction.MinimalBlockKernelRoute50.InvariantData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route50's consumed Section 7 kernel/invariant packet.

It fixes one concrete manuscript tower and carries only the two invariant facts needed to assemble the group tower consumed downstream.

• concrete : MinimalBlockKernelModuleConcreteProvenanceData chief
• dualInvariant : MinimalBlockDualInvariantVanishesData (minimalBlock_lowerFromConcreteProvenance self.concrete).rawTowerData
• rawInvariantCharacter : MinimalBlockRawInvariantCharacterData (minimalBlock_lowerFromConcreteProvenance self.concrete).rawTowerData

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

The coherent lower tower selected by the Route50 packet.

Equations

• D.lower = Q2Presentation.Induction.minimalBlock_lowerFromConcreteProvenance D.concrete

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

Forget Route50's consumed packet to the older route packet shape.

Equations

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

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

The group tower assembled from the Route50 consumed packet.

Equations

• D.groupTowerData = D.groupInvariantRouteData.groupTowerData

theorem Q2Presentation.Induction.MinimalBlockKernelRoute50.invariantData_from_splitClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (InvariantData chief)

Route50's consumed packet, assembled from existing split Section 7 closers.

Compared with minimalBlock_groupInvariantRouteData_proven, this avoids the quotient-head simplicity residual because the current group-tower route does not consume it.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute50.groupInvariantRouteData_from_route50 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route50 replacement for Route48's direct minimalBlock_groupInvariantRouteData call.

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

Route50 group-tower provider through the consumed same-tower data.

Public Route50 kernel provider

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

Drop-in kernel provider for a Route50 integration.

This has the same target as minimalBlock_groupTowerData_from_currentIntegrated48, but its kernel closure does not contain minimalBlock_groupInvariantRouteData.

Route49 skeleton with the Route50 kernel provider

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

Route49's nonterminal branch with only the Section 7 kernel provider swapped to Route50.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_kernelRoute50 (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 Route50 kernel provider.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_kernelRoute50 (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 Route50 kernel provider.

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

Boundary-framed count equality using the Route50 kernel provider.

theorem Q2Presentation.Induction.finite_surjection_counts_equal_kernelRoute50 (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 Route49 unchanged except for the Route50 Section 7 kernel/module invariant provider.