Documentation

Q2Presentation.Induction.MinimalBlockKernelRoute114Closers

Route114 kernel closers #

This sidecar does not edit Route114. It targets the five kernel Section 7 leaves still visible in the public Route114 audit:

The candidate, Frattini-collapse, raw-quotient, and invariant packet surfaces are re-provided by theorem-level route closers. The universal leastness leaf is lowered to the selected least-kernel packet used downstream: one candidate together with its universal property, from which the route-ready MinimalBlockKernelLeastOverChiefData is recovered.

Least kernel #

source
structure Q2Presentation.Induction.MinimalBlockKernelRoute114Closers.LeastKernelSelectedData {p : FramedPair} (chief : NonScalarChiefFactor p) :
Type

Route114 selected least-kernel packet.

This is the downstream shape that replaces the arbitrary-candidate minimalBlock_kernelLeastUniversalData frontier: Route114 consumers only need one selected candidate and its universal minimality proof.

Instances For
    source
    def Q2Presentation.Induction.MinimalBlockKernelRoute114Closers.LeastKernelSelectedData.leastOverChief {p : FramedPair} {chief : NonScalarChiefFactor p} (D : LeastKernelSelectedData chief) :
    MinimalBlockKernelLeastOverChiefData chief

    Forget the selected candidate/universal packet to the route-ready least kernel data.

    Equations
    Instances For
      source
      theorem Q2Presentation.Induction.MinimalBlockKernelRoute114Closers.leastCandidateData_from_route114Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :
      Nonempty (MinimalBlockKernelCandidateData chief)

      Candidate half of the Route114 least-kernel split.

      source
      theorem Q2Presentation.Induction.MinimalBlockKernelRoute114Closers.leastKernelSelectedData_from_route114Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :
      Nonempty (LeastKernelSelectedData chief)

      Selected universal leastness for the candidate used by the Route114 kernel provider.

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

      Route-ready least-over-chief data recovered from the selected Route114 least-kernel packet.

      Frattini collapse #

      source
      theorem Q2Presentation.Induction.MinimalBlockKernelRoute114Closers.frattiniCollapseFullData_from_route114Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :
      Nonempty (MinimalBlockKernelFrattiniCollapseFullData K)

      Route114 replacement for the coherent Frattini-collapse packet.

      Invariant and raw-head conversions #

      source
      def Q2Presentation.Induction.MinimalBlockKernelRoute114Closers.headActionNotPointwiseTrivial_of_invariantActual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockInvariantActualProofs2Data D) :
      MinimalBlockRawHeadActionNotPointwiseTrivialData D

      Convert the actual invariant packet's nontrivial action witness into the not-pointwise-trivial form needed to construct a nonzero concrete head.

      Equations
      • ⋯ = ⋯
      Instances For
        source
        theorem Q2Presentation.Induction.MinimalBlockKernelRoute114Closers.invariantActualProofs2Data_from_route114Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :
        Nonempty (MinimalBlockInvariantActualProofs2Data D)

        Route114 replacement for minimalBlock_invariantActualProofs2Data, using the Route112 raw-head lowering.

        Raw quotient tower #

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

        Route114 raw-quotient tower packet.

        The raw objects, actions, and bridge come from the Route90/Route110 core lowering. The head nontriviality field is supplied from the newer Route112 same-raw-tower invariant packet, so this theorem avoids the monolithic minimalBlock_kernelRawQuotientTowerData and minimalBlock_invariantActualProofs2Data leaves.

        Route-ready kernel provider #

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

        Concrete provenance through the Route114 kernel-lowered tower.

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

        Lower group/module data through the Route114 kernel-lowered tower.

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

        Route114 kernel group-tower provider with the kernel frontier lowered through the selected least-kernel, Route110 core, Route90 raw-bridge, and Route112 invariant providers.

        Public aliases #

        source
        theorem Q2Presentation.Induction.minimalBlock_kernelLeastCandidateData_from_route114Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :
        Nonempty (MinimalBlockKernelCandidateData chief)

        Public candidate-half closer for the Route114 kernel frontier.

        source
        theorem Q2Presentation.Induction.minimalBlock_kernelSelectedLeastUniversalData_from_route114Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :
        Nonempty (MinimalBlockKernelRoute114Closers.LeastKernelSelectedData chief)

        Public selected-universal closer for the Route114 kernel frontier.

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

        Public least-over-chief provider recovered from the Route114 selected least-kernel packet.

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

        Public Frattini-collapse closer for the Route114 kernel frontier.

        source
        theorem Q2Presentation.Induction.minimalBlock_invariantActualProofs2Data_from_route114Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :
        Nonempty (MinimalBlockInvariantActualProofs2Data D)

        Public invariant-packet closer for the Route114 kernel frontier.

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

        Public raw-quotient tower closer for the Route114 kernel frontier.

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

        Public concrete-provenance provider for the Route114 kernel-lowered tower.

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

        Public lower-tower provider for the Route114 kernel-lowered tower.

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

        Public Route114-compatible kernel provider.

        Route114 audit branch using the kernel provider #

        source
        theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_currentIntegrated114_kernelClosers (p : FramedPair) :
        ¬ScalarTerminal p → Nonempty (FourierBranchData p)

        Route114 nonterminal branch with only the kernel provider swapped to this sidecar's Route114 kernel closer.