Route161 Section 7 pushout/determinant lowering

Route160's current pushout/determinant frontier is the seven split actual central-extension packets from MinimalBlockActualCentralExtensionPushoutProofs:

• minimalBlock_preheadActualCentralExtensionPhiData;
• minimalBlock_preheadActualCentralExtensionSquareData;
• minimalBlock_preheadActualCentralExtensionDiagonalData;
• minimalBlock_preheadActualCentralExtensionPolarData;
• minimalBlock_preheadActualCentralExtensionNaturalityData;
• minimalBlock_preheadActualCentralExtensionAnnihilationData;
• minimalBlock_preheadActualCentralExtensionRadicalContainmentData.

This sidecar lowers that seven-packet frontier to two same-family manuscript atoms:

• the scalar central-pushout self-duality family phi_lambda;
• the simple-head determinant packet for the extraspecial square Quadratic.Extraspecial.extraspecialForm (phi_lambda).

The bridge does not call Route82 and does not route through the old minimalBlock_preheadCentralPushoutSemanticData leaf. The square, diagonal, and polar actual central-extension packets are definitional from Extraspecial.extraspecialForm; naturality, annihilation, and radical containment are projections of prop:simpleheaddet.

Manuscript anchors: Section 6 constructs the determinant obstruction of scalar central pushouts, and Section 7, prop:simpleheaddet, proves q_lambda|_T = 0, b_lambda(T,M) = 0, and the descended nonsingular radical statement for K_lambda = K / ker lambda.

Two-atom Route161 packet

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

Route161 coherent Section 7 determinant packet.

The determinant field is indexed by the extraspecial family induced from the same self-duality packet, so all actual central-extension projections use one phi_lambda family.

• selfDuality : MinimalBlockPreheadCentralPushoutSelfDualityData D
• simpleHeadDeterminant : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData (MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality self.selfDuality)

def Q2Presentation.Induction.Section7PushoutRoute161Closers.MinimalBlockPushoutRoute161SimpleHeadDeterminantData.phiData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute161SimpleHeadDeterminantData D) : MinimalBlockPreheadActualCentralExtensionPhiData D

The actual central-extension pairing packet selected by Route161.

Equations

• P.phiData = { phi := P.selfDuality.phi }

def Q2Presentation.Induction.Section7PushoutRoute161Closers.MinimalBlockPushoutRoute161SimpleHeadDeterminantData.squareData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute161SimpleHeadDeterminantData D) : MinimalBlockPreheadActualCentralExtensionSquareData P.phiData

The actual square-map packet is the extraspecial square of the selected pairing.

Equations

• P.squareData = { square := fun (lam : Module.Dual (ZMod 2) D.R) => Q2Presentation.Quadratic.Extraspecial.extraspecialForm (P.selfDuality.phi lam) }

def Q2Presentation.Induction.Section7PushoutRoute161Closers.MinimalBlockPushoutRoute161SimpleHeadDeterminantData.diagonalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute161SimpleHeadDeterminantData D) : MinimalBlockPreheadActualCentralExtensionDiagonalData P.squareData

Diagonal identity for the selected extraspecial square.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7PushoutRoute161Closers.MinimalBlockPushoutRoute161SimpleHeadDeterminantData.polarData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute161SimpleHeadDeterminantData D) : MinimalBlockPreheadActualCentralExtensionPolarData P.squareData

Polar identity for the selected extraspecial square.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7PushoutRoute161Closers.MinimalBlockPushoutRoute161SimpleHeadDeterminantData.naturalityData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute161SimpleHeadDeterminantData D) : MinimalBlockPreheadActualCentralExtensionNaturalityData P.phiData

Actual central-extension naturality from the simple-head determinant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7PushoutRoute161Closers.MinimalBlockPushoutRoute161SimpleHeadDeterminantData.annihilationData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute161SimpleHeadDeterminantData D) : MinimalBlockPreheadActualCentralExtensionAnnihilationData P.squareData

Actual central-extension annihilation on T from prop:simpleheaddet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7PushoutRoute161Closers.MinimalBlockPushoutRoute161SimpleHeadDeterminantData.radicalContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute161SimpleHeadDeterminantData D) : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData P.squareData

Actual central-extension radical containment from prop:simpleheaddet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.Section7PushoutRoute161Closers.MinimalBlockPushoutRoute161SimpleHeadDeterminantData.actualCentralExtensionPushoutData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute161SimpleHeadDeterminantData D) : MinimalBlockPreheadActualCentralExtensionPushoutData D

Reassembled actual central-extension pushout packet.

Equations

• P.actualCentralExtensionPushoutData = Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPushoutData.ofSplitPackets P.phiData P.squareData ⋯ ⋯ ⋯ ⋯ ⋯

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

Route-lower packet projected directly from the same two Route161 atoms.

Equations

• P.toPushoutRouteLower = { selfDuality := P.selfDuality, simpleHeadDeterminant := ⋯ }

theorem Q2Presentation.Induction.Section7PushoutRoute161Closers.minimalBlock_pushoutRoute161SimpleHeadDeterminantData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPushoutRoute161SimpleHeadDeterminantData D)

Construct the Route161 coherent determinant packet.

This is the new residual source: its axiom closure is the self-duality packet plus the coherent simple-head determinant packet, not the seven Route160 actual central-extension leaves.

Actual central-extension bridge

theorem Q2Presentation.Induction.Section7PushoutRoute161Closers.minimalBlock_preheadActualCentralExtensionPackets_from_section7PushoutRoute161Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (P : MinimalBlockPushoutRoute161SimpleHeadDeterminantData D), Nonempty (MinimalBlockPreheadActualCentralExtensionPhiData D) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionSquareData P.phiData) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionDiagonalData P.squareData) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionPolarData P.squareData) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionNaturalityData P.phiData) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionAnnihilationData P.squareData) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionRadicalContainmentData P.squareData)

Aggregate bridge for the seven Route160 actual central-extension packet targets, tied to one Route161 phi_lambda and one extraspecial square family.

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

Route-ready replacement for the broad actual central-extension pushout packet using the two Route161 atoms.

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

Supervisor hook: lower pushout route from the Route161 coherent packet.

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

Drop-in replacement for Section7PushoutRoute157Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute157Closers.

The statement has the same consumer shape as the Route157 provider, but its axiom frontier replaces the seven Route160 actual central-extension leaves by Route161's two coherent manuscript atoms.

Acceptance checks / exact residual report