Documentation

Q2Presentation.Induction.MinimalBlockKernelRoute216KernelRawCompactClosers

Route216 compact Section 7 kernel/raw provider #

This sidecar is route-neutral: it does not edit the integrated Route216 theorem.

The manuscript's Section 7, pages 40--42, chooses one minimal normal subgroup K, sets R = Phi(K), forms the quotient tower Y -> B = Y/R -> C = Y/K, and proves the simple-head and Frattini-centralizer-collapse facts on that same selected tower. This file records that construction as one compact kernel/raw layer packet, then derives the same public provider shape used by the current Route216 baseline:

Nonempty (MinimalBlockGroupTowerData p chief).

The point of this sidecar is compact closure, not a wide pointwise lowering. It avoids both the old Route212 split leaves and the Route214/Route200 pointwise decomposition.

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

Compact manuscript-shaped Section 7 kernel/raw layer.

The fields are intentionally dependent: the Frattini collapse, raw quotient tower, bridge, head nontriviality, and simple-head semantic packet all belong to the same selected least kernel K and its literal Phi(K) layer.

Instances For
    source
    axiom Q2Presentation.Induction.Section7KernelRoute216KernelRawCompactClosers.kernelRawCompactLayerData {p : FramedPair} (chief : NonScalarChiefFactor p) :
    Nonempty (KernelRawCompactLayerData chief)

    Residual compact Section 7 kernel/raw packet.

    This is the single Lean frontier for the manuscript construction: minimal K, R = Phi(K) with Lemma 7.2 collapse, raw R,M,T,C quotient transport, and Lemma 7.1 simple-head semantics on the same tower.

    source
    def Q2Presentation.Induction.Section7KernelRoute216KernelRawCompactClosers.KernelRawCompactLayerData.concreteProvenanceData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRawCompactLayerData chief) :
    MinimalBlockKernelModuleConcreteProvenanceData chief

    Forget the compact packet to the concrete provenance API used downstream.

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

      Lower group/module data selected by the compact packet.

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

        Same-tower actual invariant data obtained from the simple-head semantic packet carried by the compact layer.

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

          The group tower consumed by the Section 7 Fourier branch.

          Equations
          Instances For
            source
            theorem Q2Presentation.Induction.Section7KernelRoute216KernelRawCompactClosers.minimalBlock_groupTowerData_from_section7KernelRoute216KernelRawCompactClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :
            Nonempty (MinimalBlockGroupTowerData p chief)

            Drop-in compact Section 7 kernel provider for a Route216 replay.