Route83 minimal-block determinant/pushout closer

Route82 lowers the determinant/pushout frontier to four packets attached to one abstract pairing Phi:

• construction of the central-pushout pairing family;
• naturality of that pairing;
• annihilation of T by the extraspecial square;
• nonsingularity after descent to the simple head.

This sidecar removes those free-standing Route82 residual providers from the route. The new coherent packet is closer to the manuscript proof of prop:simpleheaddet: it starts with the actual scalar central-pushout family and the same-family semantic determinant packet for the induced family. The Route82 packet is then recovered by theorem-level projection. In particular, the naturality/annihilation/nonsingularity fields are not supplied for an arbitrary external Phi; they are tied to the actual scalar-pushout pairing.

Manuscript anchors: Section 7, pages 41--42, especially the scalar pushouts K_lambda = K / ker lambda, the square map q_lambda, the two vanishing statements on T, and nonsingularity after descent to the simple head.

Route83 coherent actual-scalar/simple-head packet

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

Route83 coherent pushout datum.

actualScalar is the scalar central-pushout construction: it supplies the pairing family and identifies the square with the extraspecial square attached to that same family. determinant is the same-family semantic prop:simpleheaddet packet for the semantic family obtained from actualScalar.

• actualScalar : MinimalBlockPreheadActualScalarCentralPushoutData D
• determinant : MinimalBlockPreheadCentralPushoutCoherentDeterminantSemanticData self.actualScalar.toSemanticData

def Q2Presentation.Induction.MinimalBlockPushoutRoute83Closers.MinimalBlockPreheadPushoutRoute83Data.semantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute83Data D) : MinimalBlockPreheadCentralPushoutSemanticData D

The semantic central-pushout family selected by Route83.

Equations

• P.semantic = P.actualScalar.toSemanticData

def Q2Presentation.Induction.MinimalBlockPushoutRoute83Closers.MinimalBlockPreheadPushoutRoute83Data.toRoute82Pairing {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute83Data D) : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D

The Route82 pairing construction projected from the actual scalar pushout.

Equations

• P.toRoute82Pairing = { phi := P.actualScalar.phi }

def Q2Presentation.Induction.MinimalBlockPushoutRoute83Closers.MinimalBlockPreheadPushoutRoute83Data.toRoute82Naturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute83Data D) : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingNaturalityDataRoute82 P.toRoute82Pairing

Route83 naturality projected to the Route82 naturality packet.

The statement is for the Phi coming from P, not for an arbitrary external pairing family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute83Closers.MinimalBlockPreheadPushoutRoute83Data.toRoute82Annihilation {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute83Data D) : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82 P.toRoute82Pairing

Route83 diagonal and polar vanishing projected to Route82 annihilation.

This uses the already-proved extraspecial square-map API: the square of the scalar pushout is Extraspecial.extraspecialForm (phi lambda), so the two semantic vanishing statements give Annihilates for the extraspecial square.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute83Closers.MinimalBlockPreheadPushoutRoute83Data.toRoute82DescendedNonsingular {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute83Data D) : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutDescendedNonsingularDataRoute82 P.toRoute82Pairing ⋯

Route83 radical containment projected to Route82 descended nonsingularity.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute83Closers.MinimalBlockPreheadPushoutRoute83Data.toRoute82 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute83Data D) : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadPushoutRoute82Data D

Route83 projected to the coherent Route82 packet.

Equations

• P.toRoute82 = { pairing := P.toRoute82Pairing, naturality := ⋯, annihilation := ⋯, nonsingular := ⋯ }

def Q2Presentation.Induction.MinimalBlockPushoutRoute83Closers.MinimalBlockPreheadPushoutRoute83Data.toPushoutRouteLower {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadPushoutRoute83Data D) : MinimalBlockPreheadPushoutRouteLowerData D

Route83 projected directly to the lower pushout packet consumed downstream.

Equations

• P.toPushoutRouteLower = P.toRoute82.toRoute81.toPushoutRouteLower

Constructors and drop-in provider

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute83Closers.minimalBlock_preheadPushoutRoute83Data_from_actualScalarAndCoherentDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadPushoutRoute83Data D)

Assemble Route83 from existing finer manuscript-shaped packets.

The actual scalar pushout is obtained from the standard same-family square/polar proof hooks; the simple-head determinant part is the coherent semantic prop:simpleheaddet packet for the same induced semantic family. This theorem therefore avoids the four Route82 residual axioms.

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute83Closers.minimalBlock_preheadPushoutRoute82Data_from_route83 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadPushoutRoute82Data D)

Projection from the Route83 coherent actual-scalar packet to the old Route82 coherent packet.

This is the promised projection to the old packet shape. It does not call the Route82 split-packet provider and does not use Route82's four residual axioms.

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

Route83 lower pushout packet, avoiding the Route82 residual providers.

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

Drop-in determinant-packet replacement for Route82.

Compared with Route82, the axiom closure replaces

• minimalBlock_preheadCentralPushoutPairingConstructionData_route82,
• minimalBlock_preheadCentralPushoutPairingNaturalityData_route82,
• minimalBlock_preheadCentralPushoutAnnihilationData_route82, and
• minimalBlock_preheadCentralPushoutDescendedNonsingularData_route82

by the finer existing standard square/polar scalar-pushout packets and the four same-family semantic simple-head determinant packets.