Route67 minimal-block determinant/pushout closer

Route66 still consumes minimalBlock_preheadDeterminantPackets_from_route63. Its axiom closure exposes the seven standard Section 7 determinant/pushout packets:

• minimalBlock_preheadCentralPushoutQuadraticFamilyData;
• minimalBlock_preheadCentralPushoutSquareDiagonalData;
• minimalBlock_preheadCentralPushoutPolarSymmData;
• minimalBlock_preheadExtraspecialNaturalityData;
• minimalBlock_preheadExtraspecialDiagonalZeroData;
• minimalBlock_preheadExtraspecialPolarZeroData;
• minimalBlock_preheadExtraspecialRadicalContainmentData.

This sidecar replaces those seven independent packet boundaries by two manuscript-shaped boundaries:

• minimalBlock_preheadActualScalarCentralPushoutData, the actual scalar central-pushout construction K_lambda = K / ker lambda with its square map;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData, the prop:simpleheaddet packet for that same actual semantic central-pushout family.

The exported provider minimalBlock_preheadDeterminantPackets_from_route67 has the same downstream surface as the Route63 provider and can be used as a drop-in replacement.

Route67 determinant provider

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

Route67's coherent Route50-shaped determinant packet.

The scalar pushout family is supplied by the actual scalar central-pushout packet. The simple-head determinant theorem is then applied to the semantic family obtained by forgetting only the explicit quotient witnesses and retaining the same phi_lambda.

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

Drop-in determinant-packet replacement for minimalBlock_preheadDeterminantPackets_from_route63.

Its closure lowers the seven Route66 minimal-block determinant/pushout atoms to the actual scalar pushout construction and the same-family actual prop:simpleheaddet packet.

Pushout Route67 audit theorem

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

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_pushoutRoute67 (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_pushoutRoute67 (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_pushoutRoute67 (p : FramedPair) : framedCountA p = framedCountQ p

theorem Q2Presentation.Induction.finite_surjection_counts_equal_pushoutRoute67 (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)))