Route135 Section 7 kernel closers

This sidecar leaves the promoted route files untouched. It targets the three kernel/provenance leaves visible in the current Route135 worker-combined audit:

• minimalBlock_kernelModuleConcreteProvenanceData;
• minimalBlock_rawHeadQuotientNoTrivialData;
• minimalBlock_rawLowerScalarQuotientData.

The replacement uses the existing Route106 head closer. That route keeps the manuscript Section 7 tower K, R = Phi(K), M = K/R, T, and C, and rebuilds the quotient-head and lower-scalar packets from the finer raw simple-head semantic data. Candidate/target and pushout/determinant providers are inherited unchanged from Route135.

Kernel/provenance providers

theorem Q2Presentation.Induction.Section7KernelRoute135Closers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute135Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Route135 Section 7 replacement for the concrete provenance kernel leaf.

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

The selected lower tower attached to the Route135 kernel closer.

theorem Q2Presentation.Induction.Section7KernelRoute135Closers.minimalBlock_rawHeadQuotientNoTrivialData_from_section7KernelRoute135Closers_lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockRawHeadQuotientNoTrivialData lower.rawTowerData)

Selected-tower quotient-head no-trivial-dual packet, rebuilt from the Route106 raw simple-head semantic data rather than the broad Route135 leaf.

theorem Q2Presentation.Induction.Section7KernelRoute135Closers.minimalBlock_rawLowerScalarQuotientData_from_section7KernelRoute135Closers_lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockRawLowerScalarQuotientData lower.rawTowerData)

Selected-tower lower scalar quotient packet, rebuilt from the Route106 raw simple-head semantic data rather than the broad Route135 leaf.

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

Route135 drop-in kernel group-tower provider.

Route135 audit theorem with only the kernel provider swapped

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

Route135 nonterminal Fourier branch with the Section 7 kernel provider swapped to the Route106 head-lowered closer.

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

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

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

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

Route135 finite-surjection equality with only the Section 7 kernel provider swapped to this sidecar.