Documentation

Q2Presentation.Induction.Section7KernelRoute183Closers

Route183 Section 7 kernel/provenance lowering #

This sidecar targets the compact Route182 Section 7 kernel frontier:

No new assumptions are introduced here. The Route78 packets are supplied by the existing Route141/Route175 Frattini lowerings, and the Route167 raw packets are supplied by Route180's Route43 literal object/action/head lowerings.

Route78 compact Frattini packets lowered through Route141/175 #

source
theorem Q2Presentation.Induction.Section7KernelRoute183Closers.leastKernelSelectedData_from_route183Kernel {p : FramedPair} (chief : NonScalarChiefFactor p) :
Nonempty (MinimalBlockKernelRoute78FrattiniClosers.LeastKernelSelectedData chief)

Route183 replacement for the compact Route78 least-kernel selected packet.

source
theorem Q2Presentation.Induction.Section7KernelRoute183Closers.leastOverChiefData_from_route183Kernel {p : FramedPair} (chief : NonScalarChiefFactor p) :
Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route-ready least-over-chief packet for Route183.

source
theorem Q2Presentation.Induction.Section7KernelRoute183Closers.frattiniInternalSelectedData_from_route183Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :
Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniInternalSelectedData K)

Route183 replacement for the compact Route78 internal Frattini witness.

source
theorem Q2Presentation.Induction.Section7KernelRoute183Closers.frattiniCentralizerSelectedData_from_route183Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :
Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniCentralizerSelectedData K)

Route183 replacement for the compact Route78 Frattini-centralizer packet.

source
theorem Q2Presentation.Induction.Section7KernelRoute183Closers.fourthPowerKernelSelectedData_from_route183Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :
Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FourthPowerKernelSelectedData K)

Route183 replacement for the compact Route78 fourth-power packet.

source
theorem Q2Presentation.Induction.Section7KernelRoute183Closers.frattiniSquareCommutatorLiteralExponentData_from_route183Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :
Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniSquareCommutatorLiteralExponentData K)

Route183 replacement for the compact Route78 literal Frattini exponent packet. This uses Route175's literal carrier closure, so the carrier selector is not part of the residual frontier.

source
theorem Q2Presentation.Induction.Section7KernelRoute183Closers.frattiniData_from_route183Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :
Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Concrete Frattini packet for the Route183 kernel provider.

Route167 raw packets lowered through Route180/Route43 #

source
theorem Q2Presentation.Induction.Section7KernelRoute183Closers.rawQuotientTowerData_from_route183Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) :
Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Route183 replacement for Section7KernelRoute167Closers.rawQuotientTowerData.

The residual dependencies are Route43 literal raw-object/action/head packets, not the compact Route167 raw tower atom.

source
theorem Q2Presentation.Induction.Section7KernelRoute183Closers.rawSimpleHeadSemanticData_from_route183Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Q : MinimalBlockKernelRawQuotientTowerData K F) :
Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData Q.rawData.rawTowerData)

Route183 replacement for Section7KernelRoute167Closers.rawSimpleHeadSemanticData.

The same raw tower is interpreted through Route180's Route43 simple-head pieces.

Same-tower Route183 provider #

source
structure Q2Presentation.Induction.Section7KernelRoute183Closers.KernelRoute183ModuleLayerData {p : FramedPair} (chief : NonScalarChiefFactor p) :
Type 1

Route183 same-tower module layer: selected least kernel, concrete Frattini collapse, literal raw quotient tower, and same-tower simple-head semantics.

Instances For
    source
    def Q2Presentation.Induction.Section7KernelRoute183Closers.KernelRoute183ModuleLayerData.concreteProvenanceData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute183ModuleLayerData chief) :
    MinimalBlockKernelModuleConcreteProvenanceData chief

    Forget the Route183 module-layer packet to concrete kernel provenance.

    Equations
    Instances For
      source
      def Q2Presentation.Induction.Section7KernelRoute183Closers.KernelRoute183ModuleLayerData.lowerGroupModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute183ModuleLayerData chief) :
      MinimalBlockLowerGroupModuleData chief

      Lower group/module data selected by the Route183 packet.

      Equations
      Instances For
        source
        def Q2Presentation.Induction.Section7KernelRoute183Closers.KernelRoute183ModuleLayerData.invariantActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute183ModuleLayerData chief) :
        MinimalBlockInvariantActualProofs2Data D.lowerGroupModuleData.rawTowerData

        Same-tower invariant packet from the Route183 simple-head semantics.

        Equations
        Instances For
          source
          def Q2Presentation.Induction.Section7KernelRoute183Closers.KernelRoute183ModuleLayerData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute183ModuleLayerData chief) :
          MinimalBlockGroupTowerData p chief

          The group tower consumed by the Section 7 Fourier branch.

          Equations
          Instances For
            source
            theorem Q2Presentation.Induction.Section7KernelRoute183Closers.kernelRoute183ModuleLayerData_from_section7KernelRoute183Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :
            Nonempty (KernelRoute183ModuleLayerData chief)

            Route183 module-layer packet through the lowered Frattini and raw providers.

            source
            theorem Q2Presentation.Induction.Section7KernelRoute183Closers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute183Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :
            Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

            Concrete kernel/module provenance through Route183.

            source
            theorem Q2Presentation.Induction.Section7KernelRoute183Closers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute183Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :
            Nonempty (MinimalBlockLowerGroupModuleData chief)

            Lower group/module data through Route183.

            source
            theorem Q2Presentation.Induction.Section7KernelRoute183Closers.minimalBlock_groupTowerData_from_section7KernelRoute183Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :
            Nonempty (MinimalBlockGroupTowerData p chief)

            Drop-in Route183 Section 7 kernel provider for integrated routes.