Route52 minimal-block pushout/determinant narrowing

Route51 still consumes the Route50 determinant provider minimalBlock_preheadDeterminantPackets_from_route50, whose closure bottoms out in the single Route50 residual minimalBlock_preheadSimpleHeadDeterminantRoute50Data.

This sidecar proves the same provider surface from the manuscript-shaped Section 7 determinant pieces:

• one semantic central-pushout family S;
• naturality/equivariance of S.phi;
• diagonal vanishing on T;
• polar vanishing on T x M;
• radical containment in T.

Those are exactly the four prop:simpleheaddet conclusions for the scalar central pushouts K_lambda = K / ker lambda, tied to the same semantic family. No new residual axiom is introduced here.

Manuscript-shaped determinant pieces

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute52DeterminantPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Prop

The four same-family pieces of prop:simpleheaddet used by Route52.

This has a route-specific name to avoid colliding with older experimental sidecars that used the same final-closer theorem names.

• simpleHeadEquivariance : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S
• diagonalZero : MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S
• polarZero : MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S
• radicalContainment : MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute52DeterminantPieces.toActualSplit {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (P : MinimalBlockPreheadCentralPushoutRoute52DeterminantPieces S) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData S

Forget the Route52-specific field names to the existing split actual determinant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute52DeterminantPieces.toActualData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (P : MinimalBlockPreheadCentralPushoutRoute52DeterminantPieces S) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S

Convert the four Route52 pieces to the current actual simple-head determinant packet.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutRoute52DeterminantPieces_from_semanticPackets {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutRoute52DeterminantPieces S)

Assemble the four Route52 determinant pieces for the same semantic central-pushout family.

Route52 packet

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

Route52 determinant data.

The determinant pieces are indexed by the selected semantic central-pushout family, so the equivariance, annihilation, and radical conclusions all come from one same-family prop:simpleheaddet packet rather than from Route50's opaque bundled residual.

• semantic : MinimalBlockPreheadCentralPushoutSemanticData D
• determinantPieces : MinimalBlockPreheadCentralPushoutRoute52DeterminantPieces self.semantic

def Q2Presentation.Induction.MinimalBlockPreheadDeterminantRoute52Data.actualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadDeterminantRoute52Data D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData P.semantic

The actual semantic determinant packet assembled from Route52's four manuscript-shaped pieces.

Equations

• ⋯ = ⋯

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

The bare extraspecial family selected by the Route52 semantic pushout.

Equations

• P.family = P.semantic.toExtraspecialFamily

def Q2Presentation.Induction.MinimalBlockPreheadDeterminantRoute52Data.simpleHeadDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadDeterminantRoute52Data D) : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData P.family

The Route50-style simple-head determinant theorem projected from the same-family Route52 determinant pieces.

Equations

• ⋯ = ⋯

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

Repackage Route52 data as the old Route50 packet shape.

Equations

• P.toRoute50Data = { family := P.family, simpleHeadDeterminant := ⋯ }

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

Repackage Route52 data directly as the lower pushout route packet.

Equations

• P.toPushoutRouteLowerData = { selfDuality := P.semantic.toSelfDuality, simpleHeadDeterminant := ⋯ }

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

Repackage Route52 data as the Route49 determinant packet shape.

Equations

• P.toRoute49Data = P.toRoute50Data.toRoute49Data

Route-compatible hooks

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

Construct Route52 data from the semantic central-pushout family and the four same-family simple-head determinant pieces.

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

Route52 proves Route50's old simple-head determinant packet without using minimalBlock_preheadSimpleHeadDeterminantRoute50Data.

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

Route52 proves the Route49 determinant packet without using either the Route49 or Route50 determinant residual axiom.

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

Lower pushout route from Route52's semantic determinant pieces.

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

Route52 determinant-packet projection.

This has the same conclusion as minimalBlock_preheadDeterminantPackets_from_route50, but its closure is the semantic central-pushout family plus the four manuscript-shaped simple-head determinant packets.

theorem Q2Presentation.Induction.minimalBlock_preheadDeterminantPackets_from_route50_via_route52 {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 Route50 provider surface.