Proof-data route for Section 7 semantic minimal-block packets

This sidecar keeps routed files untouched. It records the useful next de-axiomatization boundary for the Section 7 semantic packets:

• one realized group tower R = Phi(K) <= K <= L_Y, carrying the actual M = K/R, T, C, induced actions, simple-head facts, and invariant determinant character;
• one central-pushout/extraspecial determinant family over the pre-head tower, with naturality, diagonal zero, polar zero, and radical containment tied to that same family.

The theorem-level route below does not call the nine current semantic packet axioms. A coordinator can use it by supplying a single provider for MinimalBlockSemanticProofData, then reuse the existing Section 8 cover route.

One proof object for the Section 7 semantic packets

structure Q2Presentation.Induction.MinimalBlockSemanticProofData (p : FramedPair) (chief : NonScalarChiefFactor p) : Type 1

A single manuscript-shaped proof object for the Section 7 minimal block.

The groupTower field is the actual subgroup tower: it contains K, R, R = Phi(K), K <= L_Y, the K/R module bridge, the induced C-actions, and the simple-head/character facts. The determinant fields are all tied to one central-pushout self-duality family over that tower's pre-head data.

• groupTower : MinimalBlockGroupTowerData p chief
• centralPushout : MinimalBlockPreheadCentralPushoutSemanticData self.groupTower.preheadTowerData
• naturality : MinimalBlockPreheadCentralPushoutNaturalitySemanticData self.centralPushout
• diagonalZero : MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData self.centralPushout
• polarZero : MinimalBlockPreheadCentralPushoutPolarZeroSemanticData self.centralPushout
• radicalContainment : MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData self.centralPushout

@[reducible, inline]

