Route147 Section 7 combined kernel closers

This sidecar leaves the integrated Route147 file and root imports untouched. It packages the Route146 least/Frattini and Route146 raw/head providers into Route147-named kernel providers, and also gives a compact same-tower variant in which the four split raw-head/lower atoms are replaced by the coherent MinimalBlockInvariantActualProofs2Data packet on the selected raw tower.

The manuscript shape is the Section 7 tower

• selected least K;
• R = Phi(K) with Frattini collapse;
• raw R, M = K/R, T, C objects and actions;
• a nontrivial simple head and lower invariant character on that same tower.

Shared concrete assembly

def Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.concreteProvenanceDataOfRawQuotientTower {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) (Q : MinimalBlockKernelRawQuotientTowerData K F) : MinimalBlockKernelModuleConcreteProvenanceData chief

Assemble concrete provenance from a selected least kernel, Frattini collapse, and same-tower raw quotient/head packet.

Equations

• One or more equations did not get rendered due to their size.

Split Route147 package

structure Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.KernelModuleConcreteRoute147Data {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route147 split kernel package: Route78 selected least/Frattini data plus Route141/Route146 raw quotient/head data for the same selected K,F.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattini : MinimalBlockKernelModuleConcreteFrattiniData self.least
• rawTower : MinimalBlockKernelRawQuotientTowerData self.least ⋯

def Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.KernelModuleConcreteRoute147Data.concreteProvenanceData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelModuleConcreteRoute147Data chief) : MinimalBlockKernelModuleConcreteProvenanceData chief

Forget the split package to concrete kernel/module provenance.

Equations

• D.concreteProvenanceData = Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.concreteProvenanceDataOfRawQuotientTower D.least ⋯ D.rawTower

theorem Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.kernelModuleConcreteRoute147Data_from_route147CombinedClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelModuleConcreteRoute147Data chief)

Route147 split package from the two Route146 Section 7 sidecars.

theorem Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute147CombinedClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Drop-in Route147 provider for concrete kernel/module provenance.

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

Drop-in Route147 provider for lower group/module data.

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

Drop-in Route147 provider for the minimal-block group tower.

Compact same-tower raw-head/lower package variant

def Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.rawHeadActionNotPointwiseTrivialData_of_invariantActual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockInvariantActualProofs2Data D) : MinimalBlockRawHeadActionNotPointwiseTrivialData D

Convert the coherent same-tower invariant packet into the concrete not-pointwise-trivial head-action packet needed to build head nontriviality.

Equations

• ⋯ = ⋯

structure Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.KernelModuleConcreteRoute147InvariantPackageData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route147 compact package: the raw objects/actions/bridge are Route141-owned, while the simple-head and lower-character data are supplied by one coherent same-tower invariant packet.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattini : MinimalBlockKernelModuleConcreteFrattiniData self.least
• rawBridge : MinimalBlockKernelRoute78RawObjectClosers.RawObjectActionBridgeData self.least ⋯
• invariant : MinimalBlockInvariantActualProofs2Data self.rawBridge.rawData.rawTowerData

def Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.KernelModuleConcreteRoute147InvariantPackageData.rawQuotientTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelModuleConcreteRoute147InvariantPackageData chief) : MinimalBlockKernelRawQuotientTowerData D.least ⋯

The raw quotient/head packet recovered from the compact invariant package.

Equations

• D.rawQuotientTowerData = { objects := D.rawBridge.rawObjects, actions := D.rawBridge.rawActions, bridge := id (id D.rawBridge.rawBridge), head := ⋯ }

def Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.KernelModuleConcreteRoute147InvariantPackageData.concreteProvenanceData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelModuleConcreteRoute147InvariantPackageData chief) : MinimalBlockKernelModuleConcreteProvenanceData chief

Forget the compact invariant package to concrete kernel/module provenance.

Equations

• D.concreteProvenanceData = Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.concreteProvenanceDataOfRawQuotientTower D.least ⋯ D.rawQuotientTowerData

theorem Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.kernelModuleConcreteRoute147InvariantPackageData_from_route147CombinedClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelModuleConcreteRoute147InvariantPackageData chief)

Route147 compact same-tower package. This replaces the four split raw-head and lower-scalar atoms by the coherent minimalBlock_invariantActualProofs2Data packet on the selected raw object/action tower.

theorem Q2Presentation.Induction.Section7KernelRoute147CombinedClosers.minimalBlock_kernelModuleConcreteProvenanceData_from_route147CombinedInvariantPackage {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Compact Route147 concrete provenance provider using the same-tower invariant package instead of the four split raw-head/lower atoms.

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

Compact Route147 lower group/module provider.

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

Compact Route147 group-tower provider. The invariant packet is requested on the selected lower tower, so the final dual-invariant and raw-character fields stay tied to the concrete provenance selected above.

Acceptance checks