Documentation

Q2Presentation.Induction.MinimalBlockKernelRoute106HeadClosers

Route106 kernel least/head closers #

This sidecar is isolated from the integrated route files. It targets the Route106 Section 7 least-over-chief and raw-head subcluster left by the Route103 kernel provider:

The lower tower keeps the Route106 coherent Frattini/raw-module route, but the least kernel is supplied by the candidate-plus-universal-leastness split from Route63. The same-tower simple-head packet is supplied by the Route63 raw-head lowering through the manuscript hyperplane/irreducibility/action/character packets, avoiding the three broader raw-head residual names.

Least-over-chief replacement #

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

Route106 head-side replacement for MinimalBlockKernelConcreteRoute45.leastOverChiefData_from_route45.

This avoids the direct minimalBlock_kernelLeastOverChiefData atom and exposes the candidate plus universal leastness split.

Concrete lower tower with the lowered least packet #

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

Concrete provenance through the Route106 coherent Frattini/raw route, but with least-over-chief lowered through the Route63 candidate/leastness split.

This is the Route45/Route106 concrete-provenance shape needed by Route103-style kernel providers.

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

Lower group/module data through the Route106 least/head lowered concrete tower.

Same-tower simple-head replacement #

source
theorem Q2Presentation.Induction.MinimalBlockKernelRoute106HeadClosers.rawSimpleHeadSemanticData_from_route106HeadClosersLower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) :
Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData lower.rawTowerData)

Route106 head-side replacement for MinimalBlockKernelConcreteRoute45.rawSimpleHeadSemanticData_from_route45Lower.

It lowers the three broad raw-head residuals to the Route43/Route63 semantic pieces: invariant hyperplanes contain T, quotient-head irreducibility, not-pointwise-trivial action, and lower invariant-character existence.

source
def Q2Presentation.Induction.MinimalBlockKernelRoute106HeadClosers.rawHeadQuotientNoTrivialData_of_rawSimpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D) :
MinimalBlockRawHeadQuotientNoTrivialData D

Projection of the lowered simple-head packet to the quotient-head no-trivial-dual data, without using minimalBlock_rawHeadQuotientNoTrivialData.

Equations
  • ⋯ = ⋯
Instances For
    source
    theorem Q2Presentation.Induction.MinimalBlockKernelRoute106HeadClosers.rawHeadQuotientNoTrivialData_from_route106HeadClosersLower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) :
    Nonempty (MinimalBlockRawHeadQuotientNoTrivialData lower.rawTowerData)

    Selected-tower quotient-head no-trivial-dual packet through the Route106 head lowering.

    source
    theorem Q2Presentation.Induction.MinimalBlockKernelRoute106HeadClosers.rawHeadSimplicityActualData_from_route106HeadClosersLower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) :
    Nonempty (MinimalBlockRawHeadSimplicityActualData lower.rawTowerData)

    Selected-tower quotient-head simplicity packet through the Route106 head lowering.

    source
    theorem Q2Presentation.Induction.MinimalBlockKernelRoute106HeadClosers.rawLowerScalarQuotientData_from_route106HeadClosersLower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) :
    Nonempty (MinimalBlockRawLowerScalarQuotientData lower.rawTowerData)

    Selected-tower lower scalar quotient packet through the Route106 head lowering.

    Route103-shaped provider #

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

    Route106 least/head-lowered kernel group-tower provider.

    This has the same consumer target as minimalBlock_groupTowerData_from_kernelRoute103Closers, so an integrated route can swap this theorem in for the Route103 kernel provider.

    Public aliases #

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

    Public least-over-chief alias for the Route106 head closer.

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

    Public concrete-provenance alias for the Route106 head closer.

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

    Public lower-tower alias for the Route106 head closer.

    source
    theorem Q2Presentation.Induction.minimalBlock_rawSimpleHeadSemanticData_from_kernelRoute106HeadClosers_lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) :
    Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData lower.rawTowerData)

    Public selected-tower simple-head alias for the Route106 head closer.

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

    Public selected-tower quotient-head no-trivial alias for the Route106 head closer.

    source
    theorem Q2Presentation.Induction.minimalBlock_rawHeadSimplicityActualData_from_kernelRoute106HeadClosers_lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) :
    Nonempty (MinimalBlockRawHeadSimplicityActualData lower.rawTowerData)

    Public selected-tower quotient-head simplicity alias for the Route106 head closer.

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

    Public selected-tower lower scalar quotient alias for the Route106 head closer.

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

    Public drop-in kernel provider replacing minimalBlock_groupTowerData_from_kernelRoute103Closers in Route106-style branches.

    Acceptance checks #