Route60 minimal-block pushout/determinant closers

Route58 normalized the actual central-extension square to the extraspecial square attached to phi_lambda, removing the square, diagonal, and polar residuals from the final Section 7 pushout cluster. The final route still sees four non-local packets:

• minimalBlock_preheadActualCentralExtensionPhiData;
• minimalBlock_preheadActualCentralExtensionNaturalityData;
• minimalBlock_preheadActualCentralExtensionAnnihilationData;
• minimalBlock_preheadActualCentralExtensionRadicalContainmentData.

This Route60 sidecar does not integrate a new final route. It exports a drop-in Route58-shaped provider whose closure replaces those four packet names by lower-level manuscript-shaped obligations from §7:

• construction of the scalar pushout pairing family for K_lambda = K / ker lambda;
• conjugation naturality of that pairing;
• vanishing of the diagonal square on T;
• vanishing of the polar form on T x M;
• containment of the symmetrized polar radical in T.

The assembly from those packets to Route58 data is theorem-level: annihilation is extraspecial_annihilates, and radical containment is extraspecial_radical_subset.

Route60 lower-level §7 packets

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

Route60 lower-level packet for the actual scalar pushout pairing family.

Manuscript anchor: §7, K_lambda = K / ker lambda, where the commutator pairing of the central double cover gives the self-duality map phi_lambda. This packet records only that pairing family; the square and determinant conclusions are supplied separately below.

• phi : Module.Dual (ZMod 2) D.R → D.M →ₗ[ZMod 2] Module.Dual (ZMod 2) D.M

structure Q2Presentation.Induction.MinimalBlockRoute60PairingNaturalityData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockRoute60ScalarPushoutPairingData D) : Prop

Route60 lower-level packet for conjugation naturality of the actual phi_lambda family.

• phi_natural (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (c : D.C) (m m' : D.M), ((F.phi lam) ((D.actM c) m)) ((D.actM c) m') = ((F.phi lam) m) m'

structure Q2Presentation.Induction.MinimalBlockRoute60DiagonalVanishingOnTData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockRoute60ScalarPushoutPairingData D) : Prop

Route60 lower-level packet for the first half of prop:simpleheaddet: the scalar pushout square vanishes on T.

Since Route58 fixes the square to Extraspecial.extraspecialForm phi_lambda, this is the diagonal identity phi_lambda(t,t)=0 on T.

• diagonal_zero_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ t ∈ D.T, ((F.phi lam) t) t = 0

structure Q2Presentation.Induction.MinimalBlockRoute60PolarVanishingOnTData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockRoute60ScalarPushoutPairingData D) : Prop

Route60 lower-level packet for the second half of prop:simpleheaddet: b_lambda(T,M)=0.

For the Route58 extraspecial square this is the symmetrized-pairing statement phi_lambda(t,m)+phi_lambda(m,t)=0.

• symm_polar_zero_on_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ t ∈ D.T, ∀ (m : D.M), ((F.phi lam) t) m + ((F.phi lam) m) t = 0

structure Q2Presentation.Induction.MinimalBlockRoute60PolarRadicalContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockRoute60ScalarPushoutPairingData D) : Prop

Route60 lower-level packet for the radical-containment step of prop:simpleheaddet: the polar radical of the symmetrized pushout pairing is contained in T.

• symm_polar_radical_subset_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (m : D.M), (∀ (m' : D.M), ((F.phi lam) m) m' + ((F.phi lam) m') m = 0) → m ∈ D.T

New lower-level residual hooks

axiom Q2Presentation.Induction.minimalBlock_route60ScalarPushoutPairingData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockRoute60ScalarPushoutPairingData D)

Construct the actual scalar pushout pairing family phi_lambda for K_lambda = K / ker lambda.

axiom Q2Presentation.Induction.minimalBlock_route60PairingNaturalityData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockRoute60ScalarPushoutPairingData D) : Nonempty (MinimalBlockRoute60PairingNaturalityData F)

Prove conjugation naturality for the actual Route60 scalar pushout pairing.

axiom Q2Presentation.Induction.minimalBlock_route60DiagonalVanishingOnTData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockRoute60ScalarPushoutPairingData D) : Nonempty (MinimalBlockRoute60DiagonalVanishingOnTData F)

Prove q_lambda|_T = 0, expressed as diagonal vanishing for the Route58 extraspecial square.

axiom Q2Presentation.Induction.minimalBlock_route60PolarVanishingOnTData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockRoute60ScalarPushoutPairingData D) : Nonempty (MinimalBlockRoute60PolarVanishingOnTData F)

Prove b_lambda(T,M)=0, expressed as symmetrized-pairing vanishing for the Route58 extraspecial square.

axiom Q2Presentation.Induction.minimalBlock_route60PolarRadicalContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockRoute60ScalarPushoutPairingData D) : Nonempty (MinimalBlockRoute60PolarRadicalContainmentData F)

Prove that the polar radical of the actual scalar pushout pairing is contained in T.

Theorem-level projections to the current actual central-extension API

def Q2Presentation.Induction.MinimalBlockRoute60ScalarPushoutPairingData.toActualPhi {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockRoute60ScalarPushoutPairingData D) : MinimalBlockPreheadActualCentralExtensionPhiData D

Project the Route60 scalar pushout pairing to the current PhiData packet.

