Route52 minimal-block kernel/module provenance

This sidecar keeps Route51 intact and swaps only the Section 7 kernel provider.

Route51 exposes four kernel/raw leaves:

• minimalBlock_kernelModuleConcreteProvenanceData;
• minimalBlock_rawHeadDualInvariantZeroData;
• minimalBlock_rawInvariantFunctionalsKillTData;
• minimalBlock_rawLowerScalarQuotientData.

Route52 narrows them to two same-tower manuscript packets:

• minimalBlock_kernelModuleActualProofs, carrying the actual K, R = Phi(K), raw module/action data, bridge, and nontrivial head;
• minimalBlock_invariantActualProofs2Data, carrying the simple-head/no-trivial and lower invariant-character facts on the selected raw tower.

Auditable replacements for the four Route51 kernel/raw leaves

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

Route52 replacement for minimalBlock_kernelModuleConcreteProvenanceData.

The closure uses the coherent actual kernel/module construction packet rather than the Route51 provenance axiom.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute52.rawInvariantFunctionalsKillTData_from_route52 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantFunctionalsKillTData D)

Route52 replacement for minimalBlock_rawInvariantFunctionalsKillTData.

This is the manuscript statement that invariant functionals on M kill T, derived from the actual simple-head packet on the same raw tower.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute52.rawHeadDualInvariantZeroData_from_route52 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadDualInvariantZeroData D)

Route52 replacement for minimalBlock_rawHeadDualInvariantZeroData.

This is the no-trivial-dual quotient-head statement derived from irreducibility and nontriviality of the actual simple head.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute52.rawLowerScalarQuotientData_from_route52 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerScalarQuotientData D)

Route52 replacement for minimalBlock_rawLowerScalarQuotientData.

The scalar quotient is rebuilt from the actual invariant character over ZMod 2; surjectivity is Lean-level finite-field bookkeeping.

Consumed Route52 same-tower kernel/invariant data

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

Route52's consumed Section 7 packet.

It fixes one concrete manuscript tower and attaches the invariant facts to the raw tower extracted from that same provenance.

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

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

The coherent lower tower selected by the Route52 packet.

Equations

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

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

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

Equations

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

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

The group tower assembled from the Route52 consumed packet.

Equations

• D.groupTowerData = D.groupInvariantRouteData.groupTowerData

theorem Q2Presentation.Induction.MinimalBlockKernelRoute52.invariantData_from_actualKernel_simpleHead {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (InvariantData chief)

Route52's consumed packet, assembled from theorem-level Section 7 closers.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute52.groupInvariantRouteData_from_route52 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route52 group/invariant packet with the four Route51 kernel/raw leaves replaced by two coherent actual packets.

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

Route52 group-tower provider replacing MinimalBlockKernelRoute50.groupTowerData_from_route50.

Public Route52 kernel provider

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

Drop-in kernel provider for a Route52 integration.

It has the same target as minimalBlock_groupTowerData_from_kernelRoute50, but its closure no longer contains the four Route51 kernel/raw leaves.

Route51 skeleton with the Route52 kernel provider

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

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

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_kernelRoute52 (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 Route52 kernel provider.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_kernelRoute52 (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 Route52 kernel provider.

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

Boundary-framed count equality using the Route52 kernel provider.

theorem Q2Presentation.Induction.finite_surjection_counts_equal_kernelRoute52 (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 Route51 unchanged except for the Route52 Section 7 kernel/module provenance provider.