Route50 minimal-block pushout/determinant narrowing

Route49 exposes one determinant leaf:

• minimalBlock_preheadDeterminantRoute49Data.

That packet is exactly the data consumed by the nonterminal Fourier branch: one equivariant extraspecial family, annihilation on T, and polar-radical containment. This Route50 sidecar keeps the same consumed surface but replaces the opaque Route49 leaf by a single manuscript-shaped simple-head determinant packet for one bare extraspecial family.

Manuscript anchor: Section 7, prop:simpleheaddet. The Route50 packet records one family phi_lambda together with the simple-head determinant theorem for the extraspecial square form attached to that same family. The Route49-consumed annihilation and radical packets are theorem-level projections from it.

Route50 packet

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

Route50 determinant packet over a pre-head tower.

This is a one-leaf replacement for Route49's aggregate determinant leaf. It is more semantic than the Route49 data: the equivariance, annihilation, and radical conclusions all come from one simple-head determinant theorem for the extraspecial square form attached to the same bare family.

• family : MinimalBlockPreheadExtraspecialFamilyData D
• simpleHeadDeterminant : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData self.family

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

The equivariant family projected from the same simple-head determinant packet.

Equations

• P.equivariantFamily = ⋯.toEquivariantFamily

def Q2Presentation.Induction.MinimalBlockPreheadSimpleHeadDeterminantRoute50Data.annihilationData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadSimpleHeadDeterminantRoute50Data D) : MinimalBlockPreheadExtraspecialAnnihilationData P.equivariantFamily

Route49-consumed annihilation data projected from the same simple-head determinant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadSimpleHeadDeterminantRoute50Data.radicalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadSimpleHeadDeterminantRoute50Data D) : MinimalBlockPreheadExtraspecialRadicalData P.equivariantFamily

Route49-consumed radical data projected from the same simple-head determinant packet.

Equations

• ⋯ = ⋯

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

Forget Route50's semantic provenance to the Route49 packet shape.

Equations

• P.toRoute49Data = { equivariantFamily := P.equivariantFamily, annihilationData := ⋯, radicalData := ⋯ }

Route-compatible hooks

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

Route50's single determinant residual.

This is intentionally not the seven actual-central-extension split packet route: it is the simple-head determinant theorem for one extraspecial family, exactly the Section 7 statement from which the consumed annihilation/radical packets are projected.

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

Route50 proves the old Route49 data shape without using the Route49 determinant axiom.

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

Route50 determinant-packet projection consumed by the integrated nonterminal branch.

Integrated Route50 sidecar

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_currentIntegrated50 (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

Route49-shaped nonterminal branch with the determinant side supplied by Route50's simple-head determinant packet.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated50 (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_currentIntegrated50 (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_currentIntegrated50 (p : FramedPair) : framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_currentIntegrated50 (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Route50 finite-surjection equality. This is the exported theorem for axiom closure auditing.