Semantic Section 7 minimal-block closers

This sidecar refines the Section 7 minimal-block residuals without changing any existing routed file. It replaces the broad group-tower and determinant-pushout residual names by manuscript-shaped semantic packets:

• a selected minimal subgroup K;
• its Frattini layer R = Phi(K);
• the extraction of M = K/R, T, C, and the induced actions;
• the simple-head/character consequences attached to that same extraction;
• one central-pushout extraspecial square family, with naturality, diagonal vanishing, polar vanishing, and radical containment all tied to that same family.

The final theorems below are intended as drop-in routing targets for the coordinator. They do not use the existing residual axioms minimalBlock_groupTowerData, minimalBlock_preheadCentralPushoutQuadraticFamilyData, minimalBlock_preheadCentralPushoutSquareDiagonalData, minimalBlock_preheadCentralPushoutPolarSymmData, minimalBlock_preheadExtraspecialNaturalityData, minimalBlock_preheadExtraspecialDiagonalZeroData, minimalBlock_preheadExtraspecialPolarZeroData, or minimalBlock_preheadExtraspecialRadicalContainmentData.

Semantic subgroup tower packets

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

The Section 7 minimal normal subgroup K <= P <= L_Y, selected with KS = P and minimality among Y-normal subgroups with that property.

• Ksub : Subgroup p.fst.Y
• Ksub_normal : self.Ksub.Normal
• Ksub_le_upper : self.Ksub ≤ chief.upper
• Ksub_le_LY : self.Ksub ≤ p.fst.LY
• KS_eq_upper : self.Ksub ⊔ chief.lower = chief.upper
• minimal_K (K' : Subgroup p.fst.Y) : K'.Normal → K' ≤ chief.upper → K' ⊔ chief.lower = chief.upper → self.Ksub ≤ K'

structure Q2Presentation.Induction.MinimalBlockFrattiniKernelSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelChoiceSemanticData p chief) : Type

The Frattini layer R = Phi(K) supplied by the collapse lemma.

• Rsub : Subgroup p.fst.Y
• Rsub_normal : self.Rsub.Normal
• Rsub_le_Ksub : self.Rsub ≤ K.Ksub
• Rsub_card_gt_one : 1 < Nat.card ↥self.Rsub
• Rsub_eq_frattini : self.Rsub = Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub)

structure Q2Presentation.Induction.MinimalBlockModuleExtractionSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelChoiceSemanticData p chief) (R : MinimalBlockFrattiniKernelSemanticData K) : Type 1

The module/action extraction from the same subgroup tower: R, M = K/R, T, C, and the induced C-actions.

• rawModuleData : MinimalBlockRawModuleData p chief
• rawActionData : MinimalBlockRawActionData self.rawModuleData
• KmodR_equiv_rawM : ↥(Subgroup.map (QuotientGroup.mk' R.Rsub) K.Ksub) ≃* Multiplicative self.rawModuleData.M

def Q2Presentation.Induction.MinimalBlockModuleExtractionSemanticData.rawTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelChoiceSemanticData p chief} {R : MinimalBlockFrattiniKernelSemanticData K} (E : MinimalBlockModuleExtractionSemanticData K R) : MinimalBlockRawTowerData p chief

The raw pre-head tower extracted from K, R, M, T, and C.

Equations

• E.rawTowerData = Q2Presentation.Induction.MinimalBlockRawTowerData.ofModuleAction E.rawModuleData E.rawActionData

structure Q2Presentation.Induction.MinimalBlockSimpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelChoiceSemanticData p chief} {R : MinimalBlockFrattiniKernelSemanticData K} (E : MinimalBlockModuleExtractionSemanticData K R) : Prop

The simple-head and determinant-character consequences of the same tower.

• headNontrivialData : MinimalBlockHeadNontrivialData E.rawTowerData
• dualInvariantData : MinimalBlockDualInvariantVanishesData E.rawTowerData
• rawInvariantCharacterData : MinimalBlockRawInvariantCharacterData E.rawTowerData

axiom Q2Presentation.Induction.minimalBlock_kernelChoiceSemanticData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelChoiceSemanticData p chief)

Semantic residual: choose the minimal subgroup K.