abbrev Q2Presentation.Induction.MinimalBlockSemanticProofData.preheadTower {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : MinimalBlockPreheadTowerData p chief

The pre-head tower R, M, T, C extracted from the realized group tower.

Equations

• D.preheadTower = D.groupTower.preheadTowerData

Projections to the four subgroup-tower semantic packets

def Q2Presentation.Induction.MinimalBlockSemanticProofData.kernelChoice {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : MinimalBlockKernelChoiceSemanticData p chief

The selected minimal subgroup K, projected from the realized group tower.

Equations

• D.kernelChoice = { Ksub := D.groupTower.Ksub, Ksub_normal := ⋯, Ksub_le_upper := ⋯, Ksub_le_LY := ⋯, KS_eq_upper := ⋯, minimal_K := ⋯ }

def Q2Presentation.Induction.MinimalBlockSemanticProofData.frattiniKernel {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : MinimalBlockFrattiniKernelSemanticData D.kernelChoice

The Frattini subgroup R = Phi(K), projected from the realized group tower.

Equations

• D.frattiniKernel = { Rsub := D.groupTower.Rsub, Rsub_normal := ⋯, Rsub_le_Ksub := ⋯, Rsub_card_gt_one := ⋯, Rsub_eq_frattini := ⋯ }

def Q2Presentation.Induction.MinimalBlockSemanticProofData.moduleExtraction {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : MinimalBlockModuleExtractionSemanticData D.kernelChoice D.frattiniKernel

The module/action extraction M = K/R, T, C, and induced actions.

Equations

• D.moduleExtraction = { rawModuleData := D.groupTower.rawModuleData, rawActionData := D.groupTower.rawActionData, KmodR_equiv_rawM := D.groupTower.KmodR_equiv_rawM }

def Q2Presentation.Induction.MinimalBlockSemanticProofData.simpleHead {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : MinimalBlockSimpleHeadSemanticData D.moduleExtraction

The simple-head, dual-invariant, and raw determinant-character consequences.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockSemanticProofData.groupTowerViaSemanticPackets {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : MinimalBlockGroupTowerData p chief

Reassemble the current MinimalBlockGroupTowerData packet from the semantic projections. This is definitionally the same manuscript data, but routed through the semantic packet boundary.

Equations

• D.groupTowerViaSemanticPackets = Q2Presentation.Induction.MinimalBlockGroupTowerData.ofSemantic D.kernelChoice D.frattiniKernel D.moduleExtraction ⋯

theorem Q2Presentation.Induction.MinimalBlockSemanticProofData.kernelChoiceSemanticData_closed {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : Nonempty (MinimalBlockKernelChoiceSemanticData p chief)

Closure of the selected K packet from one proof object.

theorem Q2Presentation.Induction.MinimalBlockSemanticProofData.frattiniKernelSemanticData_closed {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : Nonempty (MinimalBlockFrattiniKernelSemanticData D.kernelChoice)

Closure of the selected R = Phi(K) packet from one proof object.

theorem Q2Presentation.Induction.MinimalBlockSemanticProofData.moduleExtractionSemanticData_closed {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : Nonempty (MinimalBlockModuleExtractionSemanticData D.kernelChoice D.frattiniKernel)

Closure of the selected module/action extraction packet from one proof object.

theorem Q2Presentation.Induction.MinimalBlockSemanticProofData.simpleHeadSemanticData_closed {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : Nonempty (MinimalBlockSimpleHeadSemanticData D.moduleExtraction)

Closure of the selected simple-head packet from one proof object.

Projections to the determinant semantic packets

def Q2Presentation.Induction.MinimalBlockSemanticProofData.quadraticFamily {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D.preheadTower

The central-pushout square family as an extraspecial form from the same phi.

Equations

• D.quadraticFamily = D.centralPushout.toQuadraticFamily

def Q2Presentation.Induction.MinimalBlockSemanticProofData.equivariantFamily {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : MinimalBlockPreheadExtraspecialEquivariantFamilyData D.preheadTower

The equivariant extraspecial family induced by central-pushout naturality.

Equations

• D.equivariantFamily = ⋯.toEquivariantFamily

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

The annihilation packet, assembled from diagonal and polar zero on the same central-pushout family.

Equations

• ⋯ = ⋯

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

The radical packet, assembled from radical containment for the same family.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.MinimalBlockSemanticProofData.preheadCentralPushoutSemanticData_closed {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : Nonempty (MinimalBlockPreheadCentralPushoutSemanticData D.preheadTower)

The central-pushout semantic packet, tied to the proof object's pre-head tower.

theorem Q2Presentation.Induction.MinimalBlockSemanticProofData.preheadCentralPushoutNaturalitySemanticData_closed {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData D.centralPushout)

The central-pushout naturality packet, tied to the same family.

theorem Q2Presentation.Induction.MinimalBlockSemanticProofData.preheadCentralPushoutDiagonalZeroSemanticData_closed {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData D.centralPushout)

The diagonal-zero packet, tied to the same family.

theorem Q2Presentation.Induction.MinimalBlockSemanticProofData.preheadCentralPushoutPolarZeroSemanticData_closed {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData D.centralPushout)

The polar-zero packet, tied to the same family.

theorem Q2Presentation.Induction.MinimalBlockSemanticProofData.preheadCentralPushoutRadicalContainmentSemanticData_closed {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) : Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData D.centralPushout)

The radical-containment packet, tied to the same family.

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

Reassemble the determinant packets consumed by MinimalBlockGroupTowerData.toMinimalBlock.

Minimal-block and Fourier routes parameterized by one provider

def Q2Presentation.Induction.MinimalBlockSemanticProofData.toMinimalBlock {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockSemanticProofData p chief) (h : ¬ScalarTerminal p) : MinimalBlock p

Build the strengthened MinimalBlock from one semantic proof object.

Equations

• D.toMinimalBlock h = D.groupTower.toMinimalBlock h D.equivariantFamily ⋯ ⋯

theorem Q2Presentation.Induction.minimalBlock_of_nonScalar_from_semanticProofData {p : FramedPair} {chief : NonScalarChiefFactor p} (h : ¬ScalarTerminal p) (D : MinimalBlockSemanticProofData p chief) : Nonempty (MinimalBlock p)

Minimal-block closure from one explicit semantic proof object.

This theorem has no dependency on the nine current semantic packet axioms; those constructors are replaced by the single explicit argument D.

theorem Q2Presentation.Induction.minimalBlock_of_nonScalar_from_semanticProofProvider (p : FramedPair) (provide : ∀ (chief : NonScalarChiefFactor p), Nonempty (MinimalBlockSemanticProofData p chief)) : ¬ScalarTerminal p → Nonempty (MinimalBlock p)

Minimal-block closure from a provider of proof objects for non-scalar chief factors. This is the coordinator-facing replacement boundary for Section 7.

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_from_semanticProofProvider (p : FramedPair) (provide : ∀ (chief : NonScalarChiefFactor p), Nonempty (MinimalBlockSemanticProofData p chief)) (realize : ∀ (chief : NonScalarChiefFactor p) (D : MinimalBlockSemanticProofData p chief) (h : ¬ScalarTerminal p), Nonempty (CoverRealization (D.toMinimalBlock h))) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

Nonterminal Fourier branch from the Section 7 proof provider and an external Section 8 cover-realization provider.

This is intentionally parameterized over cover realization: the sidecar's scope is Section 7 semantic de-axiomatization, not the Section 8 central-cover route.