Route126 kernel closers

This sidecar leaves the promoted Route126 files untouched. It supplies a drop-in kernel provider with the same downstream consumer shape as minimalBlock_groupTowerData_from_kernelRoute124Closers:

Nonempty (MinimalBlockGroupTowerData p chief)

Route124/Route126 public currently use two Section 7 kernel leaves:

• minimalBlock_lowerGroupModuleData;
• minimalBlock_invariantActualProofs2Data.

The theorem below replaces those two leaves by the same-tower provenance packet

• minimalBlock_provenanceSemanticData.

This packet is manuscript-shaped: it fixes the concrete K, R = Phi(K), M = K/R, T, C provenance and carries the head and lower-character data on the raw tower extracted from that same provenance.

Same-tower provenance kernel provider

theorem Q2Presentation.Induction.MinimalBlockKernelRoute126Closers.provenanceSemanticData_from_route126Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceSemanticData chief)

Route126 provenance-semantic packet.

This is the single remaining kernel provenance leaf for this sidecar.

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

The lower group/module tower selected by the Route126 provenance packet.

The axiom closure is minimalBlock_provenanceSemanticData, not minimalBlock_lowerGroupModuleData.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute126Closers.invariantActualProofs2Data_from_route126ClosersProvenance {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockProvenanceSemanticData chief) : Nonempty (MinimalBlockInvariantActualProofs2Data P.lower.rawTowerData)

The invariant packet on the lower tower selected by one provenance packet.

This is theorem-level once the provenance packet is available: its head and lower-character fields are exactly the fields required by MinimalBlockInvariantActualProofs2Data.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute126Closers.invariantActualProofs2Data_from_route126ClosersSelected {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (lower : MinimalBlockLowerGroupModuleData chief), Nonempty (MinimalBlockInvariantActualProofs2Data lower.rawTowerData)

Selected-lower invariant packet supplied by the Route126 provenance packet.

Unlike the Route124 public alias, this theorem intentionally exposes the lower tower existentially; the invariant packet is attached only to the lower tower selected by the same provenance object.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute126Closers.groupInvariantRouteData_from_route126Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route126 group/invariant packet through same-tower provenance.

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

Route126 kernel provider with the same consumer shape as minimalBlock_groupTowerData_from_kernelRoute124Closers.

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

• removes minimalBlock_lowerGroupModuleData;
• removes minimalBlock_invariantActualProofs2Data;
• adds minimalBlock_provenanceSemanticData.

Public route-ready aliases

theorem Q2Presentation.Induction.minimalBlock_provenanceSemanticData_from_kernelRoute126Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceSemanticData chief)

Public provenance provider for the Route126 kernel closer.

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

Public lower-tower provider for the Route126 kernel closer.

theorem Q2Presentation.Induction.minimalBlock_invariantActualProofs2Data_from_kernelRoute126Closers_selected {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (lower : MinimalBlockLowerGroupModuleData chief), Nonempty (MinimalBlockInvariantActualProofs2Data lower.rawTowerData)

Public selected-lower invariant provider for the Route126 kernel closer.

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

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

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

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

Route126 audit branch with only the kernel provider swapped

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

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

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

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

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

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

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