axiom Q2Presentation.Induction.minimalBlock_frattiniKernelSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelChoiceSemanticData p chief) : Nonempty (MinimalBlockFrattiniKernelSemanticData K)

Semantic residual: prove R = Phi(K) and the Frattini-collapse facts.

axiom Q2Presentation.Induction.minimalBlock_moduleExtractionSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelChoiceSemanticData p chief) (R : MinimalBlockFrattiniKernelSemanticData K) : Nonempty (MinimalBlockModuleExtractionSemanticData K R)

Semantic residual: extract M = K/R, T, C, and the induced actions.

axiom Q2Presentation.Induction.minimalBlock_simpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelChoiceSemanticData p chief} {R : MinimalBlockFrattiniKernelSemanticData K} (E : MinimalBlockModuleExtractionSemanticData K R) : Nonempty (MinimalBlockSimpleHeadSemanticData E)

Semantic residual: prove the simple-head and invariant-character consequences for the extracted tower.

def Q2Presentation.Induction.MinimalBlockGroupTowerData.ofSemantic {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelChoiceSemanticData p chief) (R : MinimalBlockFrattiniKernelSemanticData K) (E : MinimalBlockModuleExtractionSemanticData K R) (H : MinimalBlockSimpleHeadSemanticData E) : MinimalBlockGroupTowerData p chief

Reassemble the current group-tower packet from the semantic subgroup tower.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Induction.minimalBlock_groupTowerData_from_semanticClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Replacement theorem for minimalBlock_groupTowerData, assembled from the semantic K, R = Phi(K), module-extraction, and simple-head packets.

Semantic determinant-pushout packets

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

The central scalar-pushout square family over a pre-head tower.

The square map is not an arbitrary quadratic form: it is definitionally the extraspecial square form attached to phi.

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

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSemanticData.toQuadraticFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D

The finer quadratic-family packet induced by the extraspecial square map.

Equations

• S.toQuadraticFamily = { phi := S.phi, square := fun (lam : Module.Dual (ZMod 2) D.R) => Q2Presentation.Quadratic.Extraspecial.extraspecialForm (S.phi lam) }

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSemanticData.toSelfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : MinimalBlockPreheadCentralPushoutSelfDualityData D

The older self-duality packet obtained by forgetting the square map.

Equations

• S.toSelfDuality = { phi := S.phi }

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSemanticData.toExtraspecialFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : MinimalBlockPreheadExtraspecialFamilyData D

The bare extraspecial family induced by the same central-pushout data.

Equations

• S.toExtraspecialFamily = { phi := S.phi }

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSemanticData.squareDiagonalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : MinimalBlockPreheadCentralPushoutSquareDiagonalData S.toQuadraticFamily

The square map is the diagonal of the same phi family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSemanticData.polarSymmData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : MinimalBlockPreheadCentralPushoutPolarSymmData S.toQuadraticFamily

The polar map is the symmetrized phi pairing for the same family.

Equations

• ⋯ = ⋯

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutNaturalitySemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Prop

Naturality of the central-pushout self-duality 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), ((S.phi lam) ((D.actM c) m)) ((D.actM c) m') = ((S.phi lam) m) m'

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutNaturalitySemanticData.toExtraspecialNaturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) : MinimalBlockPreheadExtraspecialNaturalityData S.toExtraspecialFamily

Convert central-pushout naturality to the existing extraspecial naturality packet for the family induced by S.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutNaturalitySemanticData.toEquivariantFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) : MinimalBlockPreheadExtraspecialEquivariantFamilyData D

Build the downstream equivariant family from the same phi and naturality.

Equations

• N.toEquivariantFamily = { phi := S.phi, diagonal_invariant := ⋯ }

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Prop

Diagonal vanishing of the central-pushout square map 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, ((S.phi lam) t) t = 0

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutPolarZeroSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Prop

Polar vanishing of the central-pushout pairing on T x M.

• 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), ((S.phi lam) t) m + ((S.phi lam) m) t = 0

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Prop

Radical containment for the symmetrized central-pushout polar form.

• 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), ((S.phi lam) m) m' + ((S.phi lam) m') m = 0) → m ∈ D.T

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