Equations

• F.toActualPhi = { phi := F.phi }

def Q2Presentation.Induction.MinimalBlockRoute60ScalarPushoutPairingData.toActualSquare {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockRoute60ScalarPushoutPairingData D) : MinimalBlockPreheadActualCentralExtensionSquareData F.toActualPhi

The Route58-normalized square attached to the Route60 pairing family.

Equations

• F.toActualSquare = Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi F.toActualPhi

def Q2Presentation.Induction.MinimalBlockRoute60PairingNaturalityData.toActualNaturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockRoute60ScalarPushoutPairingData D} (N : MinimalBlockRoute60PairingNaturalityData F) : MinimalBlockPreheadActualCentralExtensionNaturalityData F.toActualPhi

Project Route60 pairing naturality to the current actual central-extension naturality packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.minimalBlock_route60ActualAnnihilationData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockRoute60ScalarPushoutPairingData D} (Diag : MinimalBlockRoute60DiagonalVanishingOnTData F) (Polar : MinimalBlockRoute60PolarVanishingOnTData F) : MinimalBlockPreheadActualCentralExtensionAnnihilationData F.toActualSquare

Route60 theorem-level construction of actual central-extension annihilation from the two manuscript halves q_lambda|_T=0 and b_lambda(T,M)=0.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.minimalBlock_route60ActualRadicalContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockRoute60ScalarPushoutPairingData D} (Rad : MinimalBlockRoute60PolarRadicalContainmentData F) : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData F.toActualSquare

Route60 theorem-level construction of actual central-extension polar-radical containment from the symmetrized-pairing radical statement.

Equations

• ⋯ = ⋯

Route60 same-family packet and Route58-compatible providers

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

Route60 packet: the actual scalar pushout pairing together with the three simple-head determinant ingredients needed after Route58 normalization.

This is lower than MinimalBlockPushoutRoute58Data: it does not store current PhiData, NaturalityData, AnnihilationData, or RadicalContainmentData; those are theorem-level projections.

• family : MinimalBlockRoute60ScalarPushoutPairingData D
• naturality : MinimalBlockRoute60PairingNaturalityData self.family
• diagonalT : MinimalBlockRoute60DiagonalVanishingOnTData self.family
• polarT : MinimalBlockRoute60PolarVanishingOnTData self.family
• radical : MinimalBlockRoute60PolarRadicalContainmentData self.family

def Q2Presentation.Induction.MinimalBlockPushoutRoute60Data.phi {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute60Data D) : MinimalBlockPreheadActualCentralExtensionPhiData D

Current actual PhiData projected from Route60.

Equations

• P.phi = P.family.toActualPhi

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

Route58-normalized actual square projected from Route60.

Equations

• P.square = P.family.toActualSquare

def Q2Presentation.Induction.MinimalBlockPushoutRoute60Data.actualNaturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute60Data D) : MinimalBlockPreheadActualCentralExtensionNaturalityData P.phi

Current actual naturality projected from Route60.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute60Data.actualAnnihilation {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute60Data D) : MinimalBlockPreheadActualCentralExtensionAnnihilationData P.square

Current actual annihilation projected from Route60.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute60Data.actualRadical {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute60Data D) : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData P.square

Current actual polar-radical containment projected from Route60.

Equations

• ⋯ = ⋯

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

Project Route60 to the Route58 normalized packet shape.

Equations

• P.toRoute58Data = { phi := P.phi, naturality := ⋯, annihilation := ⋯, radical := ⋯ }

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

Reassemble the broad actual central-extension pushout packet from Route60.

Equations

• P.actualPushout = P.toRoute58Data.actualPushout

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

Route60 projected to the Route54 coherent actual determinant packet.

Equations

• P.toRoute54Data = P.toRoute58Data.toRoute54Data

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

Route60 projected to the Route53 determinant packet shape.

Equations

• P.toRoute53Data = P.toRoute58Data.toRoute53Data

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

Route60 projected to the Route52 determinant packet shape.

Equations

• P.toRoute52Data = P.toRoute58Data.toRoute52Data

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

Route60 projected to the Route50 determinant packet shape.

Equations

• P.toRoute50Data = P.toRoute58Data.toRoute50Data

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

Route60 projected to the lower pushout packet consumed by integration.

Equations

• P.toPushoutRouteLowerData = P.toRoute58Data.toPushoutRouteLowerData

Route-compatible hooks

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

Construct Route60 data from the five lower-level §7 determinant-pushout packets.

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

Route58-shaped data supplied by Route60. Its axiom closure avoids the four Route58 residual names and exposes the lower-level Route60 packets instead.

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

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

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

Route60 replacement for Route54's coherent actual determinant packet.

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

Route53-shaped determinant data supplied by Route60.

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

Route52-shaped determinant data supplied by Route60.

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

Route50-shaped determinant data supplied by Route60.

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

Lower pushout route supplied by Route60.

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

Determinant-packet provider supplied by Route60.

This has the same consumed surface as the Route58 provider, but its nonstandard closure replaces the four remaining actual central-extension residuals by the five lower-level Route60 packets above.

theorem Q2Presentation.Induction.minimalBlock_preheadDeterminantPackets_from_route58_via_route60 {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 Route58 provider surface.

Acceptance checks / exact residual report