Documentation

Q2Presentation.Induction.Section7PushoutRoute151Closers

Route151 Section 7 pushout/determinant closers #

This sidecar leaves every integrated route and root import untouched.

Route150 compacted the Section 7 pushout/determinant frontier to four leaves:

The providers below lower that compact surface through the Route82 manuscript-shaped scalar pushout API. The square family is the extraspecial square attached to the same phi_lambda pairing, so the diagonal and polar identities are theorem-level projections. The selected simple-head determinant packet is the Route82 prop:simpleheaddet surface: naturality, annihilation on T, and descended nonsingularity/radical containment for the same family.

The selected Route151 central-pushout family #

source
def Q2Presentation.Induction.Section7PushoutRoute151Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82.toRoute151QuadraticFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) :
MinimalBlockPreheadCentralPushoutQuadraticFamilyData D

Route151's selected compact quadratic family from the Route82 scalar-pushout pairing construction.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Q2Presentation.Induction.Section7PushoutRoute151Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82.route151SquareDiagonal {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) :
    MinimalBlockPreheadCentralPushoutSquareDiagonalData (toRoute151QuadraticFamily Phi)

    The square diagonal is definitional for the selected extraspecial square.

    Equations
    • ⋯ = ⋯
    Instances For
      source
      def Q2Presentation.Induction.Section7PushoutRoute151Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82.route151PolarSymm {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) :
      MinimalBlockPreheadCentralPushoutPolarSymmData (toRoute151QuadraticFamily Phi)

      The polar form is the symmetrized phi_lambda pairing, definitionally.

      Equations
      • ⋯ = ⋯
      Instances For
        source
        def Q2Presentation.Induction.Section7PushoutRoute151Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82.toRoute151Semantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) :
        MinimalBlockPreheadCentralPushoutSemanticData D

        The semantic family selected by the same Route82 scalar-pushout pairing.

        Equations
        Instances For

          Individual compact leaf lowerings #

          source
          theorem Q2Presentation.Induction.Section7PushoutRoute151Closers.minimalBlock_preheadCentralPushoutQuadraticFamilyData_from_section7PushoutRoute151Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) :
          Nonempty (MinimalBlockPreheadCentralPushoutQuadraticFamilyData D)

          Route151 replacement for the compact quadratic-family leaf.

          Its nonstandard closure uses only the Route82 scalar-pushout pairing construction residual, not the compact Route150 quadratic-family axiom.

          source
          theorem Q2Presentation.Induction.Section7PushoutRoute151Closers.minimalBlock_preheadCentralPushoutSquareDiagonalData_from_section7PushoutRoute151Closers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) :
          Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData (MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82.toRoute151QuadraticFamily Phi))

          Route151 selected square-diagonal packet for the same lowered family.

          source
          theorem Q2Presentation.Induction.Section7PushoutRoute151Closers.minimalBlock_preheadCentralPushoutPolarSymmData_from_section7PushoutRoute151Closers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D) :
          Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData (MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82.toRoute151QuadraticFamily Phi))

          Route151 selected polar-symmetry packet for the same lowered family.

          source
          theorem Q2Presentation.Induction.Section7PushoutRoute151Closers.minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData_selected_from_section7PushoutRoute151Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) :
          ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S)

          Route151 selected actual simple-head determinant packet.

          This lowers the compact Route150 actual determinant leaf to the three remaining Route82 prop:simpleheaddet residuals over the selected pairing: naturality, annihilation on T, and descended nonsingularity.

          Four-leaf Route150 compact-surface provider #

          source
          theorem Q2Presentation.Induction.Section7PushoutRoute151Closers.minimalBlock_preheadRoute150PushoutAtoms_from_section7PushoutRoute151Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) :
          ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutQuadraticFamilyData D) ∧ Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData S.toQuadraticFamily) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData S.toQuadraticFamily) ∧ Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S)

          The exact four compact Route150 pushout/determinant surfaces, selected from one Route82 scalar-pushout construction.

          This is the audit-facing Route151 provider: its axiom closure contains the four Route82 residuals and none of the four compact Route150 leaves.

          Route-ready downstream providers #

          source
          theorem Q2Presentation.Induction.Section7PushoutRoute151Closers.minimalBlock_preheadPushoutRouteLowerData_from_section7PushoutRoute151Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) :
          Nonempty (MinimalBlockPreheadPushoutRouteLowerData D)

          Route151 lower pushout packet through the same Route82 scalar-pushout provider.

          source
          theorem Q2Presentation.Induction.Section7PushoutRoute151Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute151Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) :
          ∃ (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D), Nonempty (MinimalBlockPreheadExtraspecialAnnihilationData F) ∧ Nonempty (MinimalBlockPreheadExtraspecialRadicalData F)

          Drop-in determinant-packet provider for future integrated routes.