Semantic residual: the central-pushout square/polar family.

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

Semantic residual: naturality of that same central-pushout family.

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

Semantic residual: diagonal vanishing on T.

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

Semantic residual: polar vanishing on T x M.

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

Semantic residual: radical containment for the symmetrized polar pairing.

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData.toExtraspecialDiagonalZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (Z : MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S) (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) : MinimalBlockPreheadExtraspecialDiagonalZeroData N.toEquivariantFamily

Convert the semantic diagonal-vanishing statement to the current packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutPolarZeroSemanticData.toExtraspecialPolarZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (P : MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S) (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) : MinimalBlockPreheadExtraspecialPolarZeroData N.toEquivariantFamily

Convert the semantic polar-vanishing statement to the current packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData.toExtraspecialRadicalContainment {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (R : MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S) (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) : MinimalBlockPreheadExtraspecialRadicalContainmentData N.toEquivariantFamily

Convert semantic radical containment to the current containment packet.

Equations

• ⋯ = ⋯

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

Replacement theorem for minimalBlock_preheadCentralPushoutQuadraticFamilyData on the semantic family.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSquareDiagonalData_from_semanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData S.toQuadraticFamily)

Replacement theorem for the square-diagonal packet on the semantic family.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutPolarSymmData_from_semanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData S.toQuadraticFamily)

Replacement theorem for the polar-symmetry packet on the semantic family.

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

Replacement theorem for the previous square/polar central-pushout packet, using the semantic extraspecial square family.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialNaturalityData_from_semanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadExtraspecialNaturalityData S.toExtraspecialFamily)

Replacement theorem for the old naturality residual, on the family induced by the semantic central pushout.

def Q2Presentation.Induction.minimalBlock_preheadExtraspecialEquivariantFamilyData_of_semantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) : MinimalBlockPreheadExtraspecialEquivariantFamilyData D

Build the equivariant extraspecial family from one semantic central-pushout family and its naturality.

Equations

• Q2Presentation.Induction.minimalBlock_preheadExtraspecialEquivariantFamilyData_of_semantic S N = N.toEquivariantFamily

def Q2Presentation.Induction.minimalBlock_preheadExtraspecialAnnihilationData_of_semantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) (Z : MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S) (P : MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S) : MinimalBlockPreheadExtraspecialAnnihilationData N.toEquivariantFamily

Build determinant annihilation from the semantic diagonal and polar vanishing packets, all tied to the same central-pushout family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.minimalBlock_preheadExtraspecialRadicalData_of_semantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) (R : MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S) : MinimalBlockPreheadExtraspecialRadicalData N.toEquivariantFamily

Build the radical packet from semantic radical containment.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialDiagonalZeroData_from_semanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) : Nonempty (MinimalBlockPreheadExtraspecialDiagonalZeroData N.toEquivariantFamily)

Replacement theorem for the old diagonal-zero residual, on the semantic central-pushout family.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialPolarZeroData_from_semanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) : Nonempty (MinimalBlockPreheadExtraspecialPolarZeroData N.toEquivariantFamily)

Replacement theorem for the old polar-zero residual, on the semantic central-pushout family.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialRadicalContainmentData_from_semanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) : Nonempty (MinimalBlockPreheadExtraspecialRadicalContainmentData N.toEquivariantFamily)

Replacement theorem for the old radical-containment residual, on the semantic central-pushout family.

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

Reassemble the equivariant family, annihilation, and radical packets from semantic central-pushout residuals over one pre-head tower.

Minimal-block and count routes through the semantic packets

theorem Q2Presentation.Induction.minimalBlock_of_nonScalar_proven_groupTowerSemanticClosers (p : FramedPair) : ¬ScalarTerminal p → Nonempty (MinimalBlock p)

Section 7 minimal-block reassembly through the semantic group tower and semantic determinant packets.

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

Nonterminal Fourier branch routed through semantic Section 7 packets and the existing marked-quotient Section 8 route.

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

Recursive branch using the semantic Section 7 nonterminal route.

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

Recursion step using the semantic Section 7 route.

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

Boundary-framed count equality through the semantic Section 7 route.

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

Equal finite surjection counts through the semantic Section 7 route.