Section 7 determinant semantic packet projections

This sidecar closes the four central-pushout semantic determinant packets from the narrower actual simple-head determinant packet for the same semantic family S.

The target packets are:

• minimalBlock_preheadCentralPushoutNaturalitySemanticData;
• minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData;
• minimalBlock_preheadCentralPushoutPolarZeroSemanticData;
• minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData.

The proof does not call those four axioms. It projects them from minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData S, whose fields are exactly the same-family prop:simpleheaddet assertions for S.toQuadraticFamily.square.

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutNaturalitySemanticData.ofActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (P : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S) : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S

Project semantic naturality from the actual determinant packet for the same central-pushout family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData.ofActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (P : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S) : MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S

Project diagonal vanishing on T from annihilation of the actual extraspecial square map for the same central-pushout family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutPolarZeroSemanticData.ofActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (P : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S) : MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S

Project polar vanishing on T x M from annihilation of the actual extraspecial square map for the same central-pushout family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData.ofActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (P : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S) : MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S

Project polar-radical containment from the actual determinant packet for the same central-pushout family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutCoherentDeterminantSemanticData.ofActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (P : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S) : MinimalBlockPreheadCentralPushoutCoherentDeterminantSemanticData S

Repackage the actual same-family determinant packet as the coherent semantic determinant packet.

Equations

• ⋯ = ⋯

Proven projection theorems for the four requested semantic packets

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutCoherentDeterminantSemanticData_proven {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutCoherentDeterminantSemanticData S)

Coherent determinant semantic packet, proven from the narrower actual simple-head determinant packet for the same S.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutNaturalitySemanticData_proven {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData S)

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData_proven {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S)

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutPolarZeroSemanticData_proven {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S)

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData_proven {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S)

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSemanticDeterminantPackets_proven {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S)

All four semantic determinant packets, tied to the same actual central-pushout family and proved from the actual simple-head determinant packet.

Route-ready count theorem avoiding the four semantic packet axioms

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

Lower pushout route through the actual determinant packet for the semantic central-pushout family. Its closure avoids the four semantic determinant packet axioms targeted in this file.

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

Determinant packet projection through MinimalBlockDeterminantPacketProofs2.

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

Nonterminal Fourier branch with the determinant side routed through the actual simple-head determinant packet rather than the four semantic packet axioms.

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

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

Route-ready finite-surjection equality whose determinant side avoids the four semantic determinant packet axioms targeted by this sidecar.

Alternate final theorem for axiom-closure auditing

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

Equal finite surjection counts with the redundant [Nonempty G] discharged, using the determinant-packet-proof route from this sidecar.

theorem Q2Presentation.Induction.presentation_correct_determinantPacketProofs2 : Nonempty (GammaA ≅ GQ2Profinite)

Alternate capstone theorem using the determinant-packet-proof finite-count route, for direct final-closure auditing.