Route130 kernel closers #

This sidecar leaves the promoted Route130 files untouched. It attacks the current kernel leaf

minimalBlock_provenanceSemanticData.

The Route130 replacement below proves the same provenance-semantic packet from the stricter concrete-final provenance route:

concrete subgroup/module provenance for the selected K, R = Phi(K), M = K/R, T, C, and bridge data;
direct dual-invariant vanishing on the selected raw tower;
quotient-head simplicity on that same tower;
a raw nonzero invariant determinant character on the Frattini layer.

It also exposes a drop-in Nonempty (MinimalBlockGroupTowerData p chief) provider with the same consumer shape as minimalBlock_groupTowerData_from_kernelRoute126Closers.

Concrete-final provenance kernel provider #

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute130Closers.provenanceConcreteFinalPieces_from_route130Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

Route130 concrete-final provenance pieces.

This is the strictly smaller manuscript-shaped packet used to rebuild the Route130 provenance-semantic leaf.

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute130Closers.provenanceSemanticData_from_route130Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockProvenanceSemanticData chief)

Route130 replacement for the broad provenance-semantic kernel leaf.

The axiom closure is inherited from minimalBlock_provenanceSemanticData_from_concreteFinalProofs, not from the residual axiom minimalBlock_provenanceSemanticData.

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute130Closers.lowerGroupModuleData_from_route130Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockLowerGroupModuleData chief)

The selected lower group/module tower supplied by the Route130 concrete-final provenance route.

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute130Closers.groupInvariantRouteData_from_route130Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route130 group/invariant packet through concrete-final provenance.

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute130Closers.groupTowerData_from_route130Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupTowerData p chief)

Route130 kernel provider with the same downstream consumer shape as minimalBlock_groupTowerData_from_kernelRoute126Closers.

Axiom-closure effect relative to Route126's kernel provider:

removes minimalBlock_provenanceSemanticData;
adds the concrete-final atoms exposed by minimalBlock_provenanceConcreteFinalPieces_from_existingClosers.

Public route-ready aliases #

source

theorem Q2Presentation.Induction.minimalBlock_provenanceConcreteFinalPieces_from_kernelRoute130Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

Public concrete-final provenance provider for the Route130 kernel closer.

source

theorem Q2Presentation.Induction.minimalBlock_provenanceSemanticData_from_kernelRoute130Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockProvenanceSemanticData chief)

Public provenance-semantic provider for the Route130 kernel closer.

source

theorem Q2Presentation.Induction.minimalBlock_lowerGroupModuleData_from_kernelRoute130Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockLowerGroupModuleData chief)

Public lower-tower provider for the Route130 kernel closer.

source

theorem Q2Presentation.Induction.minimalBlock_groupInvariantRouteData_from_kernelRoute130Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupInvariantRouteData chief)

Public group/invariant route packet for the Route130 kernel closer.

source

theorem Q2Presentation.Induction.minimalBlock_groupTowerData_from_kernelRoute130Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupTowerData p chief)

Public drop-in kernel provider matching the Route126 consumer shape.

Route130 audit branch with only the kernel provider swapped #

source

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_currentIntegrated130_kernelRoute130Closers (p : FramedPair) :

¬ScalarTerminal p → Nonempty (FourierBranchData p)

Route130 nonterminal branch with the kernel provider swapped to this sidecar. This is for audit/public-route readiness; IntegratedCurrentRouteProofs130 itself is unchanged.

source

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated130_kernelRoute130Closers (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 for the Route130 audit path with the kernel provider swapped.

source

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_currentIntegrated130_kernelRoute130Closers (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 for the Route130 audit path with the kernel provider swapped.

source

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_currentIntegrated130_kernelRoute130Closers (p : FramedPair) :

framedCountA p = framedCountQ p

Framed-count equality for the Route130 audit path with the kernel provider swapped.

source

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

Finite-surjection equality for the Route130 audit path with the kernel provider swapped.