Route58 minimal-block pushout/determinant refinement

Route55 exposes the active Section 7 pushout cluster as seven split actual central-extension packets:

• the actual phi_lambda family;
• the actual square-map family;
• diagonal and polar identities;
• naturality;
• annihilation on T;
• polar-radical containment.

This sidecar strictly reduces that cluster for the current Lean interface. Once phi_lambda is fixed, the normalized scalar pushout square can be taken to be the extraspecial square Extraspecial.extraspecialForm (phi_lambda). The square packet, diagonal identity, and polar identity are then theorem-level projections from PhiData; the remaining residuals are the actual construction of phi_lambda, naturality, annihilation, and radical containment for this normalized same-family square.

No routed file imports this sidecar yet. The exported provider minimalBlock_preheadDeterminantPackets_from_route58 has the same downstream surface as Route55 while avoiding the three split square/diagonal/polar packet axioms.

Normalized square, diagonal, and polar packets from phi_lambda

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionSquareData_from_route58Phi {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : Nonempty (MinimalBlockPreheadActualCentralExtensionSquareData Phi)

Route58 theorem-level replacement for the split square packet, once PhiData is fixed.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionDiagonalData_from_route58Phi {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : Nonempty (MinimalBlockPreheadActualCentralExtensionDiagonalData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi Phi))

Route58 theorem-level replacement for the split diagonal packet, tied to the normalized square packet above.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPolarData_from_route58Phi {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : Nonempty (MinimalBlockPreheadActualCentralExtensionPolarData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi Phi))

Route58 theorem-level replacement for the split polar packet, tied to the normalized square packet above.

Route58 same-family packet

structure Q2Presentation.Induction.MinimalBlockPushoutRoute58Data {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Type

Route58 packet: the normalized actual central-extension pushout family.

Compared with Route55's seven split leaves, this packet has four residual fields. The square, diagonal, and polar data are fixed theorem-level from phi; annihilation and radical containment are required for that exact normalized square family.

• phi : MinimalBlockPreheadActualCentralExtensionPhiData D
• naturality : MinimalBlockPreheadActualCentralExtensionNaturalityData self.phi
• annihilation : MinimalBlockPreheadActualCentralExtensionAnnihilationData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi self.phi)
• radical : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi self.phi)

def Q2Presentation.Induction.MinimalBlockPushoutRoute58Data.square {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute58Data D) : MinimalBlockPreheadActualCentralExtensionSquareData P.phi

The normalized square packet selected by Route58.

Equations

• P.square = Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi P.phi

def Q2Presentation.Induction.MinimalBlockPushoutRoute58Data.diagonal {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute58Data D) : MinimalBlockPreheadActualCentralExtensionDiagonalData P.square

The normalized diagonal packet selected by Route58.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute58Data.polar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute58Data D) : MinimalBlockPreheadActualCentralExtensionPolarData P.square

The normalized polar packet selected by Route58.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute58Data.actualPushout {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute58Data D) : MinimalBlockPreheadActualCentralExtensionPushoutData D

Reassemble the broad actual central-extension pushout packet from the Route58 normalized split packet.

Equations

• P.actualPushout = Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPushoutData.ofSplitPackets P.phi P.square ⋯ ⋯ ⋯ ⋯ ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute58Data.toRoute54Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute58Data D) : MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data D

Route58 projected to the Route54 coherent actual determinant packet.

Equations

• P.toRoute54Data = P.actualPushout.toRoute54Data

def Q2Presentation.Induction.MinimalBlockPushoutRoute58Data.toRoute53Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute58Data D) : MinimalBlockPreheadDeterminantRoute53Data D

Route58 projected to the Route53 determinant packet shape.

Equations

• P.toRoute53Data = P.toRoute54Data.toRoute53Data

def Q2Presentation.Induction.MinimalBlockPushoutRoute58Data.toRoute52Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute58Data D) : MinimalBlockPreheadDeterminantRoute52Data D

Route58 projected to the Route52 determinant packet shape.

Equations

• P.toRoute52Data = P.toRoute54Data.toRoute52Data

def Q2Presentation.Induction.MinimalBlockPushoutRoute58Data.toRoute50Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute58Data D) : MinimalBlockPreheadSimpleHeadDeterminantRoute50Data D

Route58 projected to the Route50 determinant packet shape.

Equations

• P.toRoute50Data = P.toRoute54Data.toRoute50Data

def Q2Presentation.Induction.MinimalBlockPushoutRoute58Data.toPushoutRouteLowerData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute58Data D) : MinimalBlockPreheadPushoutRouteLowerData D

Route58 projected to the lower pushout packet consumed by integration.

Equations

• P.toPushoutRouteLowerData = P.toRoute54Data.toPushoutRouteLowerData

Route-compatible hooks

theorem Q2Presentation.Induction.minimalBlock_pushoutRoute58Data_from_phiExtraspecialPackets {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPushoutRoute58Data D)

Construct Route58 data from four residual packets:

• PhiData;
• NaturalityData;
• AnnihilationData for the normalized square from PhiData;
• RadicalContainmentData for the same normalized square.

This theorem avoids the split square, diagonal, and polar packet axioms.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPushoutData_from_route58 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadActualCentralExtensionPushoutData D)

Route58 replacement for the broad actual central-extension pushout packet.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutActualDeterminantRoute54Data_from_route58 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadCentralPushoutActualDeterminantRoute54Data D)

Route58 replacement for Route54's coherent actual determinant packet.

theorem Q2Presentation.Induction.minimalBlock_preheadDeterminantRoute53Data_from_route58 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadDeterminantRoute53Data D)

Route53-shaped determinant data supplied by Route58.

theorem Q2Presentation.Induction.minimalBlock_preheadDeterminantRoute52Data_from_route58 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadDeterminantRoute52Data D)

Route52-shaped determinant data supplied by Route58.

theorem Q2Presentation.Induction.minimalBlock_preheadSimpleHeadDeterminantRoute50Data_from_route58 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadSimpleHeadDeterminantRoute50Data D)

Route50-shaped determinant data supplied by Route58.

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

Lower pushout route supplied by Route58.

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

Determinant-packet provider supplied by Route58.

This has the same consumed surface as minimalBlock_preheadDeterminantPackets_from_route55, but its axiom closure avoids the split square, diagonal, and polar packet axioms.

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

Explicit drop-in replacement name for auditing the Route55 provider surface.