Route152 Section 7 kernel packet lowering

This sidecar leaves the integrated Route152 file untouched. It strictly lowers the current kernel leaf

Section7KernelRoute151Closers.kernelRoute151SelectedPackageData

by splitting the selected Section 7 packet into manuscript-shaped facts:

• the selected minimal K over the first non-scalar chief factor;
• the concrete Frattini layer R = Phi(K);
• the raw R, M = K/R, T, C object/action bridge;
• the same-raw-tower head action, direct dual-invariant vanishing, head simplicity, and raw lower invariant-character facts.

The bridge below reconstructs the exact Route151 packet from these smaller facts, so supervisors can swap the single Route151 leaf for this lowered route without editing the existing integrated theorem in this worker turn.

structure Q2Presentation.Induction.Section7KernelRoute152Closers.KernelRoute152ProvenanceModuleFacts {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route152 split facts for the Route151 selected kernel packet.

The last four fields are the same raw-tower contents of manuscript lem:simplehead and the lower Frattini character, rather than the monolithic Route151 invariant field.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattini : MinimalBlockKernelModuleConcreteFrattiniData self.least
• rawBridge : MinimalBlockKernelRoute78RawObjectClosers.RawObjectActionBridgeData self.least ⋯
• headAction : MinimalBlockRawHeadActionNotPointwiseTrivialData self.rawBridge.rawData.rawTowerData
• dualInvariant : MinimalBlockDualInvariantVanishesData self.rawBridge.rawData.rawTowerData
• headSimplicity : MinimalBlockRawHeadSimplicityActualData self.rawBridge.rawData.rawTowerData
• rawInvariantCharacter : MinimalBlockRawInvariantCharacterData self.rawBridge.rawData.rawTowerData

def Q2Presentation.Induction.Section7KernelRoute152Closers.KernelRoute152ProvenanceModuleFacts.headNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute152ProvenanceModuleFacts chief) : MinimalBlockHeadNontrivialData D.rawBridge.rawData.rawTowerData

The nonzero head quotient, recovered from the same raw tower's nontrivial head action.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7KernelRoute152Closers.KernelRoute152ProvenanceModuleFacts.headActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute152ProvenanceModuleFacts chief) : MinimalBlockRawHeadSimpleNoTrivialActualData D.rawBridge.rawData.rawTowerData

The actual simple/no-trivial head packet on the selected raw tower.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7KernelRoute152Closers.KernelRoute152ProvenanceModuleFacts.lowerScalarData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute152ProvenanceModuleFacts chief) : MinimalBlockRawLowerScalarQuotientData D.rawBridge.rawData.rawTowerData

The lower scalar quotient rebuilt from a raw nonzero invariant character.

Equations

• D.lowerScalarData = Q2Presentation.Induction.MinimalBlockRawLowerScalarQuotientData.ofRawInvariantCharacter ⋯

def Q2Presentation.Induction.Section7KernelRoute152Closers.KernelRoute152ProvenanceModuleFacts.lowerCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute152ProvenanceModuleFacts chief) : MinimalBlockRawLowerInvariantCharacterActualData D.rawBridge.rawData.rawTowerData

The actual lower invariant character on the selected Frattini layer.

Equations

• D.lowerCharacterData = Q2Presentation.Induction.MinimalBlockRawLowerInvariantCharacterActualData.ofLowerScalarQuotient D.lowerScalarData

def Q2Presentation.Induction.Section7KernelRoute152Closers.KernelRoute152ProvenanceModuleFacts.invariantActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute152ProvenanceModuleFacts chief) : MinimalBlockInvariantActualProofs2Data D.rawBridge.rawData.rawTowerData

Reassemble the Route151 invariant field from the Route152 split facts.

Equations

• D.invariantActualData = { head := ⋯, lowerCharacter := D.lowerCharacterData }

def Q2Presentation.Induction.Section7KernelRoute152Closers.KernelRoute152ProvenanceModuleFacts.toRoute151Package {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute152ProvenanceModuleFacts chief) : Section7KernelRoute151Closers.KernelRoute151SelectedPackageData chief

Forget the Route152 split facts to the exact Route151 selected packet.

Equations

• D.toRoute151Package = { least := D.least, frattini := ⋯, rawBridge := D.rawBridge, invariant := D.invariantActualData }

theorem Q2Presentation.Induction.Section7KernelRoute152Closers.kernelRoute151SelectedPackageData_of_route152ProvenanceModuleFacts {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute152ProvenanceModuleFacts chief) : Nonempty (Section7KernelRoute151Closers.KernelRoute151SelectedPackageData chief)

Bridge theorem: the split Route152 provenance/module facts imply the exact Route151 selected packet target.

theorem Q2Presentation.Induction.Section7KernelRoute152Closers.kernelRoute152ProvenanceModuleFacts_from_existingLowerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelRoute152ProvenanceModuleFacts chief)

Route152 split facts from existing lower Section 7 data.

This theorem is the workhorse lowering: its axiom closure replaces the single Route151 packet leaf by the selected Route78 least/Frattini packets, the Route141 raw object/action bridge, and the same-raw-tower direct head/lower invariant facts.

theorem Q2Presentation.Induction.Section7KernelRoute152Closers.kernelRoute151SelectedPackageData_from_section7KernelRoute152Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (Section7KernelRoute151Closers.KernelRoute151SelectedPackageData chief)

Route151 packet theorem with the Route152 split provenance/module lowering.

The axiom closure of this theorem is the intended replacement for Section7KernelRoute151Closers.kernelRoute151SelectedPackageData.